scyther/gui/Protocols/ISO-9798/isoiec-9798-2-5.spdl
2012-11-15 12:10:06 +01:00

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
{
}
}