Comparison with LySa NS

LySa is a quite striped down calculus. For example, it has a limited set of cryptographic primitives, its notion of pattern matching is limited to be on prefixes of sequences, and it does not cater for private communication within a principal. The design of LySa^NS undertaken in [34] set out to investigate how these limitations may be removed. The result was a calculus with a richer variety of cryptographic primitives, a much more flexible mechanism for pattern matching, and a notion of private communication within bounded places. As a final interesting idea, LySa^NSintroduces a meta level that describes the scenarios in which a process will be deployed. It was illustrated in [34] that the analysis technology, which will be presented in the next chapter, is capable of dealing also with these auxiliary features.

The reason that LySa, and not LySa^NS, is used in this thesis is that LySa provides a simpler framework and consequently the theory can be presented a bit more smoothly. Furthermore, LySa suffice to illustrate most of the significant points about the analysis technique and, hence, there is no need to make an overly complex presentation.

One point that, however, cannot be made with LySa as presented in this sec-tion is the nosec-tion of deployment scenarios. Instead, the framework for dealing with deployment scenarios has been “back-ported” to the LySa calculus. This development is the topic of Chapter 6. Taking advantage of the simple setting provided by LySa, the theory concerning deployment scenarios is treated more

carefully in Chapter 6 than it was in [34].

In relation to the presentation in this thesis, the development of LySa^NS may be seen as an assurance that the techniques presented here can indeed be extended to deal with a more complex setup than the somewhat simplistic one described by the LySa calculus.

Control Flow Analysis

The analysis techniques used in this thesis come from the field known asstatic analysisand were originally developed for optimising compilers. These are tech-niques that works statically, i.e. at compile-time, to calculate some aspect of the behaviour of a program. Due to their origin, the techniques have several at-tractive features. For example, they are complexity-wise quite efficient and they may be used to analyse any program. Because of theoretic and efficiency con-cerns they rely on computing approximations rather than exact answers. These approximations are, however, made in such a way that they are safe with respect to a formal semantics.

In a classic setting, static analysis techniques are divided in to several classes depending e.g. on whether they compute the flow of data or the flow of control etc. in a program. When the techniques are reinterpreted in a process calculus setting it becomes a bit harder to precisely distinguish between data and program control structures due to the succinct and expressive nature of process calculi. In this thesis, the static analysis techniques will uniformly be referred to ascontrol flow analysis.

The specification, proofs, etc. of the analyses will be carried out in a Flow Logic setting. The presentation of this framework will be in two parts. First, in Section 3.1 some general concepts of Flow Logic and control flow analysis will be described. Second, in Section 3.2 a concrete example of a control flow analysis is given in the form of a fairly standard analysis of the process calculus LySa, which relies adaption of previously developed techniques [24, 25].

3.1 Concepts in Flow Logic

Flow Logic was first introduced in [108] where it was used for an analyse of the λ-calculus. Since then Flow Logic has been used for analysis of many different kinds of languages and good overviews of the approach may be found in [109, 114].

A control flow analysis of a processPworks by collecting information about some aspects of the behaviour ofP. This information is stored in a data structureA containing theanalysis components taken from the analysis domainAnalysis. In Flow Logic, the relationship between the analysis components and the syntax of the process, which is analysed, is made formal by defining a predicate, written A |= P, that holds precisely when A is a description of the behaviour of the processP.

In Flow Logic, the definition of an analyse, thus, is the definition of the predicate A |=P. This predicate is defined structurally on the syntax of the processP by giving rules of the form

A |=P iff a logic formula overP,A,|=, etc. holds

for each syntactic construct P. The intuition is that the logic formula charac-terises the way that the behaviour ofP is described in the analysis components A. In general, the formula can be an arbitrary formula in some logic and may e.g. recursively mentionA⁰|=P⁰ for arbitrary processesP⁰. In the general case, it is therefore necessary to define the analysis predicate co-inductively in the structure ofP.

For practical purposes, however, it typically suffices to use only inductive def-initions of the analysis predicate. To ensure that the inductive definition is well-founded, the logic formula is restricted so that it may only recursively men-tion the predicate A⁰ |=P⁰ for subprocessesP⁰ ofP. This class of Flow Logic specifications are sometimes called compositional because the analysis of a pro-cess will only require the analysis of its parts. Inductively defined Flow Logic specifications are the only ones considered in this thesis.