94 lines
1.8 KiB
Plaintext
94 lines
1.8 KiB
Plaintext
|
/*
|
||
|
|
* Modeled from ISO/IEC 9798
|
||
|
|
* Modeler: Cas Cremers, Dec. 2010
|
||
|
|
*
|
||
|
|
* symmetric
|
||
|
|
* ttp
|
||
|
|
* four-pass
|
||
|
|
* mutual
|
||
|
|
*
|
||
|
|
* Modeling notes:
|
||
|
|
* - The use of TNb in message 4, as specified by the ISO standard, is
|
||
|
|
* different from other models, in which it was TNa.
|
||
|
|
*/
|
||
|
|
usertype SessionKey;
|
||
|
|
|
||
|
|
protocol isoiec-9798-2-5(A,B,P)
|
||
|
|
{
|
||
|
|
role A
|
||
|
|
{
|
||
|
|
fresh TVPa: Nonce;
|
||
|
|
var T: Ticket;
|
||
|
|
fresh TNa: Nonce;
|
||
|
|
var TNb: Nonce;
|
||
|
|
var Kab: SessionKey;
|
||
|
|
fresh Text1,Text5,Text6: Ticket;
|
||
|
|
var Text3,Text4,Text7,Text8: Ticket;
|
||
|
|
|
||
|
|
send_1(A,P, TVPa, B, Text1);
|
||
|
|
recv_2(P,A, Text4, { TVPa, Kab, B, Text3 }k(A,P), T );
|
||
|
|
claim(A,Running,B,Kab,Text5);
|
||
|
|
send_3(A,B, Text6, T, { TNa, B, Text5 }Kab );
|
||
|
|
recv_4(B,A, Text8, { TNb, A, Text7 }Kab );
|
||
|
|
|
||
|
|
claim(A,Commit,B,Kab,Text5,Text7);
|
||
|
|
claim(A,Secret,Kab);
|
||
|
|
claim(A,Secret,Text5);
|
||
|
|
claim(A,Secret,Text7);
|
||
|
|
claim(A,Alive);
|
||
|
|
claim(A,Weakagree);
|
||
|
|
}
|
||
|
|
role B
|
||
|
|
{
|
||
|
|
var TNp: Nonce;
|
||
|
|
var TNa: Nonce;
|
||
|
|
fresh TNb: Nonce;
|
||
|
|
var Kab: SessionKey;
|
||
|
|
fresh Text7,Text8: Ticket;
|
||
|
|
var Text2,Text5,Text6: Ticket;
|
||
|
|
|
||
|
|
recv_3(A,B, Text6, { TNp, Kab, A, Text2 }k(B,P), { TNa, B, Text5 }Kab );
|
||
|
|
claim(B,Running,A,Kab,Text5,Text7);
|
||
|
|
send_4(B,A, Text8, { TNb, A, Text7 }Kab );
|
||
|
|
|
||
|
|
claim(B,Commit,A,Kab,Text5);
|
||
|
|
claim(B,Secret,Kab);
|
||
|
|
claim(B,Secret,Text5);
|
||
|
|
claim(B,Secret,Text7);
|
||
|
|
claim(B,Alive);
|
||
|
|
claim(B,Weakagree);
|
||
|
|
}
|
||
|
|
role P
|
||
|
|
{
|
||
|
|
var TVPa: Nonce;
|
||
|
|
fresh TNp: Nonce;
|
||
|
|
fresh Kab: SessionKey;
|
||
|
|
fresh Text2,Text3,Text4: Ticket;
|
||
|
|
var Text1: Ticket;
|
||
|
|
|
||
|
|
recv_1(A,P, TVPa, B, Text1);
|
||
|
|
send_2(P,A, Text4, { TVPa, Kab, B, Text3 }k(A,P),
|
||
|
|
{ TNp, Kab, A, Text2 }k(B,P) );
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
protocol @keysymm25(A,B,P)
|
||
|
|
{
|
||
|
|
role A
|
||
|
|
{
|
||
|
|
var TVPN: Nonce;
|
||
|
|
var Kab: SessionKey;
|
||
|
|
var Text: Ticket;
|
||
|
|
|
||
|
|
recv_!1(B,A, { TVPN, Kab, B, Text }k(P,A) );
|
||
|
|
send_!2(A,B, { TVPN, Kab, B, Text }k(A,P) );
|
||
|
|
}
|
||
|
|
role B
|
||
|
|
{
|
||
|
|
}
|
||
|
|
role P
|
||
|
|
{
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|