The Attacker

To study the attacker, consider the attack setup of P under attack from an arbitrary attacker P• but this time using the annotated syntax. In this setup

also the attacker process P• will be annotated. Because the semantics ignores the annotation, the choice of annotations ofP•has no real semantic consequence.

That is, the choice of annotations will not in any way effect possible attacks on a process. The annotations ofP•will, however, be crucial for determining whether a particular decryption violates the authentication property or not. The choice of these annotations will be a matter of striking the balance between reporting as many errors as possible but not reporting errors that are insignificant.

In the interest of reporting many attacks, the attackers will be equipped with a unique canonical crypto-point, c•. This crypto-point will be used in all the at parts of annotations in the attackers. In the interest of not reporting too many errors all destination and origin annotations will be void by choosing the set of all crypto-pointsCP as the set for thedest andorig part of annotations.

These choices, in effect, mean that when a process P is under attack from an attacker P• only the annotations in P will cause the authentication property to be violated. That is, the control of the errors that will be reported by the analysis is left entirely to the annotations in the processP.

The definition of an (N,AC,AS,AA)-attacker from Definition 5.1 will now be extended to incorporate annotations. It will require that all encryption are an-notated with [atcdestCP] and all decryptions are annotated with [atcorigCP] such that bcc= c•. Correspondingly, the hardest attacker Phard from Defini-tion 5.2 will be equipped with such annotaDefini-tions. It is then an immediate corollary of Theorem 7.5 and the results about the hardest attackerPhard that

Corollary 7.6 (Authentication under attack) If ρ, κ, ψ |= P |Phard and ψ=∅thenP|P_• ensures destination and origin authentication for all attackers P•.

That is, P ensures destination and origin authentication no matter which at-tacker it is composed with.

7.2.5 Implementation

The implementation of the hardest attacker is, in fact, not annotated with the set of all crypto-pointsCP because this is an infinite set. Instead the analysis of Pharduses the set{c•}∪bcp(P)cwhere cp(P) are the crypto-points in the process Pthat is analysed. The formulae generated byG(Phard) wherePhardis annotated with this set is equivalent to the formula generated when the annotations use CP.

The addition of annotations in the value domain means that the signature used for the tree grammars in the implementation must also be modified. Rather than using the signature ΣLySaas discussed in Section 4.2.2 the implementation

of the authentication analysis of the processP will be work over the signature ΣDLySadef

= {bnc0|n∈name(P)} ∪

{sencbccbCc_k+1 |k∈as(P)∧c∈cp(P)∧C∈ P(cp(P))} ∪ {aencbccbCc_k+1 |k∈as(P)∧c∈cp(P)∧C∈ P(cp(P))}

That is, the signature now containsk+ 1-ary function symbols sencbccbCcand sencbccbCccorresponding to all possible annotations ofk-ary encryptions.

The analysis ignores these annotations in the analysis pattern matching i.e. at the places where the set membership operator U_i Eϑ_i is used. Inspecting the definition of the generation function for syntax, F, in Table 4.4 one finds that these tests are exactly the ones that have been encoded as tests of non-empty intersections between two tree languages using the predicate NEI. To attain the effect of ignoring annotations the axiomatisation of NEI simply ignores the annotations when it is extended to values over ΣDLySa. With these modifications the implementation of the analysis can be used to check authentication properties of annotated LySa processes.

Example 7.7The error in the public key protocol of Example 7.3 may also be seen as an error of destination and origin authentication. Consider the protocol once more but this time with authentication annotations added:

(ν±K)hA, B, K⁺i.(B, A;x).decryptxas{|;xm|}_K−[ataorig{b}]in 0

|

(A, B;y).(νmess)hB, A,{|mess|}_y[atbdest{a}]i.0

The annotations formalise the intuition that the encryption at principalBis sup-pose to be decrypted at the decryption at principalA, only. The implementation finds that the authentication property may be violated:

ψ={(b, c•),(c•, a)}

The first error reports that something encrypted at the crypto-point b may be decrypted at an attacker. The second error reports that something encrypted at the attacker may end up being decrypted at the crypto-pointa. This corresponds to the problem reported in Example 7.3.

The remaining part of the analysis result is as in Example 7.3 except that an-notations are included on encrypted values:

ρ(x•) = {l_A, l_B, l_K⁺, l_e, l_m, l•} ρ(xm) = {l•, l_m}

κ = {l•} ∪

{lAlBl_K⁺, lBlAle, l•l•l•}

γ: l_A → A

The meta level authentication analysis is identical to the meta level analysis described in Chapter 6 except that is uses the authentication analysis of Table 7.1 to analyse object level constructs. The meta level authentication analysis is given as analysis predicates of the form ρ, κ, ψ |=Γ M that includes the error componentψ.

In order to make the authentication property more refined with respect to the scenario in which a meta level process may be deployed, the crypto-points are allowed to be indexed. That is, crypto-points are now of the form c_i. The indexes iniwill be substituted whenever the meta level process is instantiated thereby attaining individual crypto-points for each instantiated process. The meta level analysis of indexed parallel composition will, however, only analyse the substitution of indexes in a process up to an assignment of canonical indices.

Indexed crypto-points must therefore respect this canonical assignment and this is the reason that canonical crypto-points have been used in the object level analysis.

A meta level process ensures destination and origin authentication if all the process it instantiates to ensures destination and origin authentication:

Corollary 7.8 (Meta level authentication) If ρ, κ, ψ|=Γ M andψ=∅and MΓVP thenP ensures destination and origin authentication.

This is a straightforward corollary Theorem 6.8 and Theorem 7.5. In particular, Theorem 6.8 has to be extended to account for annotated values in the instanti-ation but this too is straightforward because instantiinstanti-ation will not depend upon any of these annotations.

The analysis that is implemented in the LySatool (version 2) is precisely this meta level authentication analysis.

Example 7.9In Example 5.8 a message was added to the simple nonce hand-shake from Example 2.1. This was done in order to illustrate that the nonce