Thanks to Clóvis Freire Júnior of the University of Brasilia, we have a CAPSL version of the Clark-Jacob compendium of authentication protocols. The Clark-Jacob library is Section 6 of a document by John Clark and Jeremy Jacob, "A Survey of Authentication Protocol Literature: Version 1.0", 1997, posted at the University of York on the Secure Network page under the link Security Protocols Review. There is also an online security protocol library that includes this collection, at ENS Cachan, due to Comon: SPORE, the Security Protocols Open REpository.
Clovis' version of the Clark-Jacob library (which did not have 6.10.1 and 6.10.2) has been edited somewhat to ensure that the CAPSL usage is up to date. Corrections regarding the content and intent of these protocols are welcome.
The protocols implicitly make use of some new typespecs that now appear in the prelude: a symmetric-key client/server type SKCS and a mutual symmetric key node type MSKN.
A goal PRECEDES A: B | X, Y means that in B's last state, if a "B"-agent for B holds A, X, and Y, then there is or was an "A"-agent for A holding the same values of B, X, and Y. (This is a form of Schneider's "precedes" property, and it corresponds also to a form of Lowe's "agreement.")
/**************************************************************
6.1.1 ISO Symmetric Key One-Pass Unilateral Authentication */
/* Na could be a timestamp instead. */
PROTOCOL ISOSK1PU;
VARIABLES
A, B : Node;
Text2: Field;
Text1: Field;
Na: Nonce;
Kab: Skey;
DENOTES
Kab = msk(A,B): A;
Kab = msk(B,A): B;
ASSUMPTIONS
HOLDS A: B, Text2, Text1;
MESSAGES
1. A -> B: A, Text2, {Na, B, Text1}Kab;
GOALS
PRECEDES A: B | Na, Text1;
END;
/**************************************************************
6.1.2 ISO Symmetric Key Two Pass Unilateral Authentication */
PROTOCOL ISOSK2PU;
VARIABLES
A, B: Node;
Text1, Text2, Text3: Field;
Rb: Nonce;
Kab: Skey;
DENOTES
Kab = msk(A,B): A;
Kab = msk(B,A): B;
ASSUMPTIONS
HOLDS A: Text2, Text3;
HOLDS B: A,Text1;
MESSAGES
1. B -> A: B, Rb, Text1;
2. A -> B: Text3, {Rb, B, Text2}Kab;
GOALS
PRECEDES A: B | Rb,Text2;
END;
/**************************************************************
6.1.3 ISO Symmetric Key Two Pass Mutual Authentication */
/* Na and Nb could be timestamps. */
PROTOCOL ISOSK2PM;
VARIABLES
A, B: Node;
Text1, Text2, Text3, Text4: Field;
Na, Nb: Nonce;
Kab: Skey;
DENOTES
Kab = msk(A,B): A;
Kab = msk(B,A): B;
ASSUMPTIONS
HOLDS A: B, Text2, Text1;
HOLDS B: Text3, Text4;
MESSAGES
1. A -> B: A, Text2, {Na, B, Text1}Kab;
2. B -> A: Text4, {Nb, A, Text3}Kab;
GOALS
PRECEDES A: B | Na, Text1;
PRECEDES B: A | Nb, Text3;
END;
/**************************************************************
6.1.4 ISO Symmetric Key Three Pass Mutual Authentication */
PROTOCOL ISOSK3PM;
VARIABLES
A, B: Node;
Text1, Text2, Text3, Text4, Text5: Field;
Ra, Rb: Nonce;
Kab: Skey;
DENOTES
Kab = msk(A,B): A;
Kab = msk(B,A): B;
ASSUMPTIONS
HOLDS A: Text2, Text3;
HOLDS B: A, Text1, Text4, Text5;
MESSAGES
1. B -> A: B, Rb, Text1;
2. A -> B: Text3, {Ra, Rb, B, Text2}Kab;
3. B -> A: Text5, {Rb, Ra, Text4}Kab;
GOALS
SECRET Ra;
PRECEDES A: B | Ra, Rb, Text2;
PRECEDES B: A | Ra, Rb, Text4;
END;
/**************************************************************
6.1.5 Using Non-Reversible Functions */
PROTOCOL NRF;
VARIABLES
A, B: Node;
Ra, Rb: Nonce;
K: Skey, CRYPTO, FRESH;
Kab: Skey;
DENOTES
Kab = msk(A,B): A;
Kab = msk(B,A): B;
ASSUMPTIONS
HOLDS B: A;
MESSAGES
1. B -> A: B, Rb;
2. A -> B: A, {sha(Rb), Ra, A, K}Kab;
3. B -> A: B, {sha(Ra)}K;
GOALS
SECRET K;
PRECEDES A: B | Rb, Ra, K;
PRECEDES B: A | Rb, Ra, K;
END;
/**************************************************************
6.1.6 Andrew Secure RPC */
/* Attack: Message 4 can be replayed. There is also a parallel
session attack. */
PROTOCOL AndrewRPC;
VARIABLES
A, B: Node;
Kab : Skey;
Na, Nb, N_b : Skey, FRESH;
K_ab : Skey, CRYPTO, FRESH;
DENOTES
Kab = msk(A,B): A;
Kab = msk(B,A): B;
ASSUMPTIONS
HOLDS A: B;
MESSAGES
1. A -> B: A, {Na}Kab;
2. B -> A: {Na+1, Nb}Kab;
3. A -> B: {Nb+1}Kab;
4. B -> A: {K_ab, N_b}Kab;
GOALS
SECRET K_ab;
PRECEDES B: A | Na, Nb, K_ab, N_b;
PRECEDES A: B | Na, Nb;
END;
/**************************************************************
6.2.1 ISO One Pass Unilateral Authentication with CCFs */
PROTOCOL ISO1PUCCF;
VARIABLES
A, B : Node;
Na : Nonce;
Text1, Text2 : Field;
Kab : Skey;
DENOTES
Kab = msk(A,B): A;
Kab = msk(B,A): B;
ASSUMPTIONS
HOLDS A: B, Text2, Text1;
HOLDS B: Text1;
MESSAGES
1. A -> B: A, Na, B, Text2, mac(Kab,{Na, B, Text1});
GOALS
PRECEDES A: B | Na, Text1;
END;
/**************************************************************
6.2.2 ISO Two Pass Unilateral Authentication with CCFs */
PROTOCOL ISO2PUCCF;
VARIABLES
A, B: Node;
Rb : Nonce;
Text1, Text2, Text3 : Field;
Kab: Skey;
DENOTES
Kab = msk(A,B): A;
Kab = msk(B,A): B;
ASSUMPTIONS
HOLDS B: A, Text1, Text2;
HOLDS A: Text3, Text2;
MESSAGES
1. B -> A: B, Rb, Text1;
2. A -> B: Text3, mac(Kab,{Rb, B, Text2});
GOALS
PRECEDES A: B | Rb, Text2;
END;
/**************************************************************
6.2.3 ISO Two Pass Mutual Authentication with CCFs */
PROTOCOL ISO2PMCCF;
VARIABLES
A, B: Node;
Na, Nb : Nonce;
Text1, Text2, Text3, Text4 : Field;
Kab: Skey;
DENOTES
Kab = msk(A,B): A;
Kab = msk(B,A): B;
ASSUMPTIONS
HOLDS A: Text2, Text1, Text3, B;
HOLDS B: Text4, Text3, Text1;
MESSAGES
1. A -> B: A, Na, Text2, mac(Kab,{Na, B, Text1});
2. B -> A: Nb, Text4, mac(Kab,{Nb, A, Text3});
GOALS
PRECEDES A: B | Na, Text1 ;
PRECEDES B: A | Nb, Text3;
END;
/**************************************************************
6.2.4 - ISO Three Pass Mutual Authentication with CCFs */
PROTOCOL ISO3PMCCF;
VARIABLES
A, B: Node;
Ra, Rb : Nonce;
Text1, Text2, Text3, Text4, Text5 : Field;
Kab: Skey;
DENOTES
Kab = msk(A,B): A;
Kab = msk(B,A): B;
ASSUMPTIONS
HOLDS B: A, Text1, Text2, Text5, Text4;
HOLDS A: Text3, Text2, Text4;
MESSAGES
1. B -> A: B, Rb, Text1;
2. A -> B: Ra, Text3, mac(Kab,{Ra, Rb, B, Text2});
3. B -> A: Text5, mac(Kab,{Ra, Ra, Text4});
GOALS
PRECEDES A: B | Ra, Rb, Text2;
PRECEDES B: A | Ra, Rb, Text4;
END;
/**************************************************************
6.3.1 Needham-Schroeder Protocol with Conventional Keys */
/* Attack: Replay of message 3 to insert old compromised Kab. */
PROTOCOL NSSK;
VARIABLES
S : Server;
A, B : Client;
Na: Nonce;
Nb: Skey, FRESH;
Kab : Skey, CRYPTO, FRESH;
F : Field;
Kas: Skey;
DENOTES
Kas = csk(A): A;
Kas = ssk(S,A): S;
ASSUMPTIONS
HOLDS A: B, S;
MESSAGES
1. A -> S: A, B, Na;
2. S -> A: {Na, B, Kab, {Kab, A}ssk(S,B)%F}Kas;
3. A -> B: F%{Kab, A}csk(B);
4. B -> A: {Nb}Kab;
5. A -> B: {Nb-1}Kab;
GOALS
SECRET Kab;
PRECEDES B: A | Nb, Kab;
END;
/**************************************************************
6.3.2 Denning-Sacco */
PROTOCOL DenningSacco;
VARIABLES
S: Server;
A, B: Client;
Tm : Timestamp;
Kab : Skey, CRYPTO, FRESH;
F : Field;
Kas, Kbs: Skey;
DENOTES
Kas = csk(A): A;
Kas = ssk(S,A): S;
Kbs = csk(B): B;
Kbs = ssk(S,B): S;
ASSUMPTIONS
HOLDS A: B, S, Tm;
HOLDS S: Tm;
HOLDS B: Tm;
MESSAGES
1. A -> S: A, B;
2. S -> A: {B, Kab, Tm, {A, Kab, Tm}Kbs%F}Kas;
3. A -> B: F%{A, Kab, Tm}Kbs;
GOALS
SECRET Kab;
PRECEDES S: A | Tm, Kab;
PRECEDES A: B | Tm, Kab;
END;
/**************************************************************
6.3.3 Otway-Rees */
/* Attack: Type flaw if F1 can be substituted for F2
to replace Kab by {M,A,B}. */
PROTOCOL OtwayRees;
VARIABLES
S: Server;
A, B: Client;
M : Nonce;
Na, Nb : Nonce, CRYPTO;
Kab : Skey, CRYPTO, FRESH;
F1, F2 : Field;
Kbs,Kas: Skey;
DENOTES
Kbs = csk(B): B;
Kbs = ssk(S,B): S;
Kas = csk(A): A;
Kas = ssk(S,A): S;
ASSUMPTIONS
HOLDS A: B;
HOLDS B: S;
MESSAGES
1. A -> B: M, A, B, {Na, M, A, B}Kas%F1 ;
2. B -> S: M, A, B, F1%{Na, M, A, B}Kas, {Nb, M, A, B}Kbs;
3. S -> B: M, {Na, Kab}Kas%F2, {Nb, Kab}Kbs;
4. B -> A: M, F2%{Na, Kab}Kas;
GOALS
SECRET Kab;
PRECEDES S: B | Nb, Kab;
PRECEDES S: A | Na, Kab;
END;
/**************************************************************
6.3.4 Amended Needham-Schroeder */
PROTOCOL ANSSK;
VARIABLES
S : Server;
A, B: Client;
Na, Nb0 : Nonce;
Nb : Skey, FRESH;
Kab : Skey, CRYPTO, FRESH;
Kas, Kbs : Skey;
F1, F2 : Field;
DENOTES
Kas = csk(A): A;
Kas = ssk(S,A): S;
Kbs = csk(B): B;
Kbs = ssk(S,B): S;
ASSUMPTIONS
HOLDS A: B, S;
HOLDS B: Nb;
MESSAGES
1. A -> B: A;
2. B -> A: {A, Nb0}Kbs%F1;
3. A -> S: A, B, Na, F1%{A, Nb0}Kbs;
4. S -> A: {Na, B, Kab, {Kab, Nb0, A}Kbs%F2}Kas;
5. A -> B: F2%{Kab, Nb0, A}Kbs;
6. B -> A: {Nb}Kab;
7. A -> B: {Nb-1}Kab;
GOALS
SECRET Kab;
PRECEDES B: A | Nb, Kab;
PRECEDES A: B | Nb, Kab;
END;
/**************************************************************
6.3.5 Wide Mouthed Frog */
/* Attack: Take advantage of tolerance in timestamps
to cause re-authentication in a false session. */
PROTOCOL WideMouthedFrog;
VARIABLES
S : Server;
A, B : Client;
Ta, Ts : Timestamp;
Kab : Skey, CRYPTO, FRESH;
Kas, Kbs: Skey;
DENOTES
Kas = csk(A): A;
Kas = ssk(S,A): S;
Kbs = csk(B): B;
Kbs = ssk(S,B): S;
ASSUMPTIONS
HOLDS A: Ta, B, S;
HOLDS S: Ta, Ts;
HOLDS B: Ts;
MESSAGES
1. A -> S: A, {Ta, B, Kab}Kas;
2. S -> B: {Ts, A, Kab}Kbs;
GOALS
SECRET Kab;
PRECEDES S: B | Ts, A, Kab;
PRECEDES A: S | Ta, B, Kab;
END;
/**************************************************************
6.3.6 Yahalom */
/* Attack: Type flaw in which {Na, Nb} can be substituted
for Kab by using message 2 to modify message 4. */
PROTOCOL Yahalom;
VARIABLES
S : Server;
A, B : Client;
Na, Nb : Nonce;
Kab : Skey, CRYPTO, FRESH;
F : Field;
Kas, Kbs: Skey;
DENOTES
Kas = csk(A): A;
Kas = ssk(S,A): S;
Kbs = csk(B): B;
Kbs = ssk(S,B): S;
ASSUMPTIONS
HOLDS A: B;
HOLDS B: S;
MESSAGES
1. A -> B: A, Na;
2. B -> S: B, {A, Na, Nb}Kbs;
3. S -> A: {B, Kab, Na, Nb}Kas, {A, Kab}Kbs%F;
4. A -> B: F%{A, Kab}Kbs, {Nb}Kab;
GOALS
SECRET Kab;
PRECEDES A: B | Nb, Kab;
END;
/**************************************************************
6.3.7 - Carlsen Secret Key Initiator Protocol */
PROTOCOL Carlsen;
VARIABLES
S : Server;
A, B: Client;
Na, Nb, N_b : Nonce;
Kab : Skey, CRYPTO, FRESH;
F : Field;
Kbs,Kas: Skey;
DENOTES
Kbs = csk(B): B;
Kbs = ssk(S,B): S;
Kas = csk(A): A;
Kas = ssk(S,A): S;
ASSUMPTIONS
HOLDS A: B;
HOLDS B: S;
MESSAGES
1. A -> B: A, Na;
2. B -> S: A, Na, B, Nb;
3. S -> B: {Kab, Nb, A}Kbs, {Na, B, Kab}Kas%F;
4. B -> A: F%{Na, B, Kab}Kas, {Na}Kab, N_b;
5. A -> B: {N_b}Kab;
GOALS
SECRET Kab;
PRECEDES A: B | N_b, Kab;
END;
/**************************************************************
6.3.8 ISO Four Pass Authentication Protocol */
PROTOCOL ISO4P;
VARIABLES
S : Server;
A, B: Client;
Text1, Text2, Text3, Text4, Text5, Text6, Text7, Text8: Field;
TVPa: Atom;
Na, Nb, Ns : Nonce;
Kab : Skey, CRYPTO, FRESH;
F : Field;
Kas: Skey;
DENOTES
Kas = csk(A): A;
Kas = ssk(S,A): S;
ASSUMPTIONS
HOLDS A: B, S, TVPa, Text1, Text6, Text5;
HOLDS B: Text8, Text7;
HOLDS S: Text4, Text3, Text2;
MESSAGES
1. A -> S: A, TVPa, B, Text1;
2. S -> A: Text4, {TVPa, Kab, B, Text3}Kas, {Ns, Kab, A, Text2}ssk(S,B)%F;
3. A -> B: A, Text6, F%{Ns, Kab, A, Text2}csk(B), {Na, B, Text5}Kab;
4. B -> A: Text8, {Nb, A, Text7}Kab;
GOALS
SECRET Kab;
PRECEDES A: B | Na, Text5, Kab;
PRECEDES B: A | Nb, Text7, Kab;
END;
/**************************************************************
6.3.9 ISO Five Pass Authentication Protocol */
PROTOCOL ISO5P;
VARIABLES
S : Server;
A, B: Client;
Text1, Text2, Text3, Text4, Text5, Text6, Text7, Text8, Text9: Field;
Ra, Rb, R_b : Nonce;
Kab : Skey, CRYPTO, FRESH;
F : Field;
Kbs : Skey;
DENOTES
Kbs = csk(B): B;
Kbs = ssk(S,B): S;
ASSUMPTIONS
HOLDS A: B, Text1, Text9, Text8;
HOLDS B: S, Text2, Text7, Text6;
HOLDS S: Text5, Text4, Text3, B;
MESSAGES
1. A -> B: A, Ra, Text1;
2. B -> S: B, R_b, Ra, A, Text2;
3. S -> B: Text5, {R_b, Kab, A, Text4}Kbs, {Ra, Kab, B, Text3}ssk(S,A)%F;
4. B -> A: B, Text7, F%{Ra, Kab, B, Text3}csk(A), {Rb, Ra, Text6}Kab;
5. A -> B: Text9, {Ra, Rb, Text8}Kab;
GOALS
SECRET Kab;
PRECEDES B: A | Ra, Rb, Text6;
PRECEDES A: B | Ra, Rb, Text8;
END;
/*************************************************************
6.3.10 Woo-Lam Authentication Protocol Pi_f */
PROTOCOL WooLamPif;
VARIABLES
S : Server;
A, B : Client;
Nb : Nonce;
F : Field;
Kbs: Skey;
DENOTES
Kbs = ssk(S,B): S;
Kbs = csk(B): B;
ASSUMPTIONS
HOLDS A: B;
HOLDS B: S;
MESSAGES
1. A -> B: A;
2. B -> A: Nb;
3. A -> B: {A, B, Nb}csk(A)%F;
4. B -> S: B, {A, B, Nb, F%{A, B, Nb}ssk(S,A)}Kbs;
5. S -> B: {A, B, Nb}Kbs;
GOALS
PRECEDES A: B | Nb;
END;
/*************************************************************
6.3.10 Woo-Lam Authentication Protocol Pi */
/* Attack: Parallel session attack, attacker can masquerade
as A. */
PROTOCOL WooLamPi;
VARIABLES
S : Server;
A, B : Client;
Nb : Nonce;
F : Field;
Kbs: Skey;
DENOTES
Kbs = ssk(S,B): S;
Kbs = csk(B): B;
ASSUMPTIONS
HOLDS A: B;
HOLDS B: S;
MESSAGES
1. A -> B: A;
2. B -> A: Nb;
3. A -> B: {Nb}csk(A)%F;
4. B -> S: B, {A, F%{Nb}ssk(S,A)}Kbs;
5. S -> B: {Nb}Kbs;
GOALS
PRECEDES A: B | Nb;
END;
/*************************************************************
6.3.11 Woo and Lam Mutual Authentication Protocol */
/* Attack: Parallel session attack by Q that causes P
to accept a prior P-Q key. */
PROTOCOL WooLamMutual;
VARIABLES
S : Server;
P, Q : Client;
N1, N2 : Nonce;
F1, F2 : Field;
Kpq : Skey, CRYPTO, FRESH;
Kqs : Skey;
DENOTES
Kqs = csk(Q): Q;
Kqs = ssk(S,Q): S;
ASSUMPTIONS
HOLDS P: Q;
HOLDS Q: S;
MESSAGES
1. P -> Q: P, N1;
2. Q -> P: Q, N2;
3. P -> Q: {P, Q, N1, N2}csk(P)%F1;
4. Q -> S: P, Q, F1%{P, Q, N1, N2}ssk(S,P), {P, Q, N1, N2}Kqs;
5. S -> Q: {Q, N1, N2, Kpq}ssk(S,P)%F2, {P, N1, N2, Kpq}Kqs;
6. Q -> P: F2%{Q, N1, N2, Kpq}csk(P), {N1, N2}Kpq;
7. P -> Q: {N2}Kpq;
GOALS
SECRET Kpq;
PRECEDES Q: P | N1, N2;
PRECEDES P: Q | N2;
END;
/**************************************************************
6.4.1 Needham-Schroeder Signature Protocol */
PROTOCOL NSS;
VARIABLES
S : Server;
A, B: Client;
msg : Field;
F : Field;
Kas, Kbs : Skey;
CS: Skey;
FUNCTIONS
Kss(Server): Skey,PRIVATE;
DENOTES
Kas = csk(A): A;
Kas = ssk(S, A): S;
Kbs = csk(B): B;
Kbs = ssk(S, B): S;
CS = sha(msg): A,B;
ASSUMPTIONS
HOLDS A: S, B, msg;
HOLDS B: S;
MESSAGES
1. A -> S: A, {CS}Kas;
2. S -> A: {A, CS}Kss(S)%F;
3. A -> B: msg, F;
4. B -> S: B, F%{A, CS}Kss(S);
5. S -> B: {A, CS}Kbs;
GOALS
PRECEDES A: B | msg;
END;
Part II