6.2 The Analysis
6.2.4 Implementation
The implementation of the meta level analysis is made by quite simple modifi-cation to the implementation of the object level analysis, which was described in Chapter 4.
The generation function on syntax,F, is equipped with an auxiliary parameter Γ accounting for the environment of assignments to set identifiers. The generation functionGcallsF with an empty environment. The generation functionFof all the object level constructs is as described in Table 4.4 except that the canonical names and the canonical variables now also considers indices.
The extension of the generation function to the meta level constructs closely follows the definition of the analysis predicate in Table 6.3. The most involved part is to fulfil the requirement for unique expression labels that must be added to object level expressions. The challenge in attaining unique expression labels though the meta level analysis arises because the analysis may modify the syntax of expressions by the substitution in the rule (MIPar) for the analysis of indexed parallel composition.
The remedy is to assign indices to the labels on expressions in the meta level syntax and extend the substitution to encompass labels as well. For example, to attain unique labels the following scheme can be used. All expressions in a meta level process are labelled uniquely. Furthermore, indices are added to the labels corresponding to the indexes bound by indexed parallel compositions in which the label appear. For example, an expression E that appears inside |i∈S|j∈S
will have a label lij. Whenever the expression is analysed the indices will be substituted by elements from the appropriate indexing sets.
As an aside, one could mention that a similar strategy could be used to assign indices to names and variables. This would liberate the user of the LySatool from the obligation of adding these indices. However, adding these indices by
hand is more flexible and can be used as a means for controlling the precision of the analysis.
Alternatively, one may wish to have a labelling that uses the same labels for identical names and variables akin to the labelling discussed in Example 4.13.
To obtain such a labelling one may proceed and assign label lV to an indexed name or variable V. Here, any indices on V will be interpreted as indices of the label and substituted accordingly. For example, a namenij will be give the label lnij andi andj are substituted when the corresponding indexed parallel compositions are analysed by applying the rule (MIPar).
The use of the attacker’s labell• in the implementation does not change by the above modifications. The labell•will simply be interpreted as having no indices and will therefore not be modified by substitution.
6.3 Summary
This chapter has described a syntactic extension to LySa that caters for speci-fication of deployment scenarios. This syntactic extension is referred to as the meta level. A meta level process specifiesan entire set of object level processes i.e. of ordinary LySa processes. This set of processes constitutes the deployment scenario, which conceptually describes how an application is allowed to be used.
Next, an analysis of meta level processes has been developed. This analysis aims at describing the behaviour of all the object level processes that a meta process describes. The analysis is an extension of the control flow analysis from Chapter 3. Correspondingly, the implementation of the meta level analysis is made by relying on the work of Chapter 4. Finally, the notion of a hardest attacker presented in Chapter 5 has been lifted to the meta level.
The meta level analysis can now be used to account for the way an application behaves in theentire scenario, in which the application may be deployed. The analysis can make this account even when the application is exposed to arbitrary attacks. A simple example of this is given below:
Example 6.9Recall the meta level process from Example 6.1 takingS1 andS2
to be the set of natural numbersN: letX ⊆Nin let Y ⊆Nin(ν K)
|i∈X|j∈Y (ν nij)hAi, Bj, niji.(Bj, Ai;xij).decryptxij as{nij;zij}Kin 0
| |j∈Y |i∈X (Ai, Bj;yij).(νmessij)hBj, Ai,{yij,messij}Ki.0
Let bNc be the set {1} and label the process with unique expression labels as discussed in Section 6.2.4. When analysing the above deployment scenario under attack from arbitrary attackers the implementation of the meta level analysis in
the LySatool finds the analysis result:
Notice that each of the canonical names and variables indexed with the canonical index 1 represents all the values where 1 could be substituted for any value inN. For example, the messagelA1lB1ln11 represent all the sequences in the Cartesian product
{Ai |i∈N} × {Bi |i∈N} × {nij |i∈N∧j∈N}
Even though this analysis result may appear to be extremely imprecise it is still informative. For example, it reveals that mess11 is not it the set ρ(x•). This means that no attacker can ever attain any of the messages messij no matter
how the meta level process is instantiated.
Example 6.9 is a simple example of how the meta level analysis may be used to analysearbitrarily large scenarios that a security aware networking applications may be deployed in. Chapter 7 gives many more examples of the use of the anal-ysis and, in particular, comments on how the analanal-ysis can be used to guarantee that the applications are able to tackle classical security problems.
The meta level analysis presented in this chapter bears some resemblance to the result shown by Comon-Lundh and Cortier [48]. They show that it suffices to consider a limited number of principals when analysing a protocol. The result is shown by projecting the behaviour of all principals onto a the limited number of principals. More precisely is suffices to consider k+ 1 principals where k is the number of different parts that a principal can play in the protocol. One comment on this is that Stoller has shown that there exists protocols that require exponentially many different principals [129] sokmay be quite large.
The meta level analysis can also be seen as projection of the behaviour of different principals. However, the projection is onto the canonical values in the analysis result rather that onto the semantic behaviour as in [48]. The approximations used here can, therefore, be made as fine or as coarse as you want correspond-ing to chooscorrespond-ing the number for different principals you want to consider. This can be done without jeopardising the soundness of the (computable) analysis result. On the downside, the approach presented here can only hope to validate properties that are defined up to the canonical assignment. The next chapter,
however, shows that this suffices for the properties such as confidentiality and authentication.
Security in Networking Systems
The development that has been presented so far has focused on building the technology necessary to analyse networking applications that work on insecure networks. This chapter focuses on how this technology can be used to directly address the security problems that arise in these systems.
It is important to recall that the analysis works by over-approximating the be-haviour of systems. Thus, if something (bad) doesnot turn up in the analysis result this something will not be a part of the system behaviour. That is, the analysis can be use to guarantee safety properties. In the context of security, this means that the analysis can be used to guarantee the absence of attacks.
On the other hand, if the analysis reports an attack there is a priori no way of knowing whether this is a real attack or whether it is a consequence of over-approximating. To show that a reported attack really does exist, one must devise an execution sequence that leads to the attack. In practice, it is often helpful to inspect the analysis result in order to devise such an attack sequence.
7.1 Confidentiality
One of the most important and simple security properties is confidentiality i.e.
the ability to keep messages secret. Interpreting the notion of confidentiality in LySa is quite straightforward. For example, one can use the following definition:
Definition 7.1 (Confidentiality) LetP be an arbitrary process andP•be an arbitrary attacker. The processP preserves confidentiality of a valueV if there are no execution
P |P•→∗P0 →P00 whereP0→P00 bindsV to a variable fromP•.
With this definition, it is straightforward to use the analysis to check whether a processP preserves confidentiality of some valueV.
Theorem 7.2 (Analysis of confidentiality) Let P be a process and V be a value such thatas(V)⊆as(P)andaa(V)⊆aa(P). If
ρ, κ|=P |(fn(P),ac(P),as(P),aa(P))-Phard and bVc 6∈ρ(x•) thenP preserves confidentiality of V.
ProofThe theorem is a corollary of Lemma 5.3 about the analysis of the hardest attacker and Theorem 3.12 about variable bindings recorded by the analysis: If V semantically may become bound to some variable of the attacker then bVc will be inρ(x•). Conversely, ifbVc 6∈ρ(x•) then no such binding can take place.
Notice that the value V must have an arity used in P because according to Lemma 5.6 these are the only ones that will be recorded inρ.
The notion of confidentiality can easily be extended to meta level processes. A meta level processM preserves confidentiality of a valueV if all instances ofM preserve confidentiality of V. The meta level analysis ofM together withPhard can then be used to check whetherM preserves confidentiality of some value.
The analysis result computed by the implementation does not represent ρ(x•) directly but instead uses a tree grammar encoding of the set. Recall from Sec-tion 5.3.1 that in the implementaSec-tion all the applied expressions in the attacker are labelled by a special labell•. This means thatρ(x•) =L(γ, l•) i.e. thatρ(x•) is the language generated by starting from l• in the tree grammar γ, which is computed by the implementation.
It may require some work to figure out whether a particular encrypted value is inL(γ, l•) i.e. whether a particular encrypted value is confidential. However, as discussed in Section 4.2.1 the tree grammars inγ are normalised, which makes it very simple to figure out whether a namen is confidential. One must simply inspect whether there exists a rulel•→ bncin γ; if not, thennis confidential.
Example 7.3Recall the public key “protocol” from Example 2.2:
(ν±K)hA, B, K+i.(B, A;x).decryptxas{|;xm|}K−in 0
|
(A, B;y).(νmess)hB, A,{|mess|}yi.0
The intention of the protocol is that the message generated by B is kept confi-dential when it is sent toA because it will be encrypted with the keyK+ and becauseK− is confidential.
The implementation of the analysis finds the following analysis result for the protocol under attack from an arbitrary attacker
ρ(x•) = {lA, lB, lK+, le, lm, l•}
The analysis result guarantees that the protocol preserves confidentiality ofK− because there is no rulel•→K−inγ. However, the analysis does not guarantee the confidentiality ofmess because the rulel•→mess is inγ.
Inspecting the analysis result a little closer, one finds the rulele→ {|lm|}l
• inγ, which says that, according to the analysis, the message can be encrypted using any value that the attacker knows. This will indeed also be the case semantically:
If the attacker knows the key pairm+, m− it can output hA, B, m+ithat will be received by principal B. Principal B replies by sendinghB, A,{|mess|}m+i, which the attacker then may receive. Now, the attacker can usem− to decrypt
mess.
An example of a protocol that preserves confidentiality has already been given in Example 6.9 on page 100. By inspection of the analysis result in Example 6.9 it is clear that there are no rules of the forml•→ bmessijcin the analysis result.
This means that the meta level analysis guarantees that the protocol preserves confidentiality of any messagemessij in any instance of the meta level process.