CHAPTER 7. AN APPLICATION TO THE NEEDHAM- . . .
in Section 6.3, this kind of test cannot be made in the logic. Instead we ensure that the outcome of the test is readily observable by performing an output on channels, and this output action can be captured in the logic.
The remainder of the specification should be fairly self explanatory. The processesA4(i),B5, F AandF B are left unspecified; the first two express the behaviour of the respective principals after a successful run of the authentication protocol (and may e.g. continue communication with a symmetric key generated from a nonce), and the last two processes specify the behaviour on unexpected input (which we will not concern ourselves with for the present purpose).
7.2.6 A Trace of The Attack
A formal derivation from theSP EC process, which demonstrates the attack on the protocol, is given in Table 7.2.
The active substitutions arising from the three process outputs have variables x1,x2 andx3. For convenience we also represent the three environment inputs by active substitutions with variablesy1,y2andy3which areunder restriction.
The labelled semantics prescribe that environment input is substituted directly into the process in question (since we are working with the early semantics).
We then use the fact thatA{M/x} ≡(νx)({M/x} |A) to introduce a new active substitution with private variable.
7.3. LOGICAL PROPERTIES
SP EC≡(νa, na)(chξ1i.A1(1))|(νb0, nb0)c(y1).B1|P K
≡−−−−−→(νa, nνx1chx1i a)({ξ1/x1} |A1(1))|(νb0, nb0)c(y1).B1|P K
≡(νa, na, b0, nb0)({ξ1/x1} |A1(1)|c(y1).B1)|P K
c(y1)
−−−→≡(νa, na, b0, nb0, y1)({ξ1/x1} | {ξ2/y1} |A1(1)|B1)|P K
=(νa, na, b0, nb0, y1)({ξ1/x1} | {ξ2/y1} |A1(1)|chξ3i.B2)|P K
≡−−−−−−→(νa, nνx2.chx2i a, b0, nb0, y1, y2)({ξ1/x1} | {ξ2/y1} | {ξ3/x2} |A1(1)|B2)|P K
=(νa, na, b0, nb0, y1, y2)({ξ1/x1} | {ξ2/y1} | {ξ3/x2} |c(y2).A2(1)|B2)|P K
c(y2)
−−−→≡(νa, na, b0, nb0, y1, y2)({ξ1/x1} | {ξ2/y1} | {ξ3/x2} | {ξ4/y2}
|(if ξ5=E na thenA3elseF A)|B2)|P K
→(νa, na, b0, nb0, y1, y2)({ξ1/x1} | {ξ2/y1} | {ξ3/x2} | {ξ4/y2} |A3|B2|P K
=(νa, na, b0, nb0, y1, y2)({ξ1/x1} | {ξ2/y1} | {ξ3/x2} | {ξ4/y2} |chξ6i.A4|B2|P K
≡−−−−−→(νa, nνx3chx3i a, b0, nb0, y1, y2)({ξ1/x1} | {ξ2/y1} | {ξ3/x2} | {ξ4/y2} | {ξ6/x3} |A4|B2|P K
=(νa, na, b0, nb0, y1, y2)({ξ1/x1} | {ξ2/y1} | {ξ3/x2} | {ξ4/y2} | {ξ6/x3} |A4|c(y3).B3|P K
c(y3)
−−−→≡(νa, na, b0, nb0, y1, y2, y3)({ξ1/x1} | {ξ2/y1} | {ξ3/x2} | {ξ4/y2} | {ξ6/x3} | {ξ7/y3}
|A4|ifξ8=E nb0 thenB4 elseF B)|P K
→(νa, na, b0, nb0, y1, y2, y3)({ξ1/x1} | {ξ2/y1} | {ξ3/x2} | {ξ4/y2} | {ξ6/x3} | {ξ7/y3}
|A4|shsucci.B5)|P K
≡−−−−−→(νa, nνx4chx4i a, b0, nb0, y1, y2, y3)({ξ1/x1} | {ξ2/y1} | {ξ3/x2} | {ξ4/y2} | {ξ6/x3} | {ξ7/y3}
| {succ/x4} |A4|B5)|P K
ξ1= [z1, zb1,enc([na, za], zb1)] [a+, b1+,enc([na, a+], b1+)]
ξ2= [za, zb0,enc([fst(dec(trd(x1), b−1)), za], zb1)] [a+, b0+,enc([na, a+], b0+)]
ξ3= [zb0,fst(y1),enc([fst(dec(trd(y1), b−0)), nb0],fst(y1))] [b0+, a+,enc([na, nb0], a+)]
ξ4= [zb1, za,trd(x2)] [b1+, a+,enc([na, nb0], a+)]
ξ5=fst(dec(trd(y2), a−)) na
ξ6= [za, zb1,enc(snd(dec(trd(y2), a−)), zb1)] [a+, b1+,enc(nb0, b1+)]
ξ7= [za, zb0,enc(dec(trd(x3), b−1), zb0)] [a+, b0+,enc(nb0, b0+)]
ξ8=dec(trd(y3, b−0)) nb0
Table 7.2: A trace of the attack on the Needham-Schroeder Public Key Protocol.
The trace is shown in the top part of the table and relies on auxiliary definitions of terms as given in the bottom part, which consists of two columns: the left column gives the actual terms, while the right column gives the corresponding normal forms of the terms after applying active substitutions.
CHAPTER 7. AN APPLICATION TO THE NEEDHAM- . . .
that we have to use an existentially quantified variable x00 instead of directly usingnb0 because this is a private name. Does the processSP EC satisfyA2? The answer is no, because b−0 is not in the frame synthesis of the relevant derivative ofSP EC. The reason is that the namebis private in processBand is not revealed to the environment at any point in the trace. This corresponds to the intuition of the attack: the noncenb0 is not obtained by decrypting the message embedded iny3, but rather by usingAas an oracle and trickingAinto decrypting the message embedded iny3.
Hence an alternative formulation is called for:
A3 =∆ hνcihc(y¯ 1)ihν¯cihc(y2)ihν¯cihc(y3)ih¯si∃x(trd(y3) =enc(x, zb0)) This formula asserts that there is some synthesis term (x) which is syntactically equal to the term encrypted iny3, namelynb0. The processSP EC does satisfy A3 because nb0 is in the frame synthesis of the relevant derivative ofSP EC.
More precisely, the frame of the second last derivate ofSP ECis given as follows:
ϕ= (νa, na, b0, nb0, y1, y2, y3)({ξ1/x1} | {ξ2/y1} | {ξ3/x2} | {ξ4/y2} | {ξ6/x3} | {ξ7/y3}) The interesting term is ξ6 (bound to x3) which, when the private active sub-stitutions are applied, reduces to the triple [a+, b1+,enc(nb0, b1+)]. Since the name b1 is free inϕ, the last term of this triple can be decrypted so we have that
ecores(x3, ϕ) ={a+, b1+,enc(nb0, b1+), nb0}
Sinceecores(ϕ)⊆ S(ϕ) we have thatnb0 ∈ S(ϕ), confirming the satisfaction ϕLF ∃x(trd(y3) =enc(x, zb0))
and henceSP ECA3.
Yet another approach would be employ the technique in the proof of Propo-sition 3 in [2], which states that the problem of deciding static equivalence reduces to deciding membership of the synthesis set in theories which include public-key axioms. The idea is to add an active substitution with a fresh private name encrypted under the public key generated fromnb0 to theSP ECprocess:
SP EC0 =∆ SP EC|(νh){enc(h,nb0+)/y}
Then the noncenb0 can be deduced by the environment in the end of a successful protocol run exactly ifSP EC0 satisfies the following formulae:
A4 =∆ hν¯cihc(y1)ihν¯cihc(y2)ihν¯cihc(y3)ihshsuccii∃x∃x0(dec(y, x)> x0) The formulaA3describes the desired assertion more directly thanA4, butA4 has the advantage of also working in a setting with symmetric key encryption.
If the message containing the nonce nb0 were encrypted with a symmetric key not known by the environment, the term containing the noncenb0 could not be reconstructed in the logic and hence syntactical equality could not be tested as inA3.
102
7.3. LOGICAL PROPERTIES
7.3.2 General Safety Properties – Invariance
We have now demonstrated that the logic is sufficiently strong to capture the attack on the Needham-Schroeder Public Key Protocol. However the formulae A3 andA4 exhibited above were designed with the specific attack in mind. In a more general situation, when one is faced with a protocol specification to be verified, one would wish to express more general safety properties, e.g. that there is no possible trace leading to the disclosure of the nonce nb0.
More specifically, we would like to assert that whenever an (arbitrary) exe-cution trace of the protocol leads to the input of y3 in B3 followed an output of the success message, the nonce embedded in the input cannot be deduced by the environment. This amounts to asserting that the following formula (which is just the last part ofA3) holdsinvariantly – i.e. in any possible derived state ofSP EC:
A5 =∆ hc(y3)ihshsuccii¬∃x(trd(y3) =enc(x, zb0))
If we assume thatA4(i),B5,F AandF Bare finite processes, in the sense that they do not afford infinite transition sequences, then theSP EC process is also finite. In this case invariance can be defined using only constructs from the basic logic LA. LetU be any finite set of names and variables. We then define invariance of Aink steps inductively as follows:
Inv0U(A) =∆ A
InvkU+1(A) =∆ A∧[τ]InvkU(A)∧
^
u∈U
[¯u]InvkU(A)∧[νu]Inv¯ kU(A)∧[u(x)]InvkU(A)
Recall that the box modalities express necessity, so e.g. [τ]A expresses that no matter how an internal reduction is performed, the derived process must satisfy A. Hence the formulaInvk(A) expresses that no matter how a process performs k consecutive actions, the resulting derived process must satisfyA.
LetU be the set of variables and names occurring inSP EC and let kmax
be the upper bound on the length of possible transition sequences that SP EC can afford. We are now equipped to express a safety property which asserts that SP EC does not reveal the noncenb0 to the environment at any point in its execution:
A6 =∆ InvkUmax(A5)
Clearly SP EC 6 A6 as exemplified by the formula A3 given in the previous subsection, i.e. the safety property is not satisfied by our specification.
The definition of the invariance operator relies on processes with finite-length transition sequences (not to be mistaken for processes with finitestates). How-ever, systems with infinite behaviour arise in many settings where the above
CHAPTER 7. AN APPLICATION TO THE NEEDHAM- . . .
definition of invariance therefore would not suffice. A standard solution is to introduce process variables and recursion into the logic and thereby obtain a µ-calculus [17]. This allows invariance to be defined as a maximal fixed point of an appropriate semantic function over a complete lattice [6, Section 5.2]. Tarski’s Fixed Point Theorem [6, Appendix A] gives us that a unique such fixed point exists if the function is monotonic, and in order to satisfy this one would have to omit negation from the logic. We leave further developments in this direction for future work.