--The John Clark and Jeremy Jacob Library of Protocols
 
--* - Indicates a flawed protocol
    
--6.1 Symetric Key Protocols Without Trusted Third Part
 
--6.1.1    ISO Symmetric Key One-Pass Unilateral Authentication Protocol
--Known: A.KAB = B.KAB
 
--A -> B: txt2, {[Ta|Na], B, txt1}KAB

X: assume(A.Kab == B.Kab);
A: => B(<txt2, e[<Na, B, txt1>]Kab>);
B: <- (msg1);
B: (txt2, enc):= msg1;
B: (Na, B, txt1) := d[enc]Kab;
-- Any assertions possible?

--6.1.2    ISO Symmetric Key Two-Pass Unilateral Authentication Protocol
 
--A -> B: RB, txt1
--B -> A: txt3, {RB, B, txt2}KAB

X: assume(A.Kab == B.Kab);
A:  => B(<Rb, txt1>);
B: <-(msg1);
B: (Rb, txt1) := msg1;
B: => A(<txt3, e[<Rb, B, txt2>]Kab>);
A: <-(msg2);
A: (txt3, enc) := msg2;
A: (Rb', B, txt2) := d[enc]Kab;
A: assert(Rb == Rb');

--6.1.3    ISO Symmetric Key One-Pass Mutual Authentication Protocol
 
--A -> B: txt2, {[Ta|Na], B, txt1}KAB
--B -> A: txt4, {[Ta|Nb], A, txt3}KAB

--Note: same as 6.1.1 except B sends message as well

X: assume(A.Kab == B.Kab);
A: => B(<txt2, e[<Na, B, txt1>]Kab>);
B: <- (msg1);
B: (txt2, enc1):= msg1;
B: (Na, B, txt1) := d[enc1]Kab; 

B: => A(<txt4, e[<Nb, A, txt1>]Kab>);
A: <- (msg2);
A: (txt4, enc2):= msg2;
A: (Nb, A, txt3) := d[enc2]Kab; 

--6.1.4    ISO Symmetric Key Three-Pass Unilateral Authentication Protocol
 
--A -> B: RA, txt1
--B -> A: txt3, {RA, RB, B, txt2}KAB
--A -> B: txt5, {RB, RA, txt4} KAB

X: assume(A.Kab == B.Kab);
A:  => B(<Ra, txt1>);
B: <-(msg1);
B: (Ra, txt1) := msg1;

B: => A(<txt3, e[<Rb, Ra, A, txt2>]Kab>);
A: <-(msg2);
A: (txt3, enc) := msg2;
A: (Rb, Ra', B, txt2) := d[enc]Kab;
A: assert(Ra == Ra');

A: =>B(<txt5, e[<Ra, Rb, txt4>]Kab>);
B: <- (msg3);
B: (txt5, enc3) := msg3;
B: (Ra'', Rb', txt4) := d[enc3]Kab;
B: assert(Rb == Rb');
 
--6.1.5    Using Non-Reversible Functions
 
--A -> B: A, RA
--B -> A: B, {hash(RA), RB, B, K}KAB
--A -> B: A, {hash(RB)}KAB

X: assume(A.Kab == B.Kab);
A: => B(hash);
B: <-(hash);

A: => B(<A, Ra>);
B: <-(msg1);
B: (A, Ra) := msg1;

B: => A(<B, e[<ep[Ra]hash, Rb, B, K>]Kab>);
A: <- (msg2);
A: (B, enc1) := msg2;
A: (auth, Rb, B, K) := d[enc1]Kab;
A: check := ep[Ra]hash;
A: assert(auth == check);

A: => B(<A, e[ep[Rb]hash]Kab>);
B: <-(msg3);
B: (A, enc2) := msg3;
B: auth := d[enc2]Kab;
B: check := ep[Rb]hash;
B: assert(auth == check);
 
--Question: What purpose does hashing serve in this protocol?
--Answers:  Reduce msg length, amount encrypted?
 
--6.1.6    Andrew Secure RPC Protocol*
 
--A -> B: A, {NA}KAB
--B -> A: {NA+1, NB}KAB
--A -> B: {NB+1}KAB
--B -> A: {K, NB2}KAB
 
X: assume(A.Kab == B.Kab);
A: => B(<A, e[Na]Kab>);
B: <- (msg1);
B: (A, enc1) := msg1;
B: Na := d[enc1]Kab;
B: => A(e[<f(Na), Nb>]Kab);
A: <-(msg2);
A: (fNa', Nb) := d[msg2]Kab;
A: fNa := f(Na);
A: assert(fNa == fNa');
A: => B(e[f(Nb)]Kab);
B: <- (msg3);
B: fNb' := d[msg3]Kab;
B: fNb := f(Nb);
B: assert(fNb == fNb');
B: => A(e[<Kab', Nb'>]Kab);
A: <- (msg4);
A: (Kab', Nb') := d[msg4]Kab;


--NOTE:  How do you best represent Na+1 in CPAL? e[x]f ?

--6.2 Authentication Using Cryptographic Check Functions
 
--6.2.1 ISO One-Pass Unilateral Authentication with CryptographicCheckFunctions
 
--A->B: [Ta|Na], B, txt2, hash{Kab, [Ta|Na], B, txt1}

A: => B(<hash, Kab, txt1>);
B: <- (pre);
B: (hash, Kab, txt1) := pre;

A: => B(<Na, B, txt2, ep[<Kab, Na, B, txt1>]hash>);
B: <- (msg1);
B: (Na, B, txt2, auth) := msg1;
B: check := ep[<Kab, Na, B, txt1>]hash;
B: assert(auth == check);

--6.2.2 ISO Two-Pass Unilateral Authentication with CCFs
 
--A->B: Ra, txt1
--B->A: txt3, hash{Kab, Ra, A, txt2}

--Pre-Protocol Ops
A: =>B(<hash, A, Kab, txt2>);
B: <-(pre);
B: (hash, A, Kab, txt2) := pre;
--Protocol Start
A: => B(<Ra, txt1>);
B: <- (msg1);
B: (Ra, txt1) := msg1;
B: => A(<txt3, e[<Kab, Ra, A, txt2>]hash>);
A: <- (msg2);
A: (txt3, auth) := msg2;
A: check := e[<Kab, Ra, A, txt2>]hash;
A: assert(auth == check);
 
--6.2.3 ISO Two-Pass Mutual Authentication with CCFs
 
--A -> B: [Ta|Na], txt2, hash{[Ta|Na], B, txt1}Kab
--B -> A: [Tb|Nb], txt4, hash{[Tb|Nb], A, txt3}Kab
 

--Pre-Protocol Ops
A: =>B(<hash, A, B, Kab, txt1, txt3>);
B: <-(pre);
B: (hash, A, B, Kab, txt1, txt3) := pre;
--Protocol Start
A: => B(<Na, txt2, e[<Kab, Na, B, txt1>]hash>); -- had to add id B, to construct hash
B: <- (msg1);
B: (Na, txt2, auth) := msg1;
B: check := e[<Kab, Na, B, txt1>]hash;
B: assert(auth == check);

B: => A(<Nb, txt2, e[<Kab, Nb, A, txt3>]hash>);
A: <- (msg2);
A: (Nb, txt4, auth) := msg2;
A: check := e[<Kab, Nb, A, txt3>]hash;
A: assert(auth == check);

--6.2.4    ISO Three-Pass Mutual Authentication with CCF
 
--A -> B: RA, txt1
--B -> A: txt3, hash{RB, RA, A, txt2}KAB
--A -> B: txt5, hash{RA, RB, txt4} KAB

--Pre-Protocol Ops
A: =>B(<hash, A, Kab, txt2, txt4>);
B: <-(pre);
B: (hash, A, Kab, txt2, txt4) := pre;
--Protocol Start
A: => B(<Ra, txt1>);
B: <- (msg1);
B: (Ra, txt1) := msg1;

B: => A(<Rb, txt3, e[<Kab, Rb, Ra, A, txt2>]hash>);
A: <- (msg2);
A: (Rb, txt3, auth) := msg2;
A: check := e[<Kab, Rb, Ra, A, txt2>]hash;
A: assert(auth == check);

A: => B(<txt5, e[<Kab, Ra, Rb, txt4>]hash>);
B: <- (msg3);
B: (txt5, auth) := msg3;
B: check := e[<Kab, Ra, Rb, txt4>]hash;
B: assert(auth == check);
 
--6.3     Symmetric Key Protocols Involving Trusted Third Parties
 
--6.3.1    Needham Schroeder Protocol with Conventional Keys*
 
--A -> S:  A, B, Na
--S -> A:  {Na, B, Kab, {Kab, A}Kbs}Kas
--A -> B:  {Kab, A}Kbs
--B -> A:  {Nb}Kab
--A -> B:  {Nb + 1}Kab


 
--6.3.2    Denning Sacco Protocol
 
--A->S:  A, B
--S->A:  {B, Kab, T, {A, Kab, T}Kbs}Kas
--A->B:  {A, Kab, T}Kbs
 
--6.3.3        Otway-Rees Protocol*
 
--A->B:  M, A, B, {Na, M, A, B}Kas
--B->S:  M, A, B, {Na, M, A, B}Kas, {Nb, M, A, B}Kbs
--S->B:  M, {Na, Kab}Kas, {Nb, Kab}Kbs
--B->A:  M, {Na, Kab}Kas
 
--6.3.4        Amended Needham Schroeder Protocol
 
--A->B:  A
--B->A:  {A, Nb1}Kbs
--A->S:  A, B, Na, {A, Nb1}Kbs
--S->A:  {Na, B, Kab, {Kab, Nb1, A}Kbs}Kas
--A->B:  {Kab, Nb1, A}Kbs
--B->A:  {Nb}Kab
--A->B:  {Nb-1}Kab

X: assume(B.Kbs == S.Kbs);
X: assume(A.Kas == S.Kas);

A: => B(A);
B: <-(A);

B: => A(e[<A, Nb'>]Kbs);
A: <-(msg2);

A: => S(<A, B, Na, msg2>);
S: <- (msg3);
S: (A, B, Na, msg2) := msg3;
S: (A', Nb') := d[msg2]Kbs;

S: => A(e[<Na, B, Kab, e[<Kab, Nb', A'>]Kbs>]Kas);
A: <- (msg4);
A: (Na', B', Kab, cert) := d[msg4]Kas;
A: assert(Na == Na');
A: assert(B == B');

A: => B(cert);
B: <- (msg5);
B: (Kab, Nb'', A') := d[msg5]Kbs;
B: assert(Nb' == Nb'');
B: assert(A == A');

B: => A(e[Nb]Kab);
A: <- (msg6);
A: Nb := d[msg6]Kab;

A: => B(e[f(Nb)]Kab);
B: <- (msg7);
B: fNb' := d[msg7]Kab;
B: fNb := f(Nb);
B: assert(fNb == fNb');

--Note: Last two messages confirm Kab and msg 6 authenticates B
 
--6.3.5        Wide Mouthed Frog Protocol*
 
--A->S:  A, {Ta, B, Kab}Kas
--S->B:  {Ts, A, Kab}Kbs
 
--Goal: Supposed to authenticate A, transport session key to B
 
--6.3.6        Yahalom*
 
--A->B:  A, Na
--B->S:  B, {A, Na, Nb}Kbs
--S->A:  {B, Kab, Na, Nb}Kas, {A, Kab}Kbs
--A->B:  {A, Kab}Kbs, {Nb}Kab
 
--* - Attack is based on {A, Na, Nb}Kbs replacing {A, Kab}Kbs in msg 4
--(this only works if length(Keys) = length(Na,Nb)), second part of
--message 4 from attacker is {Nb}NaNb but I don't know how the
--attacker is supposed to discover Nb. on. p49
 
--6.3.7        Carlsen's Secret Key Initiator Protocol
 
--A->B:  A, Na
--B->S:  A, Na, B, Nb
--S->B:  {Kab, Nb, A}Kbs, {Na, B, Kab}Kas
--B->A: {Na, B, Kab}Kas, {Na}Kab, N'b
--A->B:  {N'}Kab

X: assume(B.Kbs == S.Kbs);
X: assume(A.Kas == S.Kas);

A: =>B(<A, Na>);
B: <- (msg1);
B: (A, Na) := msg1;

B: =>S(<A, Na, B, Nb>);
S: <- (msg2);
S: (A, Na, B, Nb) := msg2;

S: =>B(<e[<Kab, Nb, A>]Kbs, e[<Na, B, Kab>]Kas>);
B: <- (msg3);
B: (secB, secA) := msg3;
B: (Kab, Nb', A') := d[secB]Kbs;
B: assert(Nb == Nb');
B: assert(A == A');

B: => A(<secA, e[Na]Kab, N'b>);
A: <- (msg4);
A: (secA, eNa, N'b) := msg4;
A: (Na', B, Kab) := d[secA]Kas;
A: assert(Na == Na');
A: Na'' := d[eNa]Kab;
A: assert(Na == Na'');

A: => B(e[N'b]Kab);
B: <- (msg5);
B: N''b := d[msg5]Kab;
B: assert(N'b == N''b);
 
--6.3.8        ISO Four-Pass Authentication Protocol
 
--A->B:  TVPa, B, txt1
--S->A:  txt4, {TVPa, Kab, B, txt3}Kas, {[Ts|Ns], Kab, A, txt2}Kbs
--A->B:  txt6, {[Ts|Ns], Kab, A, txt2}Kbs, {[Ta|Na], B, txt5}Kab
--B->A:  txt8, {[Tb|Nb], A, txt7}Kab
 
--6.3.9        ISO Five-Pass Authentication Protocol
 
--A->B:  Ra, txt1
--B->S:  R'b, Ra, A, txt2
--S->B:  txt5, {R'b, Kab, A, txt4}Kbs, {Ra, Kab, B, txt3}Kas
--B->A:  txt7, {Ra, Kab, B, txt3}Kas, {Rb, Ra, txt6}Kab
--A->B:  txt9, {Ra, Rb, txt8}Kab

X: assume(B.Kbs == S.Kbs);
X: assume(A.Kas == S.Kas);

A: => B(<Ra, txt1>);
B: <-(msg1);
B: (Ra, txt1) := msg1;

B: => S(<R'b, Ra, A, txt2>);
S: <-(msg2);
S: (R'b, Ra, A, txt2) := msg2;

S: => B(<txt5, e[<R'b, Kab, A, txt4>]Kbs, e[<Ra, Kab, B, txt3>]Kas>);
B: <- (msg3);
B: (txt4, tickB, tickA) := msg3;
B: (R''b, Kab, A', txt4) := d[tickB]Kbs;
B: assert(R'b == R''b);
B: assert(A == A');

B: => A(<txt7, tickA, e[<Rb, Ra, txt6>]Kab>);
A: <-(msg4);
A: (txt7, tickA, chalA) := msg4;
A: (Ra', Kab, B, txt3) := d[tickA]Kas;
A: assert(Ra == Ra');
A: (Rb, Ra'', txt6) := d[chalA]Kab;
A: assert(Ra == Ra'');

A: => B(<txt9, e[<Ra, Rb, txt8>]Kab>);
B: <-(msg5);
B: (txt9, chalB) := msg5;
B: (Ra', Rb', txt8) := d[chalB]Kab;
B: assert(Rb == Rb');
B: assert(Ra == Ra');
 
--6.3.10    Woo and Lam Authentication Protocols
--Assume: principals can detect replay
 
--WL f
--A->B:  A
--B->A:  Nb
--A->B:  {A, B, Nb}Kas
--B->S:  {A, B, Nb, {A, B, Nb}Kas}Kbs
--S->B:  {A, B, Nb}Kbs

--6.3.10    Woo and Lam Authentication Protocols
--Assume: principals can detect replay
 
--WL f
--A->B:  A
--B->A:  Nb
--A->B:  {A, B, Nb}Kas
--B->S:  {A, B, Nb, {A, B, Nb}Kas}Kbs
--S->B:  {A, B, Nb}Kbs

-- PreStart Setup
X: assume(B.Kbs == S.Kbs);
X: assume(A.Kas == S.Kas);
X: =>A(B); -- B cannot check id's unless A has same id for B as it has.
A: <-(B);  -- Otherwise, why should S send B in message 5?
X: =>B(B);
B: <-(B);

-- Protocol Start
A: => B(A);
B: <-(A);

B: => A(Nb);
A: <-(Nb);

A: => B(e[<A, B, Nb>]Kas);
B: <-(tickA);

B: => S(e[<A, B, Nb, tickA>]Kbs);
S: <-(msg4);
S: (A, B, Nb, tickA) := d[msg4]Kbs;
S: A_B_Nb := d[tickA]Kas;
S: assert(<A, B, Nb> == A_B_Nb);

S: => B(e[<A, B, Nb>]Kbs);
B: <-(msg5);
B: A_B_Nb := d[msg5]Kbs;
B: assert(<A, B, Nb> == A_B_Nb);

--WL 1
--A->B:  A
--B->A:  Nb
--A->B:  {A, B, Nb}Kas
--B->S:  {A, B, {A, B, Nb}Kas}Kbs
--S->B:  {A, B, Nb}Kbs

-- PreStart Setup
X: assume(B.Kbs == S.Kbs);
X: assume(A.Kas == S.Kas);
X: =>A(B);
A: <-(B);
X: =>B(B);
B: <-(B);

-- Protocol Start
A: => B(A);
B: <-(A);

B: => A(Nb);
A: <-(Nb);

A: => B(e[<A, B, Nb>]Kas);
B: <-(tickA);

B: => S(e[<A, B, tickA>]Kbs);
S: <-(msg4);
S: (A, B, tickA) := d[msg4]Kbs;
S: (A', B', Nb) := d[tickA]Kas;
S: assert(<A, B> == <A', B'>);

S: => B(e[<A, B, Nb>]Kbs);
B: <-(msg5);
B: A_B_Nb := d[msg5]Kbs;
B: assert(A_B_Nb == <A, B, Nb>);
 
--WL 2
--A->B:  A
--B->A:  Nb
--A->B:  {A, Nb}Kas
--B->S:  {A, {A, Nb}Kas}Kbs
--S->B:  {A, Nb}Kbs

-- PreStart Setup
X: assume(B.Kbs == S.Kbs);
X: assume(A.Kas == S.Kas);

-- Protocol Start
A: => B(A);
B: <-(A);

B: => A(Nb);
A: <-(Nb);

A: => B(e[<A, Nb>]Kas);
B: <-(tickA);

B: => S(e[<A, tickA>]Kbs);
S: <-(msg4);
S: (A, tickA) := d[msg4]Kbs;
S: (A', Nb) := d[tickA]Kas;
S: assert(A == A');

S: => B(e[<A, Nb>]Kbs);
B: <-(msg5);
B: A_Nb := d[msg5]Kbs;
B: assert(A_Nb == <A, Nb>);

--WL 3
--A->B:  A
--B->A:  Nb
--A->B:  {Nb}Kas
--B->S:  {A, {Nb}Kas}Kbs
--S->B:  {A, Nb}Kbs
 
-- PreStart Setup
X: assume(B.Kbs == S.Kbs);
X: assume(A.Kas == S.Kas);

-- Protocol Start
A: => B(A);
B: <-(A);

B: => A(Nb);
A: <-(Nb);

A: => B(e[Nb]Kas);
B: <-(tickA);

B: => S(e[<A, tickA>]Kbs);
S: <-(msg4);
S: (A, tickA) := d[msg4]Kbs;
S: Nb := d[tickA]Kas;
-- i.e. shoul we do an assert on A here?
-- No, A is used to determine decrypt key to use so it is already checked..

S: => B(e[<A, Nb>]Kbs);
B: <-(msg5);
B: A_Nb := d[msg5]Kbs;
B: assert(A_Nb == <A, Nb>);

--WL final simplification*
--A->B:  A
--B->A:  Nb
--A->B:  {Nb}Kas
--B->S:  {A, {Nb}Kas}Kbs
--S->B:  {Nb}Kbs

-- PreStart Setup
X: assume(B.Kbs == S.Kbs);
X: assume(A.Kas == S.Kas);

-- Protocol Start
A: => B(A);
B: <-(A);

B: => A(Nb);
A: <-(Nb);

A: => B(e[Nb]Kas);
B: <-(tickA);

B: => S(e[<A, tickA>]Kbs);
S: <-(msg4);
S: (A, tickA) := d[msg4]Kbs;
S: Nb := d[tickA]Kas;

S: => B(e[Nb]Kbs);
B: <-(msg5);
B: Nb' := d[msg5]Kbs;
B: assert(Nb == Nb');
 
--* - Don't follow first attack. p52.  But do follow second one.
 
--6.3.11    Woo and Lam Mutual Authenticaiton Protocol*
 
--P->Q:  P, Np
--Q->P:  Q, Nq
--P->Q:  {P, Q, Np, Nq}Kps
--Q->S:  {P, Q, Np, Nq}Kps, {P, Q, Np, Nq}Kqs
--S->Q:  {Q, Np, Nq, Kpq}Kps, {P, Np, Nq, Kpq}Kqs
--Q->P:  {Q, Np, Nq, Kpq}Kps, {Np, Nq}Kpq
--P->Q:  {Kq}Kpq

X: assume(P.Kps == S.Kps);
X: assume(Q.Kqs == S.Kqs);

P: => Q(<P, Np>);
Q: <-(msg1);
Q: (P, Np) := msg1;

Q: => P(<Q, Nq>);
P: <-(msg2);
P: (Q, Nq) := msg2;

P: => Q(e[<P, Q, Np, Nq>]Kps);
Q: <-(tickP);

Q: => S(<tickP, e[<P, Q, Np, Nq>]Kqs>);
S: <-(msg4);
S: (tickP, tickQ) := msg4;
S: (P, Q, Np, Nq) := d[tickQ]Kqs;
S: (P', Q', Np', Nq') := d[tickP]Kps;
S: assert(<P, Q, Np, Nq> == <P', Q', Np', Nq'>);

S: => Q(<e[<Q, Np, Nq, Kpq>]Kps, e[<P, Np, Nq, Kpq>]Kqs>);
Q: <-(msg5);
Q: (tickP, tickQ) := msg5;
Q: (P', Np', Nq', Kpq) := d[tickQ]Kqs;
Q: assert(<P', Np', Nq'> == <P, Np, Nq>);

Q: => P(<tickP, e[<Np, Nq>]Kpq>);
P: <-(msg6);
P: (tickP, chalP) := msg6;
P: (Q', Np', Nq', Kpq) := d[tickP]Kps;
P: assert(<Q', Np', Nq'> == <Q, Np, Nq>);
P: (Np'', Nq'') := d[chalP]Kpq;
P: assert(<Np, Nq> == <Np'', Nq''>);
 
-- Attack allows one participant to get two sessions going with
-- same key.  Weak
 
--6.4             Signatures with Conventional Key Encryption
 
--6.4.1        Needham-Schroeder Signature Protocol
 
--A->S:  A, {hash(msg)}Ka
--S->A:  {A, hash(msg)}Ks
--A->B:  msg, {A, hash(msg)}Ks
--B->S:  B, {A, hash(msg)}Ks
--S->B:  {A, hash(msg)}Kb
 
--6.5         Symmetric Key Repeated Authentication Protocols
--6.5.1        Kerberos Version 5
 
--U        user
--C        client
--G        Ticket granting server
--A        Key Distribution center
--S        server
--Tcg      {U, C, G, Kcg, Tstart, Texpire}Kag
--Acg      {C, T}Kcg
--Tcs      {U, C, S, Kcs, T'start, T'expire}Kcg
--Acs      {C, T'}Kcs
--Ku       key known to A & C, shared, U's password allows it to decrypt
--L1	   Lifetime
 
--C->A:  U, G, L1, N1
--A->C:  U, Tcg, {G, Kcg, Tstart, Texpire, N1}Ku
--C->G:  S, L2, N2, Tcg, Acg
--G->C:  U, Tcs, {S, Kcs, T'start, T'expire}Kcg
--C->S:  Tcs, Acs
--S->C:  {T'}Kcs
 
--Before Start of Protocol
X: => A(C);
A: <-(C);
X: => C(C);
C: <-(C);
--Start of Protocol

X: assume(A.Kag == G.Kag);
X: assume(C.Ku == A.Ku);
X: assume(C.Kcg == G.Kcg);
X: assume(S.Kgs == G.Kgs);

C: => A(<U, G, L1, N1>);
A: <-(msg1);
A: (U, G, L1, N1) := msg1;

A: => C(<U, e[<U, C, G, Kcg, Tst, Texp>]Kag, e[<G, Kcg, Tst, Texp, N1>]Ku>);
C: <-(msg2);
C: (U', tickAG, tickU) := msg2;
C: assert(U == U');
C: (G', Kcg, Tst, Texp, N1') := d[tickU]Ku;
C: assert(<N1, G> == <N1', G'>);

C: => G(<S, L2, N2, tickAG, e[<C, T>]Kcg>);
G: <-(msg3);
G: (S, L2, N2, tickAG, timeCG) := msg3;
G: (U, C', G, Kcg, Tst, Texp) := d[tickAG]Kag;
G: (C, T) := d[timeCG]Kcg; -- T assures freshness, compared with Tst, Texp
G: assert(C == C');

G: => C(<U, e[<U, C, S, Kcs, T'st, T'exp>]Kgs, e[<S, Kcs, T'st, T'exp>]Kcg>);
C: <- (msg4);
C: (U, tickGS, tickCG) := msg4;
C: (S', Kcs, T'st, T'exp) := d[tickCG]Kcg;
C: assert(S == S');

C: => S(<tickGS, e[<C, T'>]Kcs>);
S: <-(msg5);
S: (tickGS, timeCS) := msg5;
S: (U, C, S, Kcs, T'st, T'exp) := d[tickGS]Kgs;
S: (C', T') := d[timeCS]Kcs; -- T' assures freshness, comp with T'st, T'exp
S: assert(C == C');

S: => C(e[T']Kcs);
C: <-(msg6);
C: T'' := d[msg6]Kcs;
C: assert(T' == T'');


--6.5.2        Neumann Stubblebine*
 
--      Initial Protocol
--A->B:  A, Na
--B->S:  B, {A, Na, Tb}Kbs, Nb
--S->A:  {B, Na, Kab, Tb}Kas, }{A, Kab, Tb}Kbs, Nb
--A->B:  {A, Kab, Tb}Kbs, {Nb}Kab
 
 --           Repeated Authentication
--A->B:  N'a, {A, Kab, Tb}Kbs
--B->A:  N'b, {N'a}Kab
--A->B:  {N''b}Kab
 
--6.5.3        Kehne Langendorfer Schoenwalder KLS*
 
 --     Initial
--A->B:  A, Na
--B->S:  Na, A, Nb, B
--S->B:  {Nb, A, Kab}Kbs, {Na, B, Kab}Kas
--B->A:  {Na, B, Kab}Kas, {Tb, A, Kab}Kbb, Nc, {Na}Kab
--A->B:  {Nc}Kab
 
--            Repeated
--A->B:  N'a, {Tb, A, Kab}Kab
--B->A:  N'b, {N'a}Kab
--A->B:  {N'b}Kab
 
-- BEFORE PROTOCOL
-- A must have ID for B before protocol starts in order to
-- check that the B identifier in tickAS is good.  Otherwise
-- an intruder could substitute his ID I in msg2 so a tickBS
-- would be encrypted with Kis instead of Kbs.
X: => A(B);
A: <-(B);
X: => B(B);
B: <-(B);
-- Need to discuss above with Dr. Yasinsac.  Do with assume instead?

-- Protocol START
X: assume(A.Kas == S.Kas);
X: assume(B.Kbs == S.Kbs);

A: => B(<A, Na>);
B: <-(msg1);
B: (A, Na) := msg1;

B: => S(<Na, A, Nb, B>);
S: <-(msg2);
S: (Na, A, Nb, B) := msg2;

S: => B(<e[<Nb, A, Kab>]Kbs, e[<Na, B, Kab>]Kas>);
B: <-(msg3);
B: (tickBS, tickAS) := msg3;
B: (Nb', A', Kab) := d[tickBS]Kbs;
B: assert(<Nb, A> == <Nb', A'>);

B: => A(<tickAS, e[<Tb, A, Kab>]Kbb, Nc, e[Na]Kab>);
A: <-(msg4);
A: (tickAS, tickBB, Nc, tickAB) := msg4;
A: (Na', B', Kab) := d[tickAS]Kas;
A: assert(<B, Na> == <B', Na'>);

A: => B(e[Nc]Kab);
B: <- (msg5);
B: Nc' := d[msg5]Kab;
B: assert(Nc == Nc');

-- Repeated Part of Protocol
A: => B(<N'a, tickBB>);
B: <-(msg1b);
B: (N'a, tickBB) := msg1b;
B: (Tb', A', Kab') := d[tickBB]Kbb; -- Tb' assures freshness of key

B: => A(<N'b, e[N'a]Kab>);
A: <-(msg2b);
A: (N'b, tickAB') := msg2b;
A: N'a' := d[tickAB']Kab;
A: assert(N'a == N'a');

A: => B(e[N'b]Kab);
B: <-(msg3b);
B: N'b' := d[msg3b]Kab;
B: assert(N'b == N'b');

--6.5.4        The Kao Chow Repeated Authentication Protocols
 
--      One* 
--A->S:  A, B, Na
--S->B:  {A, B, Na, Kab}Kas, {A, B, Na, Kab}Kbs
--B->A:  {A, B, Na, Kab}Kas, {Na}Kab, Nb
--A->B:  {Nb}Kab

X: assume(S.Kas == A.Kas);
X: assume(S.Kbs == B.Kbs);

-- START
A: => S(<A, B, Na>);
S: <-(msg1);
S: (A, B, Na) := msg1;

S: => B(<e[<A, B, Na, Kab>]Kas, e[<A, B, Na, Kab>]Kbs>);
B: <-(msg2);
B: (tickAS, tickBS) := msg2;
B: (A, B, Na, Kab) := d[tickBS]Kbs;

B: => A(<tickAS, e[Na]Kab, Nb>);
A: <-(msg3);
A: (tickAS, tickAB, Nb) := msg3;
A: (A', B', Na', Kab) := d[tickAS]Kas;
A: assert(<A, B, Na> == <A', B', Na'>);
A: Na'' := d[tickAB]Kab;
A: assert(Na == Na'');

A: => B(e[Nb]Kab);
B: <-(msg4);
B: Nb' := d[msg4]Kab;
B: assert(Nb ==  Nb'); 

--            Two
--A->S:  A, B, Na
--S->B:  {A, B, Na, Kab, Kt}Kas, {A, B, Na, Kab, Kt}Kbs
--B->A:  {A, B, Na, Kab}Kas, {Na, Kab}Kt, Nb -- Purpose of Nb?
--A->B:  {Na, Kab}Kt -- Switch Nb for Na?  Brackin does. in empaapa2.pdf

-- For Kao Chow Two and Three, there doesn't appear to be
-- any authentication of A to B
-- Example Attack:
-- Masquerading as S the attacker replays msg2.1 and sends to B as msg2.2
-- Masquerading as A, the attacker replays msg4.1 and sends to B as msg4.2
-- msgX.Y = the xth message in the Yth session
-- A is not authenticated, And if session key was broken from this session
-- Attacker could impersonate A in subsequent messages.

X: assume(S.Kas == A.Kas);
X: assume(S.Kbs == B.Kbs);

-- START
A: => S(<A, B, Na>);
S: <-(msg1);
S: (A, B, Na) := msg1;

S: => B(<e[<A, B, Na, Kab, Kt>]Kas, e[<A, B, Na, Kab, Kt>]Kbs>);
B: <-(msg2);
B: (tickAS, tickBS) := msg2;
B: (A, B, Na, Kab, Kt) := d[tickBS]Kbs;

B: => A(<tickAS, e[<Na, Kab>]Kt, Nb>);
A: <-(msg3);
A: (tickAS, chalA, Nb) := msg3;
A: (A', B', Na', Kab, Kt) := d[tickAS]Kas;
A: assert(<A, B, Na> == <A', B', Na'>);
A: (Na'', Kab) := d[chalA]Kt;
A: assert(Na == Na'');

A: => B(e[<Na, Kab>]Kt);
B: <-(msg4);
B: Na_Kab := d[msg4]Kt;
B: assert(Na_Kab ==  <Na, Kab>);
 
--           Three (tickets)
--A->S:  A, B, Na
--S->B:  {A, B, Na, Kab, Kt}Kas, {A, B, Na, Kab, Kt}Kbs
--B->A:  {A, B, Na, Kab}Kas, {Na, Kab}Kt, Nb, {A, B, Ta, Kab}Kbs
--A->B:  {Na, Kab}Kt, {A, B, Ta, Kab}Kbs
 
X: assume(S.Kas == A.Kas);
X: assume(S.Kbs == B.Kbs);

-- START
A: => S(<A, B, Na>);
S: <-(msg1);
S: (A, B, Na) := msg1;

S: => B(<e[<A, B, Na, Kab, Kt>]Kas, e[<A, B, Na, Kab, Kt>]Kbs>);
B: <-(msg2);
B: (tickAS, tickBS) := msg2;
B: (A, B, Na, Kab, Kt) := d[tickBS]Kbs;

B: => A(<tickAS, e[<Na, Kab>]Kt, Nb, e[<A, B, Ta, Kab>]Kbs>);
A: <-(msg3);
A: (tickAS, chalA, Nb, thttp://www.arca.com/proj_papers/brackin/Empaapa2.pdfickBS) := msg3;
A: (A', B', Na', Kab, Kt) := d[tickAS]Kas;
A: assert(<A, B, Na> == <A', B', Na'>);
A: (Na'', Kab) := d[chalA]Kt;
A: assert(Na == Na'');

A: => B(<chalA, tickBS>);
B: <-(msg4);
B: (Na_Kab, tickBS) := d[msg4]Kt;
B: assert(Na_Kab ==  <Na, Kab>);
B: (A'', B'', Ta, Kab') := d[tickBS]Kbs;
B: assert(<A, B, Kab> == <A'', B'', Kab'>);

--6.6         Public Key Protocols without Trusted Third Party
 
--6.6.1        ISO Public Key One-Pass Unilateral Authentication Protocol
 
--A->B:  CertA, [Ta|Na], B, txt2, {[Ta|Na], B, txt1}Ka-1

X: assume(global.decrypt(CA.Ka+, A.Ka-));
X: assume(global.decrypt(B.Kca+, CA.Kca-));

-- Na is a sequence number, i.e. state must be kept between sessions.
-- A timestamp would be vulnerable to repeated authentications
-- i.e. replay of recently sent authentication

--Pre Protocol
CA: => A(ep[<A, Ka+>]Kca-);
A: <-(certA);

--Protocol Start
A: => B(<certA, Na, B, txt2, ep[<Na, B, txt1>]Ka->);
B: <-(msg);
B: (certA, Na, B, txt2, sigA) := msg;
B: (A, Ka+) := dp[certA]Kca+;
B: (Na', B', txt1) := dp[sigA]Ka+;
B: assert(<Na, B> == <Na', B'>);

--6.6.2        ISO Public Key Two-Pass Unilateral Authentication Protocol
 
--B->A:  Rb, txt1
--A->B:  CertA, Ra, Rb, B, txt3, {Ra, Rb, B, txt2}Ka-1

-- What is purpose of Ra sent by A?
-- Ra seems pointless, however, used in later protocol.

X: assume(global.decrypt(CA.Ka+, A.Ka-));
X: assume(global.decrypt(B.Kca+, CA.Kca-));

--Pre Protocol
CA: => A(ep[<A, Ka+>]Kca-);
A: <-(certA);

-- Protocol Start
B: => A(<Rb, txt1>);
A: <-(msg1);
A: (Rb, txt1) := msg1;

A: => B(<certA, Ra, Rb, B, txt3, ep[<Ra, Rb, B, txt2>]Ka->);
B: <-(msg);
B: (certA, Ra, Rb', B, txt3, sigA) := msg;
B: assert(Rb == Rb');
B: (A, Ka+) := dp[certA]Kca+;
B: (Ra', Rb'', B', txt2) := dp[sigA]Ka+;
B: assert(<Ra, Rb, B> == <Ra', Rb'', B'>);
 
--6.6.3        ISO Public Key Two-Pass Mutual Authentication Protocol
 
--A->B:  CertA, [Ta|Na], B, txt2, {[Ta|Na], B, txt1}Ka-1
--B->A:  CertB,[Tb|Nb], A, txt4, {[Tb|Nb], A, txt3}Kb-1
 
--Note:  two above messages disjoint
 
X: assume(global.decrypt(CA.Ka+, A.Ka-));
X: assume(global.decrypt(B.Kca+, CA.Kca-));
X: assume(global.decrypt(CA.Kb+, B.Kb-));
X: assume(global.decrypt(A.Kca+, CA.Kca-));

-- Na is a sequence number.

--Pre Protocol
CA: => A(ep[<A, Ka+>]Kca-);
A: <-(certA);
CA: => B(ep[<B, Kb+>]Kca-);
B: <-(certB);

--Protocol Start
A: => B(<certA, Na, B, txt2, ep[<Na, B, txt1>]Ka->);
B: <-(msg1);
B: (certA, Na, B, txt2, sigA) := msg1;
B: (A, Ka+) := dp[certA]Kca+;
B: (Na', B', txt1) := dp[sigA]Ka+;
B: assert(<Na, B> == <Na', B'>);

--Protocol Start
B: => A(<certB, Nb, A, txt4, ep[<Nb, A, txt3>]Kb->);
A: <-(msg2);
A: (certB, Nb, A, txt4, sigB) := msg2;
A: (B, Kb+) := dp[certB]Kca+;
A: (Nb', A', txt3) := dp[sigB]Kb+;
A: assert(<Nb, A> == <Nb', A'>);

--6.6.4        ISO Three-Pass Mutual Authentication Protocol
 
--B->A:  Rb, txt1
--A->B:  CertA, Ra, Rb, B, txt3, {Ra, Rb, B, txt2}Ka-1
--B->A:  CertB, Rb, Ra, A, txt5, {Rb, Ra, A, txt4}Kb-1

X: assume(global.decrypt(CA.Ka+, A.Ka-));
X: assume(global.decrypt(B.Kca+, CA.Kca-));
X: assume(global.decrypt(CA.Kb+, B.Kb-));
X: assume(global.decrypt(A.Kca+, CA.Kca-));

--Pre Protocol
CA: => A(ep[<A, Ka+>]Kca-); -- distribute certificates
A: <-(certA);
A: (A, Ka+) := dp[certA]Kca+;
CA: => B(ep[<B, Kb+>]Kca-);
B: <-(certB);
B: (B, Kb+) := dp[certB]Kca+;
CA: => A(ep[<B, Kb+>]Kca-); -- distribute identities, B exempt since it
A: <-(certB);               -- receives certA before it uses.
A: (B, Kb+) := dp[certB]Kca+;

-- Protocol Start
B: => A(<Rb, txt1>);
A: <-(msg1);
A: (Rb, txt1) := msg1;

A: => B(<certA, Ra, Rb, B, txt3, ep[<Ra, Rb, B, txt2>]Ka->);
B: <-(msg);
B: (certA, Ra, Rb', B, txt3, sigA) := msg;
B: assert(Rb == Rb');http://www.arca.com/proj_papers/brackin/Empaapa2.pdf
B: (A, Ka+) := dp[certA]Kca+;
B: (Ra', Rb'', B', txt2) := dp[sigA]Ka+;
B: assert(<Ra, Rb, B> == <Ra', Rb'', B'>);

B: => A(<certB, Rb, Ra, A, txt5, ep[<Rb, Ra, A, txt4>]Kb->);
A: <-(msg2);
A: (certB, Rb', Ra', A, txt3, sigB) := msg2;
A: assert(<Ra, Rb> == <Ra', Rb'>);
A: (B', Kb+) := dp[certB]Kca+;
A: (Rb'', Ra'', A', txt2) := dp[sigB]Kb+;
A: assert(<Rb, Ra, A, B> == <Rb'', Ra'', A', B'>);
 
--6.6.5        ISO Two Pass Parallel Mutual Authentication Protocol
 
--A->B:  CertA, Ra, txt1
--B->A:  CertB, Rb, txt2
--B->A:  Rb, Ra, A, txt6, {Rb, Ra, A, txt5}Kb-1
--A->B:  Ra, Rb, B, txt4, {Ra, Rb, B, txt3}Ka-1
 

X: assume(global.decrypt(CA.Ka+, A.Ka-));
X: assume(global.decrypt(B.Kca+, CA.Kca-));
X: assume(global.decrypt(CA.Kb+, B.Kb-));
X: assume(global.decrypt(A.Kca+, CA.Kca-));

--Pre Protocol
CA: => A(ep[<A, Ka+>]Kca-);
A: <-(certA);
A: (A, Ka+) := dp[certA]Kca+;
CA: => B(ep[<B, Kb+>]Kca-);
B: <-(certB);
B: (B, Kb+) := dp[certB]Kca+;

-- Protocol Start
A: => B(<certA, Ra, txt1>);
B: <-(msg1);http://www.arca.com/proj_papers/brackin/Empaapa2.pdf
B: (certA, Ra, txt1) := msg1;
B: (A, Ka+) := dp[certA]Kca+;

B: => A(<certB, Rb, txt2>);
A: <-(msg2);
A: (certB, Rb, txt2) := msg2;
A: (B, Kb+) := dp[certB]Kca+;

B: => A(<Rb, Ra, A, txt6, ep[<Rb, Ra, A, txt5>]Kb->);
A: <-(msg3);
A: (Rb', Ra', A', txt6, sigB) := msg3;
A: assert(<A, Ra, Rb> == <A', Ra', Rb'>);
A: (Rb'', Ra'', A'', txt5) := dp[sigB]Kb+;
A: assert(<A, Ra, Rb> == <A'', Ra'', Rb''>);

A: => B(<Ra, Rb, B, txt4, ep[<Ra, Rb, B, txt3>]Ka->);
B: <-(msg4);
B: (Ra', Rb', B', txt4, sigA) := msg4;
B: assert(<B, Ra, Rb> == <B', Ra', Rb'>);
B: (Ra'', Rb'', B'', txt3) := dp[sigA]Ka+;
B: assert(<B, Ra, Rb> == <B'', Ra'', Rb''>);

--6.6.6        Bilateral Key Exchange with Public Key
 
--B->A:  B, {Nb, B}Ka+
--A->B:  {f(Nb), Na, A, K}Kb+
--B->A:  {f(Na)}K
 
--Question: What is the purpose of f()?  We'll try to attack without it,
--and maybe we can find out.
 
X: assume(global.decrypt(A.Ka-, B.Ka+));
X: assume(global.decrypt(B.Kb-, A.Kb+));

B: => A(<B, ep[<Nb, B>]Ka+>);
A: <-(msg1);
A: (B, sigB) := msg1;
A: (Nb, B) := dp[sigB]Ka-;

A: => B(ep[<f(Nb), Na, A, K>]Kb+);
B: <-(msg2);
B: (fNb, Na, A, K) := dp[msg2]Kb-;
B: check := f(Nb);
B: assert(fNb == check);  -- What does it mean if A is not checked? 
                          -- i.e. What purpose does A serve?

B: => A(e[f(Na)]K);
A: <-(msg3);
A: fNa := d[msg3]K;
A: check := f(Na);
A: assert(fNa == check);

--6.6.7        Diffie Hellman Exchange
 
--A->B:  X = GX modN
--B->A:  Y = GY modN
 
--Note:  No guarantee of authenticity
X: assume(A.p == B.p);
X: assume(A.g == B.g);

A: => B(f(p, g, x));
B: <-(Ya);

B: => A(f(p, g, y));
A: <-(Yb);

B: K := f(p, g, Ya, y);
A: K := f(p, g, Yb, x);

X: gassert(A.K == B.K);
 
--6.7         Public Key Protocols with Trusted Third Party
 
--6.7.1        Needham-Schroeder Public Key Protocol*
 
--A->S:  A, B
--S->A:  {Kb, B}Ks-1
--A->B:  {Na, A}Kb
--B->S:  B, A
--S->B:  {Ka, A}Ks-1
--B->A:  {Na, Nb}Ka
--A->B:  {Nb}Kb
 
--6.8          SPLICE/AS Authentication Protocol*
 
--C->AS:  C, S, N1
--AS->C:  AS, {AS, C, N1, Ks}Kas-1
--C->S:  C, S, {C, T, L, {N2}Ks}Kc-1
--S->AS:  S, C, N3
--AS->S:  AS, {AS, S, N3, Kc}Kas-1
--S->C:  S, C, {S, N2+1}Kc 

X: assume(global.decrypt(C.Kas+, AS.Kas-)); -- pk verify, sign
X: assume(global.decrypt(S.Kas+, AS.Kas-));
X: assume(global.decrypt(AS.Kc+, C.Kc-));
X: assume(global.decrypt(C.Kc-, AS.Kc+)); -- pk decrypt, encrypt
X: assume(global.decrypt(S.Ks-, AS.Ks+));

C: => AS(<C, S, N1>);
AS: <-(msg1);
AS: (C, S, N1) := msg1;

AS: => C(<AS, ep[<AS, C, N1, Ks+>]Kas->);
C: <-(msg2);
C: (AS, tickAS) := msg2;
C: (AS', C', N1', Ks+) := dp[tickAS]Kas+;
C: assert(<AS, C, N1> == <AS', C', N1'>);

C: => S(<C, S, ep[<C, T, L, ep[N2]Ks+>]Kc->);
S: <-(msg3);
S: (C, S, sigC) := msg3;

S: => AS(<S, C, N3>);
AS: <-(msg4);
AS: (S', C', N3) := msg4;
AS: assert(<S, C> == <S', C'>);

AS: => S(<AS, ep[<AS, S, N3, Kc+>]Kas->);
S: <-(msg5);
S: (AS, sigAS) := msg5;
S: (AS', S', N3', Kc+) := dp[sigAS]Kas+;
S: assert(<AS, S, N3> == <AS', S', N3'>);
S: (C', T, L, encS) := dp[sigC]Kc+;
S: assert(C == C');
S: N2 := dp[encS]Ks-;

S: => C(<S, C, ep[<S, f(N2)>]Kc+>);
C: <-(msg6);
C: (S'', C'', encC) := msg6;
C: assert(<C, S> == <C'', S''>);
C: (S''', fN2) := dp[encC]Kc-;
C: assert(S == S''');
C: check := f(N2);
C: assert(fN2 == check);
 
--6.8.1        Hwang and Chen's Modified SPLICE/AS*
 
--C->AS:  C, S, N1
--AS->C:  AS, {AS, C, N1, S, Ks}Kas-1
--C->S:  C, S, {C, T, L, {N2}Ks}Kc-1
--S->AS:  S, C, N3
--AS->S:  AS, {AS, S, N3, C, Kc}Kas-1
--S->C:  S, C, {S, N2+1}Kc

X: assume(global.decrypt(C.Kas+, AS.Kas-)); -- pk verify, sign
X: assume(global.decrypt(S.Kas+, AS.Kas-));
X: assume(global.decrypt(AS.Kc+, C.Kc-));
X: assume(global.decrypt(C.Kc-, AS.Kc+)); -- pk decrypt, encrypt
X: assume(global.decrypt(S.Ks-, AS.Ks+));

C: => AS(<C, S, N1>);
AS: <-(msg1);
AS: (C, S, N1) := msg1;

AS: => C(<AS, ep[<AS, C, N1, S, Ks+>]Kas->);
C: <-(msg2);
C: (AS, tickAS) := msg2;
C: (AS', C', N1', S', Ks+) := dp[tickAS]Kas+;
C: assert(<AS, C, S, N1> == <AS', C', S', N1'>);

C: => S(<C, S, ep[<C, T, L, ep[N2]Ks+>]Kc->);
S: <-(msg3);
S: (C, S, sigC) := msg3;

S: => AS(<S, C, N3>);
AS: <-(msg4);
AS: (S', C', N3) := msg4;
AS: assert(<S, C> == <S', C'>);

AS: => S(<AS, ep[<AS, S, N3, C, Kc+>]Kas->);
S: <-(msg5);
S: (AS, sigAS) := msg5;
S: (AS', S', N3', C', Kc+) := dp[sigAS]Kas+;
S: assert(<AS, S, C, N3> == <AS', S', C', N3'>);
S: (C', T, L, encS) := dp[sigC]Kc+;
S: assert(C == C');
S: N2 := dp[encS]Ks-;

S: => C(<S, C, ep[<S, f(N2)>]Kc+>);
C: <-(msg6);
C: (S'', C'', encC) := msg6;
C: assert(<C, S> == <C'', S''>);
C: (S''', fN2) := dp[encC]Kc-;
C: assert(S == S''');
C: check := f(N2);
C: assert(fN2 == check);
 
--6.9          Denning Sacco Key Distribution with Public Key*
 
--A->S:  A, B
--S->A:  CertA, CertB
--A->B:  CertA, CertB, {{Kab, Ta}Ka-1)Kb

X: assume(global.decrypt(A.Ks+, S.Ks-));
X: assume(global.decrypt(B.Ks+, S.Ks-));

A: => S(<A, B>)
S: <-(msg1);
S: (A, B) := msg1;

S: => A(<ep[<A, Ka+>]Ks-, ep[<B, Kb+>]Ks->);
A: <-(msg2);
A: (certA, certB) := msg2;
A: (B', Kb+) := dp[certB]Ks+;
A: assert(B == B');

A: => B(<certA, certB, ep[ep[<Kab, Ta>]Ka-]Kb+>);
B: <-(msg3);
B: (certA, certB, encB) := msg3;
B: (A, Ka+) := dp[certA]Ks+;
B: sigA := dp[encB]Kb-;
B: (Kab, Ta) := dp[sigA]Ka+;
 
--6.9.1        CCITT X.509*
 
--A->B:  A, {Ta, Na, B, Xa, {Ya}Kb}Ka-1
--B->A:  B, {Tb, Nb, A, Na, Xb, {Yb}Ka}Kb-1
--A->B:  A, {Nb}Ka-1
 
--Problem: signing after encryption

X: assume(global.decrypt(B.Ka+, A.Ka-));
X: assume(global.decrypt(A.Kb+, B.Kb-));

A: => B(<A, ep[<Ta, Na, B, Xa, ep[Ya]Kb>]Ka->);
B: <-(msg1);
B: (A, sigA) := msg1;
B: (Ta, Na, B, Xa, encB) := dp[sigA]Ka+;
B: Ya := dp[encB]Kb-;

B: => A(<B, ep[<Tb, Nb, A, Na, Xb, ep[Yb]Ka+>]Kb->);
A: <-(msg2);
A: (B', sigB) := msg2;
A: (Tb, Nb, A', Na', Xb, encA) := dp[sigB]Kb+;
A: assert(<A, Na> == <A', Na'>);
A: Yb := dp[encA]Ka-;

A: => B(<A, ep[Nb]Ka->);
B: <-(msg3);
B: (A, sigA') := msg3;
B: Nb' := dp[sigA']Ka+;
B: assert(Nb == Nb');
 
--6.10        Miscellaneous
 
--6.10.1    Shamir Rivest Adelman Three Pass Protocol*
 
--A->B:  {M}Ka
--B->A:  {{M}Ka}Kb
--A->B:  {M}Kb
 
-- No secrets known between principals before protocol starts. 
-- Assumes encryption commutative. i.e. -> d[e[e[x]Ka]Kb]Ka == e[x]Kb

-- I really don't understand this protocol.  Why can't an intruder
-- just take the first message and apply his own key.
-- This should allow the production of a message the intruder can
-- decrypt unless Kb and Ka have a special relationship.

-- Anyway, CPALES doesn't model commutative encryption.

A: => B(e[m]Ka);
B: <-(msg1);

B: => A(e[msg1]Kb);
A: <-(msg2);

A: => B(d[msg2]Ka);
B: <-(msg3);
B: m := d[msg3]Kb;

X: gassert(B.m == A.m);

--6.10.2    Gong Mutual Authentication Protocol
 
--Pa                   secret shared between A and A
--(k, Ha, Hb)          hash(Ns, Na, B, Pa), 
--hash(Ns, Nb, A, Pb)  B xors with 2nd field of message 2 to get (K, Ha, Hb)
--k                    a secret to be shared between clients
--Ha, Hb               handshake numbers
 
--A->B:  A, B, Na
--B->S:  A, B, Na, Nb
--S->B:  Ns, hash(Ns, Nb, A, Pb) xor (K, Ha, Hb), hash(k, Ha, Hb, Pb)
--B->A:  Ns, Hb
--A->B:  Ha
 

--6.10.3    Encrypted Key Exchange - EKE*
 
--P          Password
--R          Randomly generated session key
 
--A->B:  {Ka}P
--B->A:  {{R}Ka}P
--A->B:  {Na}R
--B->A:  {Na, Nb}R
--A->B:  {Nb}R
 
 
-- Note: To analyze a password protocol you must also look at the
-- weakness of P.  That is, P is subject to brute force attack If it is
-- used to encrypt a value that is not random, it can be determined.
-- * Clark Jacob Attack seems to be based upon A accepting password for key
-- exchange.  Does this fit a client server model?

X: assume(A.P == B.P);

A: => B(e[Ka]P);
B: <-(msg1);
B: Ka := d[msg1]P;

B: => A(e[e[R]Ka]P);
A: <-(msg2);
A: R := d[d[msg2]P]Ka;

A: => B(e[Na]R);
B: <-(msg3);
B: Na := d[msg3]R;

B: => A(e[<Na, Nb>]R);
A: <-(msg4);
A: (Na', Nb) := d[msg4]R;
A: assert(Na == Na');

A: => B(e[Nb]R);
B: <-(msg5);
B: Nb' := d[msg5]R;
B: assert(Nb == Nb');
 
--6.10.4    Davis Swick Private Key Certificates*
 
--      One* 
--B->A:  {A, msg}Kbt
--A->T:  {A, msg}Kbt, B
--T->A:  {msg, B}Kat

X: assume(A.Kat == T.Kat);
X: assume(B.Kbt == T.Kbt);

B: => A(e[<A, m>]Kbt);
A: <-(certB);

A: => T(<msg1, B>);
T: <-(certB);
T: (certB, B) := msg2;
T: (A, m) := d[certB]Kbt;

T: => A(e[<m, B>]Kat);
A: <-(msg3);
A: (m, B') := d[msg3]Kat;
A: assert(B == B');

--            Three
--B->T:  {Kbt, B, Lb}Kt
--T->B:  {K'bt, B, L'b}Kt, {K'bt, T, L'b, checksum}Kbt

X: assume(B.Kbt == T.Kbt);

-- Pre Protocol Setup
T: => B(e[<Kbt, B, Lb>]Kt);
B: <-(certB);

-- Start of Protocol
B: => T(certB);
T: <-(certB);
T: (Kbt, B, Lb) := d[certB]Kt;  -- assume T doesn't hold certificates

T: => B(<e[<K'bt, B, L'b>]Kt, e[<K'bt, T, L'b, checksum>]Kbt>);
B: <-(msg2);
B: (newCertB, encKey) := msg2;
B: (K'bt, T, L'b, checksum) := d[encKey]Kbt;

X: gassert(T.K'bt == B.K'bt);
 
--            Four
--A->T:  {Kat, A, La}Kt, {Kbt, B, Lb}Kt
--T->A:  {Kab, A, Lab}Kbt, {Kab, B, Lab, checksum}Kat
--A->B:  {msg, A}Kab, {Kab, A, Lab}Kbt

X: assume(B.Kbt == T.Kbt);
X: assume(A.Kat == T.Kat);
X: assume(T.B == A.B);
X: assume(T.A == A.A);

-- Pre Protocol Setup
T: => A(<e[<Kat, A, La>]Kt, e[<Kbt, B, Lb>]Kt>);
A: <-(premsg);
A: (certA, certB) := premsg;

-- Start of Protocol
A: => T(<certA, certB>);
T: <-(msg1);
T: (certA, certB) := msg1;
T: (Kat, A, La) := d[certA]Kt;
T: (Kbt, B, Lb) := d[certB]Kt;

T: => A(<e[<Kab, A, Lab>]Kbt, e[<Kab, B, Lab, checksum>]Kat>);
A: <-(msg2);
A: (certB, newKey) := msg2;
A: (Kab, B', Lab, checksum) := d[newKey]Kat;
A: assert(B == B');

A: => B(<e[<m, A>]Kab, certB>);
B: <-(msg3);
B: (encMsg, certB) := msg3;
B: (Kab, A, Lab) := d[certB]Kbt;
B: (m, A') := d[encMsg]Kab;
B: assert(A == A');

X: gassert(A.m == B.m);