Added ISO/IEC 9798 models.
This commit is contained in:
parent
65713fd508
commit
a911f56705
16
gui/Protocols/ISO-9798/Makefile
Normal file
16
gui/Protocols/ISO-9798/Makefile
Normal file
@ -0,0 +1,16 @@
|
||||
|
||||
outputs= isoiec-9798-3-6-1.spdl isoiec-9798-3-6-2.spdl \
|
||||
isoiec-9798-3-7-1.spdl isoiec-9798-3-7-2.spdl
|
||||
|
||||
all: $(outputs)
|
||||
|
||||
isoiec-9798-3-6-%.spdl: isoiec-9798-3-6-%.cpp isoiec-9798-3-6.template
|
||||
cpp -C -P $< >$@
|
||||
|
||||
isoiec-9798-3-7-%.spdl: isoiec-9798-3-7-%.cpp isoiec-9798-3-7.template
|
||||
cpp -C -P $< >$@
|
||||
|
||||
clean:
|
||||
\rm -f $(outputs)
|
||||
|
||||
|
78
gui/Protocols/ISO-9798/iso25-tag.spdl
Normal file
78
gui/Protocols/ISO-9798/iso25-tag.spdl
Normal file
@ -0,0 +1,78 @@
|
||||
/*
|
||||
* 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;
|
||||
usertype Tag;
|
||||
|
||||
const t1,t2a,t2b,t3,t4,t5: Tag;
|
||||
|
||||
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, { t2a, TVPa, Kab, B, Text3 }k(A,P), T );
|
||||
claim(A,Running,B,Kab,Text5);
|
||||
send_3(A,B, Text6, T, { t3, TNa, B, Text5 }Kab );
|
||||
recv_4(B,A, Text8, { t4, 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, { t2b, TNp, Kab, A, Text2 }k(B,P), {
|
||||
t3, TNa, B, Text5 }Kab );
|
||||
claim(B,Running,A,Kab,Text5,Text7);
|
||||
send_4(B,A, Text8, { t4, 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, { t2a, TVPa, Kab, B, Text3 }k(A,P),
|
||||
{ t2b, TNp, Kab, A, Text2 }k(B,P) );
|
||||
}
|
||||
}
|
||||
|
95
gui/Protocols/ISO-9798/iso26-tag.spdl
Normal file
95
gui/Protocols/ISO-9798/iso26-tag.spdl
Normal file
@ -0,0 +1,95 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* symmetric
|
||||
* ttp
|
||||
* five-pass
|
||||
* mutual
|
||||
*
|
||||
* MPA Attack reported by Mathuria:
|
||||
* - Type flaw MPA when in parallel with Abadi-Needham protocol.
|
||||
*
|
||||
*/
|
||||
usertype Tag;
|
||||
|
||||
const t1,t2,t3,t4,t5: Tag;
|
||||
|
||||
protocol isoiec-9798-2-6-tag(A,B,P)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var Rb: Nonce;
|
||||
fresh Ra,Rpa: Nonce;
|
||||
var Kab: SessionKey;
|
||||
var T: Ticket;
|
||||
fresh Text2,Text6,Text7: Ticket;
|
||||
var Text1,Text4,Text5,Text8,Text9: Ticket;
|
||||
|
||||
recv_1(B,A, Rb, Text1);
|
||||
send_2(A,P, Ra, Rb, B, Text2);
|
||||
recv_3(P,A, Text5, {t1, Ra,Kab,B,Text4}k(A,P), T );
|
||||
claim(A,Running,B,Kab,Text6);
|
||||
send_4(A,B, Text7, T, {t3,Rpa,Rb,Text6}Kab );
|
||||
recv_5(B,A, Text9, {t4,Rb,Rpa,Text8}Kab );
|
||||
|
||||
claim(A,Commit,B,Kab,Text6,Text8);
|
||||
claim(A,Secret,Kab);
|
||||
claim(A,Secret,Text6);
|
||||
claim(A,Secret,Text8);
|
||||
claim(A,Alive);
|
||||
claim(A,Weakagree);
|
||||
}
|
||||
role B
|
||||
{
|
||||
fresh Rb: Nonce;
|
||||
var Rpa: Nonce;
|
||||
var Kab: SessionKey;
|
||||
fresh Text1,Text8,Text9: Ticket;
|
||||
var Text3,Text6,Text7: Ticket;
|
||||
|
||||
send_1(B,A, Rb, Text1);
|
||||
recv_4(A,B, Text7, {t2,Rb,Kab,A,Text3}k(B,P), {t3,Rpa,Rb,Text6}Kab );
|
||||
claim(B,Running,A,Kab,Text6,Text8);
|
||||
send_5(B,A, Text9, {t4,Rb,Rpa,Text8}Kab );
|
||||
|
||||
claim(B,Commit,A,Kab,Text6);
|
||||
claim(B,Secret,Kab);
|
||||
claim(B,Secret,Text6);
|
||||
claim(B,Secret,Text8);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
role P
|
||||
{
|
||||
var Ra, Rb: Nonce;
|
||||
fresh Kab: SessionKey;
|
||||
fresh Text3,Text4,Text5: Ticket;
|
||||
var Text2: Ticket;
|
||||
|
||||
recv_2(A,P, Ra, Rb, B, Text2);
|
||||
send_3(P,A, Text5, {t1,Ra,Kab,B,Text4}k(A,P),
|
||||
{t2,Rb,Kab,A,Text3}k(B,P) );
|
||||
}
|
||||
}
|
||||
|
||||
protocol @keysymm26(A,B,P)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var TVPN: Nonce;
|
||||
var Kab: SessionKey;
|
||||
var Text: Ticket;
|
||||
var Tag: Ticket;
|
||||
|
||||
recv_!1(B,A, { Tag,TVPN, Kab, B, Text }k(P,A) );
|
||||
send_!2(A,B, { Tag,TVPN, Kab, B, Text }k(A,P) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
}
|
||||
role P
|
||||
{
|
||||
}
|
||||
}
|
||||
|
35
gui/Protocols/ISO-9798/isoiec-9798-2-1-udkey.spdl
Normal file
35
gui/Protocols/ISO-9798/isoiec-9798-2-1-udkey.spdl
Normal file
@ -0,0 +1,35 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* symmetric
|
||||
* one-pass
|
||||
* unilateral
|
||||
*
|
||||
* Note: the identity B may be ommitted, if
|
||||
* (a) the environment disallows such attacks, or
|
||||
* (b) a unidirectional key is used
|
||||
*/
|
||||
protocol isoiec-9798-2-1-udkey(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh TNA: Nonce;
|
||||
fresh Text1,Text2: Ticket;
|
||||
|
||||
claim(A,Running,B,TNA,Text1);
|
||||
send_1(A,B, Text2, { TNA, Text1 }k(A,B) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
var TNA: Nonce;
|
||||
var Text1,Text2: Ticket;
|
||||
|
||||
recv_1(A,B, Text2, { TNA, Text1 }k(A,B) );
|
||||
|
||||
claim(B,Commit,A,TNA,Text1);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
55
gui/Protocols/ISO-9798/isoiec-9798-2-1.spdl
Normal file
55
gui/Protocols/ISO-9798/isoiec-9798-2-1.spdl
Normal file
@ -0,0 +1,55 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* symmetric
|
||||
* one-pass
|
||||
* unilateral
|
||||
*
|
||||
* Note: the identity B may be ommitted, if
|
||||
* (a) the environment disallows such attacks, or
|
||||
* (b) a unidirectional key is used
|
||||
*/
|
||||
protocol @keysymm-21(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var T: Nonce;
|
||||
var Text: Ticket;
|
||||
|
||||
recv_!1(B,A, { T, A, Text }k(A,B) );
|
||||
send_!2(A,B, { T, A, Text }k(B,A) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
var T: Nonce;
|
||||
var Text: Ticket;
|
||||
|
||||
recv_!3(A,B, { T, B, Text }k(A,B) );
|
||||
send_!4(B,A, { T, B, Text }k(B,A) );
|
||||
}
|
||||
}
|
||||
|
||||
protocol isoiec-9798-2-1(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh TNA: Nonce;
|
||||
fresh Text1,Text2: Ticket;
|
||||
|
||||
claim(A,Running,B,TNA,Text1);
|
||||
send_1(A,B, Text2, { TNA, B, Text1 }k(A,B) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
var TNA: Nonce;
|
||||
var Text1,Text2: Ticket;
|
||||
|
||||
recv_1(A,B, Text2, { TNA, B, Text1 }k(A,B) );
|
||||
|
||||
claim(B,Commit,A,TNA,Text1);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
40
gui/Protocols/ISO-9798/isoiec-9798-2-2-udkey.spdl
Normal file
40
gui/Protocols/ISO-9798/isoiec-9798-2-2-udkey.spdl
Normal file
@ -0,0 +1,40 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* symmetric
|
||||
* two-pass
|
||||
* unilateral
|
||||
*
|
||||
* Note: the identity A may be ommitted, if
|
||||
* (a) the environment disallows such attacks, or
|
||||
* (b) a unidirectional key is used
|
||||
*
|
||||
*/
|
||||
protocol isoiec-9798-2-2-udkey(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var RB: Nonce;
|
||||
var Text1: Ticket;
|
||||
fresh Text2,Text3: Ticket;
|
||||
|
||||
recv_1(B,A, RB,Text1 );
|
||||
claim(A,Running,B,RB,Text2);
|
||||
send_2(A,B, Text3, { RB, Text2 }k(B,A) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
fresh RB: Nonce;
|
||||
fresh Text1: Ticket;
|
||||
var Text2,Text3: Ticket;
|
||||
|
||||
send_1(B,A, RB,Text1 );
|
||||
recv_2(A,B, Text3, { RB, Text2 }k(B,A) );
|
||||
|
||||
claim(B,Commit,A,RB,Text2);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
59
gui/Protocols/ISO-9798/isoiec-9798-2-2.spdl
Normal file
59
gui/Protocols/ISO-9798/isoiec-9798-2-2.spdl
Normal file
@ -0,0 +1,59 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* symmetric
|
||||
* two-pass
|
||||
* unilateral
|
||||
*
|
||||
* Note: the identity A may be ommitted, if
|
||||
* (a) the environment disallows such attacks, or
|
||||
* (b) a unidirectional key is used
|
||||
*/
|
||||
protocol @keysymm-22(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var T: Nonce;
|
||||
var Text: Ticket;
|
||||
|
||||
recv_!1(B,A, { T, A, Text }k(A,B) );
|
||||
send_!2(A,B, { T, A, Text }k(B,A) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
var T: Nonce;
|
||||
var Text: Ticket;
|
||||
|
||||
recv_!3(A,B, { T, B, Text }k(A,B) );
|
||||
send_!4(B,A, { T, B, Text }k(B,A) );
|
||||
}
|
||||
}
|
||||
|
||||
protocol isoiec-9798-2-2(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var RB: Nonce;
|
||||
var Text1: Ticket;
|
||||
fresh Text2,Text3: Ticket;
|
||||
|
||||
recv_1(B,A, RB,Text1 );
|
||||
claim(A,Running,B,RB,Text2);
|
||||
send_2(A,B, Text3, { RB, B, Text2 }k(B,A) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
fresh RB: Nonce;
|
||||
fresh Text1: Ticket;
|
||||
var Text2,Text3: Ticket;
|
||||
|
||||
send_1(B,A, RB,Text1 );
|
||||
recv_2(A,B, Text3, { RB, B, Text2 }k(B,A) );
|
||||
|
||||
claim(B,Commit,A,RB,Text2);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
49
gui/Protocols/ISO-9798/isoiec-9798-2-3-udkey.spdl
Normal file
49
gui/Protocols/ISO-9798/isoiec-9798-2-3-udkey.spdl
Normal file
@ -0,0 +1,49 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* symmetric
|
||||
* two-pass
|
||||
* mutual
|
||||
*
|
||||
* Note: the identity inside the encryption may be ommitted, if
|
||||
* (a) the environment disallows such attacks, or
|
||||
* (b) a unidirectional key is used
|
||||
*
|
||||
* In case (b), modeled here, the second key is reversed.
|
||||
*
|
||||
*/
|
||||
protocol isoiec-9798-2-3-udkey(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh TNA: Nonce;
|
||||
var TNB: Nonce;
|
||||
fresh Text1,Text2: Ticket;
|
||||
var Text3,Text4: Ticket;
|
||||
|
||||
claim(A,Running,B,TNA,Text1);
|
||||
send_1(A,B, Text2, { TNA, Text1 }k(A,B) );
|
||||
recv_2(B,A, Text4, { TNB, Text3 }k(B,A) );
|
||||
|
||||
claim(A,Commit,B,TNB,Text3);
|
||||
claim(A,Alive);
|
||||
claim(A,Weakagree);
|
||||
}
|
||||
role B
|
||||
{
|
||||
var TNA: Nonce;
|
||||
fresh TNB: Nonce;
|
||||
var Text1,Text2: Ticket;
|
||||
fresh Text3,Text4: Ticket;
|
||||
|
||||
recv_1(A,B, Text2, { TNA, Text1 }k(A,B) );
|
||||
claim(B,Running,A,TNB,Text3);
|
||||
send_2(B,A, Text4, { TNB, Text3 }k(B,A) );
|
||||
|
||||
claim(B,Commit,A,TNA,Text1);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
67
gui/Protocols/ISO-9798/isoiec-9798-2-3.spdl
Normal file
67
gui/Protocols/ISO-9798/isoiec-9798-2-3.spdl
Normal file
@ -0,0 +1,67 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* symmetric
|
||||
* two-pass
|
||||
* mutual
|
||||
*
|
||||
* Note: the identity inside the encryption may be ommitted, if
|
||||
* (a) the environment disallows such attacks, or
|
||||
* (b) a unidirectional key is used
|
||||
*
|
||||
*/
|
||||
protocol @keysymm-23(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var T: Nonce;
|
||||
var Text: Ticket;
|
||||
|
||||
recv_!1(B,A, { T, A, Text }k(A,B) );
|
||||
send_!2(A,B, { T, A, Text }k(B,A) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
var T: Nonce;
|
||||
var Text: Ticket;
|
||||
|
||||
recv_!3(A,B, { T, B, Text }k(A,B) );
|
||||
send_!4(B,A, { T, B, Text }k(B,A) );
|
||||
}
|
||||
}
|
||||
|
||||
protocol isoiec-9798-2-3(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh TNA: Nonce;
|
||||
var TNB: Nonce;
|
||||
fresh Text1,Text2: Ticket;
|
||||
var Text3,Text4: Ticket;
|
||||
|
||||
claim(A,Running,B,TNA,Text1);
|
||||
send_1(A,B, Text2, { TNA, B, Text1 }k(A,B) );
|
||||
recv_2(B,A, Text4, { TNB, A, Text3 }k(A,B) );
|
||||
|
||||
claim(A,Commit,B,TNB,Text3);
|
||||
claim(A,Alive);
|
||||
claim(A,Weakagree);
|
||||
}
|
||||
role B
|
||||
{
|
||||
var TNA: Nonce;
|
||||
fresh TNB: Nonce;
|
||||
var Text1,Text2: Ticket;
|
||||
fresh Text3,Text4: Ticket;
|
||||
|
||||
recv_1(A,B, Text2, { TNA, B, Text1 }k(A,B) );
|
||||
claim(B,Running,A,TNB,Text3);
|
||||
send_2(B,A, Text4, { TNB, A, Text3 }k(A,B) );
|
||||
|
||||
claim(B,Commit,A,TNA,Text1);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
50
gui/Protocols/ISO-9798/isoiec-9798-2-4-udkey.spdl
Normal file
50
gui/Protocols/ISO-9798/isoiec-9798-2-4-udkey.spdl
Normal file
@ -0,0 +1,50 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* symmetric
|
||||
* three-pass
|
||||
* mutual
|
||||
*
|
||||
* Note: the identity inside the encryption may be ommitted, if
|
||||
* (a) the environment disallows such attacks, or
|
||||
* (b) a unidirectional key is used
|
||||
*
|
||||
* In case (b), modeled here, the second key is reversed.
|
||||
*/
|
||||
protocol isoiec-9798-2-4-udkey(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var RB: Nonce;
|
||||
fresh RA: Nonce;
|
||||
var Text1,Text4,Text5: Ticket;
|
||||
fresh Text2,Text3: Ticket;
|
||||
|
||||
recv_1(B,A, RB,Text1 );
|
||||
claim(A,Running,B,RA,RB,Text2);
|
||||
send_2(A,B, Text3, { RA, RB, Text2 }k(A,B) );
|
||||
recv_3(B,A, Text5, { RB, RA, Text4 }k(B,A) );
|
||||
|
||||
claim(A,Commit,B,RA,RB,Text2,Text4);
|
||||
claim(A,Alive);
|
||||
claim(A,Weakagree);
|
||||
}
|
||||
role B
|
||||
{
|
||||
fresh RB: Nonce;
|
||||
var RA: Nonce;
|
||||
fresh Text1,Text4,Text5: Ticket;
|
||||
var Text2,Text3: Ticket;
|
||||
|
||||
send_1(B,A, RB,Text1 );
|
||||
recv_2(A,B, Text3, { RA, RB, Text2 }k(A,B) );
|
||||
claim(B,Running,A,RA,RB,Text2,Text4);
|
||||
send_3(B,A, Text5, { RB, RA, Text4 }k(B,A) );
|
||||
|
||||
claim(B,Commit,A,RA,RB,Text2);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
88
gui/Protocols/ISO-9798/isoiec-9798-2-4.spdl
Normal file
88
gui/Protocols/ISO-9798/isoiec-9798-2-4.spdl
Normal file
@ -0,0 +1,88 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* symmetric
|
||||
* three-pass
|
||||
* mutual
|
||||
*
|
||||
* Note: the identity inside the encryption may be ommitted, if
|
||||
* (a) the environment disallows such attacks, or
|
||||
* (b) a unidirectional key is used
|
||||
*/
|
||||
protocol @keysymm-24a(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var T1,T2: Nonce;
|
||||
var Text: Ticket;
|
||||
|
||||
recv_!1(B,A, { T1, T2, A, Text }k(A,B) );
|
||||
send_!2(A,B, { T1, T2, A, Text }k(B,A) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
var T1,T2: Nonce;
|
||||
var Text: Ticket;
|
||||
|
||||
recv_!3(A,B, { T1, T2, B, Text }k(A,B) );
|
||||
send_!4(B,A, { T1, T2, B, Text }k(B,A) );
|
||||
}
|
||||
}
|
||||
|
||||
protocol @keysymm-24b(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var T1,T2: Nonce;
|
||||
var Text: Ticket;
|
||||
|
||||
recv_!1(B,A, { T1, T2, Text }k(A,B) );
|
||||
send_!2(A,B, { T1, T2, Text }k(B,A) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
var T1,T2: Nonce;
|
||||
var Text: Ticket;
|
||||
|
||||
recv_!3(A,B, { T1, T2, Text }k(A,B) );
|
||||
send_!4(B,A, { T1, T2, Text }k(B,A) );
|
||||
}
|
||||
}
|
||||
|
||||
protocol isoiec-9798-2-4(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var RB: Nonce;
|
||||
fresh RA: Nonce;
|
||||
var Text1,Text4,Text5: Ticket;
|
||||
fresh Text2,Text3: Ticket;
|
||||
|
||||
recv_1(B,A, RB,Text1 );
|
||||
claim(A,Running,B,RA,RB,Text2);
|
||||
send_2(A,B, Text3, { RA, RB, B, Text2 }k(A,B) );
|
||||
recv_3(B,A, Text5, { RB, RA, Text4 }k(A,B) );
|
||||
|
||||
claim(A,Commit,B,RA,RB,Text2,Text4);
|
||||
claim(A,Alive);
|
||||
claim(A,Weakagree);
|
||||
}
|
||||
role B
|
||||
{
|
||||
fresh RB: Nonce;
|
||||
var RA: Nonce;
|
||||
fresh Text1,Text4,Text5: Ticket;
|
||||
var Text2,Text3: Ticket;
|
||||
|
||||
send_1(B,A, RB,Text1 );
|
||||
recv_2(A,B, Text3, { RA, RB, B, Text2 }k(A,B) );
|
||||
claim(B,Running,A,RA,RB,Text2,Text4);
|
||||
send_3(B,A, Text5, { RB, RA, Text4 }k(A,B) );
|
||||
|
||||
claim(B,Commit,A,RA,RB,Text2);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
93
gui/Protocols/ISO-9798/isoiec-9798-2-5.spdl
Normal file
93
gui/Protocols/ISO-9798/isoiec-9798-2-5.spdl
Normal file
@ -0,0 +1,93 @@
|
||||
/*
|
||||
* 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
|
||||
{
|
||||
}
|
||||
}
|
||||
|
90
gui/Protocols/ISO-9798/isoiec-9798-2-6.spdl
Normal file
90
gui/Protocols/ISO-9798/isoiec-9798-2-6.spdl
Normal file
@ -0,0 +1,90 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* symmetric
|
||||
* ttp
|
||||
* five-pass
|
||||
* mutual
|
||||
*
|
||||
* MPA Attack reported by Mathuria:
|
||||
* - Type flaw MPA when in parallel with Abadi-Needham protocol.
|
||||
*
|
||||
*/
|
||||
protocol isoiec-9798-2-6(A,B,P)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var Rb: Nonce;
|
||||
fresh Ra,Rpa: Nonce;
|
||||
var Kab: SessionKey;
|
||||
var T: Ticket;
|
||||
fresh Text2,Text6,Text7: Ticket;
|
||||
var Text1,Text4,Text5,Text8,Text9: Ticket;
|
||||
|
||||
recv_1(B,A, Rb, Text1);
|
||||
send_2(A,P, Ra, Rb, B, Text2);
|
||||
recv_3(P,A, Text5, {Ra,Kab,B,Text4}k(A,P), T );
|
||||
claim(A,Running,B,Kab,Text6);
|
||||
send_4(A,B, Text7, T, {Rpa,Rb,Text6}Kab );
|
||||
recv_5(B,A, Text9, {Rb,Rpa,Text8}Kab );
|
||||
|
||||
claim(A,Commit,B,Kab,Text6,Text8);
|
||||
claim(A,Secret,Kab);
|
||||
claim(A,Secret,Text6);
|
||||
claim(A,Secret,Text8);
|
||||
claim(A,Alive);
|
||||
claim(A,Weakagree);
|
||||
}
|
||||
role B
|
||||
{
|
||||
fresh Rb: Nonce;
|
||||
var Rpa: Nonce;
|
||||
var Kab: SessionKey;
|
||||
fresh Text1,Text8,Text9: Ticket;
|
||||
var Text3,Text6,Text7: Ticket;
|
||||
|
||||
send_1(B,A, Rb, Text1);
|
||||
recv_4(A,B, Text7, {Rb,Kab,A,Text3}k(B,P), {Rpa,Rb,Text6}Kab );
|
||||
claim(B,Running,A,Kab,Text6,Text8);
|
||||
send_5(B,A, Text9, {Rb,Rpa,Text8}Kab );
|
||||
|
||||
claim(B,Commit,A,Kab,Text6);
|
||||
claim(B,Secret,Kab);
|
||||
claim(B,Secret,Text6);
|
||||
claim(B,Secret,Text8);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
role P
|
||||
{
|
||||
var Ra, Rb: Nonce;
|
||||
fresh Kab: SessionKey;
|
||||
fresh Text3,Text4,Text5: Ticket;
|
||||
var Text2: Ticket;
|
||||
|
||||
recv_2(A,P, Ra, Rb, B, Text2);
|
||||
send_3(P,A, Text5, {Ra,Kab,B,Text4}k(A,P),
|
||||
{Rb,Kab,A,Text3}k(B,P) );
|
||||
}
|
||||
}
|
||||
|
||||
protocol @keysymm26(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
|
||||
{
|
||||
}
|
||||
}
|
||||
|
33
gui/Protocols/ISO-9798/isoiec-9798-3-1.spdl
Normal file
33
gui/Protocols/ISO-9798/isoiec-9798-3-1.spdl
Normal file
@ -0,0 +1,33 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* signature
|
||||
* one-pass
|
||||
* unilateral
|
||||
*/
|
||||
const Cert: Function;
|
||||
|
||||
protocol isoiec-9798-3-1(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh TNA: Nonce;
|
||||
fresh Text1,Text2: Ticket;
|
||||
|
||||
claim(A,Running,B,TNA,Text1);
|
||||
send_1(A,B, Cert(A),TNA,B,Text2, { TNA, B, Text1 }sk(A) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
var TNA: Nonce;
|
||||
var Text1,Text2: Ticket;
|
||||
|
||||
recv_1(A,B, Cert(A),TNA,B,Text2, { TNA, B, Text1 }sk(A) );
|
||||
|
||||
claim(B,Commit,A,TNA,Text1);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
39
gui/Protocols/ISO-9798/isoiec-9798-3-2.spdl
Normal file
39
gui/Protocols/ISO-9798/isoiec-9798-3-2.spdl
Normal file
@ -0,0 +1,39 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* signature
|
||||
* two-pass
|
||||
* unilateral
|
||||
*/
|
||||
const Cert: Function;
|
||||
|
||||
protocol isoiec-9798-3-2(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var Rb: Nonce;
|
||||
fresh Ra: Nonce;
|
||||
var Text1: Ticket;
|
||||
fresh Text2,Text3: Ticket;
|
||||
|
||||
recv_1(B,A, Rb,Text1 );
|
||||
claim(A,Running,B,Ra,Rb,Text2);
|
||||
send_2(A,B, Cert(A),Ra,Rb,B,Text3, { Ra, Rb, B, Text2 }sk(A) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
fresh Rb: Nonce;
|
||||
var Ra: Nonce;
|
||||
fresh Text1: Ticket;
|
||||
var Text2,Text3: Ticket;
|
||||
|
||||
send_1(B,A, Rb,Text1 );
|
||||
recv_2(A,B, Cert(A),Ra,Rb,B,Text3, { Ra, Rb, B, Text2 }sk(A) );
|
||||
|
||||
claim(B,Commit,A,Ra,Rb,Text2);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
44
gui/Protocols/ISO-9798/isoiec-9798-3-3.spdl
Normal file
44
gui/Protocols/ISO-9798/isoiec-9798-3-3.spdl
Normal file
@ -0,0 +1,44 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* signature
|
||||
* two-pass
|
||||
* mutual
|
||||
*/
|
||||
const Cert: Function;
|
||||
|
||||
protocol isoiec-9798-3-3(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh TNA: Nonce;
|
||||
var TNB: Nonce;
|
||||
fresh Text1,Text2: Ticket;
|
||||
var Text3,Text4: Ticket;
|
||||
|
||||
claim(A,Running,B,TNA,Text1);
|
||||
send_1(A,B, Cert(A), TNA, B,Text2, { TNA, B, Text1 }sk(A) );
|
||||
recv_2(B,A, Cert(B), TNB, A,Text4, { TNB, A, Text3 }sk(B) );
|
||||
|
||||
claim(A,Commit,B,TNB,Text3);
|
||||
claim(A,Alive);
|
||||
claim(A,Weakagree);
|
||||
}
|
||||
role B
|
||||
{
|
||||
var TNA: Nonce;
|
||||
fresh TNB: Nonce;
|
||||
var Text1,Text2: Ticket;
|
||||
fresh Text3,Text4: Ticket;
|
||||
|
||||
recv_1(A,B, Cert(A), TNA, B,Text2, { TNA, B, Text1 }sk(A) );
|
||||
claim(B,Running,A,TNB,Text3);
|
||||
send_2(B,A, Cert(B), TNB, A,Text4, { TNB, A, Text3 }sk(B) );
|
||||
|
||||
claim(B,Commit,A,TNA,Text1);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
46
gui/Protocols/ISO-9798/isoiec-9798-3-4.spdl
Normal file
46
gui/Protocols/ISO-9798/isoiec-9798-3-4.spdl
Normal file
@ -0,0 +1,46 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* signature
|
||||
* three-pass
|
||||
* mutual
|
||||
*/
|
||||
const Cert: Function;
|
||||
|
||||
protocol isoiec-9798-3-4(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var RB: Nonce;
|
||||
fresh RA: Nonce;
|
||||
var Text1,Text4,Text5: Ticket;
|
||||
fresh Text2,Text3: Ticket;
|
||||
|
||||
recv_1(B,A, RB,Text1 );
|
||||
claim(A,Running,B,RA,RB,Text2);
|
||||
send_2(A,B, Cert(B), RA,RB,B,Text3, { RA, RB, B, Text2 }sk(A) );
|
||||
recv_3(B,A, Cert(A), RB,RA,A,Text5, { RB, RA, A, Text4 }sk(B) );
|
||||
|
||||
claim(A,Commit,B,RA,RB,Text2,Text4);
|
||||
claim(A,Alive);
|
||||
claim(A,Weakagree);
|
||||
}
|
||||
role B
|
||||
{
|
||||
fresh RB: Nonce;
|
||||
var RA: Nonce;
|
||||
fresh Text1,Text4,Text5: Ticket;
|
||||
var Text2,Text3: Ticket;
|
||||
|
||||
send_1(B,A, RB,Text1 );
|
||||
recv_2(A,B, Cert(B), RA,RB,B,Text3, { RA, RB, B, Text2 }sk(A) );
|
||||
claim(B,Running,A,RA,RB,Text2,Text4);
|
||||
send_3(B,A, Cert(A), RB,RA,A,Text5, { RB, RA, A, Text4 }sk(B) );
|
||||
|
||||
claim(B,Commit,A,RA,RB,Text2);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
49
gui/Protocols/ISO-9798/isoiec-9798-3-5.spdl
Normal file
49
gui/Protocols/ISO-9798/isoiec-9798-3-5.spdl
Normal file
@ -0,0 +1,49 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* signature
|
||||
* two-pass
|
||||
* mutual
|
||||
* parallel
|
||||
*/
|
||||
const Cert: Function;
|
||||
|
||||
protocol isoiec-9798-3-5(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh RA: Nonce;
|
||||
var RB: Nonce;
|
||||
fresh Text1,Text3,Text4: Ticket;
|
||||
var Text2,Text5,Text6: Ticket;
|
||||
|
||||
send_1(A,B, Cert(A), RA,Text1 );
|
||||
recv_2(B,A, Cert(B), RB,Text2 );
|
||||
recv_3(B,A, RB,RA,A,Text6, { RB, RA, A, Text5 }sk(B) );
|
||||
claim(A,Running,B,RA,RB,Text3,Text5);
|
||||
send_4(A,B, RA,RB,B,Text4, { RA, RB, B, Text3 }sk(A) );
|
||||
|
||||
claim(A,Commit,B,RA,RB,Text5);
|
||||
claim(A,Alive);
|
||||
claim(A,Weakagree);
|
||||
}
|
||||
role B
|
||||
{
|
||||
var RA: Nonce;
|
||||
fresh RB: Nonce;
|
||||
var Text1,Text3,Text4: Ticket;
|
||||
fresh Text2,Text5,Text6: Ticket;
|
||||
|
||||
recv_1(A,B, Cert(A), RA,Text1 );
|
||||
send_2(B,A, Cert(B), RB,Text2 );
|
||||
claim(B,Running,A,RA,RB,Text5);
|
||||
send_3(B,A, RB,RA,A,Text6, { RB, RA, A, Text5 }sk(B) );
|
||||
recv_4(A,B, RA,RB,B,Text4, { RA, RB, B, Text3 }sk(A) );
|
||||
|
||||
claim(B,Commit,A,RA,RB,Text3,Text5);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
12
gui/Protocols/ISO-9798/isoiec-9798-3-6-1.cpp
Normal file
12
gui/Protocols/ISO-9798/isoiec-9798-3-6-1.cpp
Normal file
@ -0,0 +1,12 @@
|
||||
#define NAME isoiec-9798-3-6-1
|
||||
#define IA A
|
||||
#define IB B
|
||||
#define ResA A,pk(A)
|
||||
#define ResB B,pk(B)
|
||||
#define TokenAB Text9,ResA,{Rb,ResA,Text5}sk(T),{Rb,Ra,B,A,Text8}sk(A)
|
||||
#define TokenBA Ra,Rb,Text3,{B,Ra,Rb,A,Text2}sk(B)
|
||||
#define TokenTA ResA,ResB,{Rpa,ResB,Text6}sk(T),{Rb,ResA,Text5}sk(T)
|
||||
|
||||
#include "isoiec-9798-3-6.template"
|
||||
|
||||
|
69
gui/Protocols/ISO-9798/isoiec-9798-3-6-1.spdl
Normal file
69
gui/Protocols/ISO-9798/isoiec-9798-3-6-1.spdl
Normal file
@ -0,0 +1,69 @@
|
||||
|
||||
|
||||
/*
|
||||
* Modeled from ISO standard
|
||||
*
|
||||
* signature
|
||||
* ttp
|
||||
* five-pass
|
||||
* mutual
|
||||
*
|
||||
* A initiates and also communicates with T
|
||||
*
|
||||
* parameters:
|
||||
*
|
||||
* NAME
|
||||
* IA
|
||||
* IB
|
||||
* ResA
|
||||
* ResB
|
||||
* TokenAB
|
||||
* TokenBA (although identical in both cases)
|
||||
* TokenTA
|
||||
*
|
||||
*/
|
||||
protocol isoiec-9798-3-6-1(A,B,T)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Ra,Rpa: Nonce;
|
||||
fresh Text1,Text4,Text8,Text9: Ticket;
|
||||
var Rb: Nonce;
|
||||
var Text2,Text3;
|
||||
var Text5,Text6,Text7: Ticket;
|
||||
|
||||
send_1(A,B, Ra,A,Text1);
|
||||
recv_2(B,A, B,Ra,Rb,Text3,{B,Ra,Rb,A,Text2}sk(B));
|
||||
send_3(A,T, Rpa,Rb,A,B,Text4);
|
||||
recv_4(T,A, Text7,A,pk(A),B,pk(B),{Rpa,B,pk(B),Text6}sk(T),{Rb,A,pk(A),Text5}sk(T));
|
||||
claim(A,Running,B,Ra,Rb,Text8);
|
||||
send_5(A,B, Text9,A,pk(A),{Rb,A,pk(A),Text5}sk(T),{Rb,Ra,B,A,Text8}sk(A));
|
||||
|
||||
claim(A,Commit,B,Ra,Rb,Text2);
|
||||
claim(A,Alive);
|
||||
}
|
||||
role B
|
||||
{
|
||||
var Ra,Rpa: Nonce;
|
||||
var Text1,Text5,Text8,Text9: Ticket;
|
||||
fresh Text2,Text3,Text4: Ticket;
|
||||
fresh Rb: Nonce;
|
||||
|
||||
recv_1(A,B, Ra,A,Text1);
|
||||
claim(B,Running,A,Ra,Rb,Text2);
|
||||
send_2(B,A, B,Ra,Rb,Text3,{B,Ra,Rb,A,Text2}sk(B));
|
||||
recv_5(A,B, Text9,A,pk(A),{Rb,A,pk(A),Text5}sk(T),{Rb,Ra,B,A,Text8}sk(A));
|
||||
|
||||
claim(B,Commit,A,Ra,Rb,Text8);
|
||||
claim(B,Alive);
|
||||
}
|
||||
role T
|
||||
{
|
||||
var Rpa, Rb: Nonce;
|
||||
var Text4: Ticket;
|
||||
fresh Text5,Text6,Text7: Ticket;
|
||||
|
||||
recv_3(A,T, Rpa,Rb,A,B,Text4);
|
||||
send_4(T,A, Text7,A,pk(A),B,pk(B),{Rpa,B,pk(B),Text6}sk(T),{Rb,A,pk(A),Text5}sk(T));
|
||||
}
|
||||
}
|
12
gui/Protocols/ISO-9798/isoiec-9798-3-6-2.cpp
Normal file
12
gui/Protocols/ISO-9798/isoiec-9798-3-6-2.cpp
Normal file
@ -0,0 +1,12 @@
|
||||
#define NAME isoiec-9798-3-6-2
|
||||
#define IA A
|
||||
#define IB B
|
||||
#define ResA A,pk(A)
|
||||
#define ResB B,pk(B)
|
||||
#define TokenAB Rpa,Text9,TokenTA,{Rb,Ra,B,A,Text8}sk(A)
|
||||
#define TokenBA Ra,Rb,Text3,{B,Ra,Rb,A,Text2}sk(B)
|
||||
#define TokenTA ResA,ResB,{Rpa,Rb,ResA,ResB,Text5}sk(T)
|
||||
|
||||
#include "isoiec-9798-3-6.template"
|
||||
|
||||
|
69
gui/Protocols/ISO-9798/isoiec-9798-3-6-2.spdl
Normal file
69
gui/Protocols/ISO-9798/isoiec-9798-3-6-2.spdl
Normal file
@ -0,0 +1,69 @@
|
||||
|
||||
|
||||
/*
|
||||
* Modeled from ISO standard
|
||||
*
|
||||
* signature
|
||||
* ttp
|
||||
* five-pass
|
||||
* mutual
|
||||
*
|
||||
* A initiates and also communicates with T
|
||||
*
|
||||
* parameters:
|
||||
*
|
||||
* NAME
|
||||
* IA
|
||||
* IB
|
||||
* ResA
|
||||
* ResB
|
||||
* TokenAB
|
||||
* TokenBA (although identical in both cases)
|
||||
* TokenTA
|
||||
*
|
||||
*/
|
||||
protocol isoiec-9798-3-6-2(A,B,T)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Ra,Rpa: Nonce;
|
||||
fresh Text1,Text4,Text8,Text9: Ticket;
|
||||
var Rb: Nonce;
|
||||
var Text2,Text3;
|
||||
var Text5,Text6,Text7: Ticket;
|
||||
|
||||
send_1(A,B, Ra,A,Text1);
|
||||
recv_2(B,A, B,Ra,Rb,Text3,{B,Ra,Rb,A,Text2}sk(B));
|
||||
send_3(A,T, Rpa,Rb,A,B,Text4);
|
||||
recv_4(T,A, Text7,A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text5}sk(T));
|
||||
claim(A,Running,B,Ra,Rb,Text8);
|
||||
send_5(A,B, Rpa,Text9,A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text5}sk(T),{Rb,Ra,B,A,Text8}sk(A));
|
||||
|
||||
claim(A,Commit,B,Ra,Rb,Text2);
|
||||
claim(A,Alive);
|
||||
}
|
||||
role B
|
||||
{
|
||||
var Ra,Rpa: Nonce;
|
||||
var Text1,Text5,Text8,Text9: Ticket;
|
||||
fresh Text2,Text3,Text4: Ticket;
|
||||
fresh Rb: Nonce;
|
||||
|
||||
recv_1(A,B, Ra,A,Text1);
|
||||
claim(B,Running,A,Ra,Rb,Text2);
|
||||
send_2(B,A, B,Ra,Rb,Text3,{B,Ra,Rb,A,Text2}sk(B));
|
||||
recv_5(A,B, Rpa,Text9,A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text5}sk(T),{Rb,Ra,B,A,Text8}sk(A));
|
||||
|
||||
claim(B,Commit,A,Ra,Rb,Text8);
|
||||
claim(B,Alive);
|
||||
}
|
||||
role T
|
||||
{
|
||||
var Rpa, Rb: Nonce;
|
||||
var Text4: Ticket;
|
||||
fresh Text5,Text6,Text7: Ticket;
|
||||
|
||||
recv_3(A,T, Rpa,Rb,A,B,Text4);
|
||||
send_4(T,A, Text7,A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text5}sk(T));
|
||||
}
|
||||
}
|
68
gui/Protocols/ISO-9798/isoiec-9798-3-6.template
Normal file
68
gui/Protocols/ISO-9798/isoiec-9798-3-6.template
Normal file
@ -0,0 +1,68 @@
|
||||
/*
|
||||
* Modeled from ISO standard
|
||||
*
|
||||
* signature
|
||||
* ttp
|
||||
* five-pass
|
||||
* mutual
|
||||
*
|
||||
* A initiates and also communicates with T
|
||||
*
|
||||
* parameters:
|
||||
*
|
||||
* NAME
|
||||
* IA
|
||||
* IB
|
||||
* ResA
|
||||
* ResB
|
||||
* TokenAB
|
||||
* TokenBA (although identical in both cases)
|
||||
* TokenTA
|
||||
*
|
||||
*/
|
||||
protocol NAME(A,B,T)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Ra,Rpa: Nonce;
|
||||
fresh Text1,Text4,Text8,Text9: Ticket;
|
||||
var Rb: Nonce;
|
||||
var Text2,Text3;
|
||||
var Text5,Text6,Text7: Ticket;
|
||||
|
||||
send_1(A,B, Ra,IA,Text1);
|
||||
recv_2(B,A, IB,TokenBA);
|
||||
send_3(A,T, Rpa,Rb,IA,IB,Text4);
|
||||
recv_4(T,A, Text7,TokenTA);
|
||||
claim(A,Running,B,Ra,Rb,Text8);
|
||||
send_5(A,B, TokenAB);
|
||||
|
||||
claim(A,Commit,B,Ra,Rb,Text2);
|
||||
claim(A,Alive);
|
||||
}
|
||||
role B
|
||||
{
|
||||
var Ra,Rpa: Nonce;
|
||||
var Text1,Text5,Text8,Text9: Ticket;
|
||||
fresh Text2,Text3,Text4: Ticket;
|
||||
fresh Rb: Nonce;
|
||||
|
||||
recv_1(A,B, Ra,IA,Text1);
|
||||
claim(B,Running,A,Ra,Rb,Text2);
|
||||
send_2(B,A, IB,TokenBA);
|
||||
recv_5(A,B, TokenAB);
|
||||
|
||||
claim(B,Commit,A,Ra,Rb,Text8);
|
||||
claim(B,Alive);
|
||||
}
|
||||
role T
|
||||
{
|
||||
var Rpa, Rb: Nonce;
|
||||
var Text4: Ticket;
|
||||
fresh Text5,Text6,Text7: Ticket;
|
||||
|
||||
recv_3(A,T, Rpa,Rb,IA,IB,Text4);
|
||||
send_4(T,A, Text7,TokenTA);
|
||||
}
|
||||
}
|
||||
|
12
gui/Protocols/ISO-9798/isoiec-9798-3-7-1.cpp
Normal file
12
gui/Protocols/ISO-9798/isoiec-9798-3-7-1.cpp
Normal file
@ -0,0 +1,12 @@
|
||||
#define NAME isoiec-9798-3-7-1
|
||||
#define IA A
|
||||
#define IB B
|
||||
#define ResA A,pk(A)
|
||||
#define ResB B,pk(B)
|
||||
#define TokenAB Text7,Ra,ResA,{Rb,ResA,Text3}sk(T),{Rb,Ra,B,A,Text6}sk(A)
|
||||
#define TokenBA Ra,Rb,Text9,{A,Ra,Rb,B,Text8}sk(B)
|
||||
#define TokenTA ResA,ResB,{Rpa,ResB,Text4}sk(T),{Rb,ResA,Text3}sk(T)
|
||||
|
||||
#include "isoiec-9798-3-7.template"
|
||||
|
||||
|
66
gui/Protocols/ISO-9798/isoiec-9798-3-7-1.spdl
Normal file
66
gui/Protocols/ISO-9798/isoiec-9798-3-7-1.spdl
Normal file
@ -0,0 +1,66 @@
|
||||
/*
|
||||
* Modeled from ISO standard
|
||||
*
|
||||
* signature
|
||||
* ttp
|
||||
* five-pass
|
||||
* mutual
|
||||
*
|
||||
* B initiates and A communicates with T
|
||||
*
|
||||
* parameters:
|
||||
*
|
||||
* NAME
|
||||
* IA
|
||||
* IB
|
||||
* ResA
|
||||
* ResB
|
||||
* TokenAB
|
||||
* TokenBA (although identical in both cases)
|
||||
* TokenTA
|
||||
*
|
||||
*/
|
||||
protocol isoiec-9798-3-7-1(A,B,T)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Ra,Rpa: Nonce;
|
||||
var Rb: Nonce;
|
||||
var Text1,Text3,Text4,Text5,Text8,Text9: Ticket;
|
||||
fresh Text2,Text6,Text7: Ticket;
|
||||
|
||||
recv_1(B,A, Rb,B,Text1 );
|
||||
send_2(A,T, Rpa,Rb,A,Text2 );
|
||||
recv_3(T,A, Text5, A,pk(A),B,pk(B),{Rpa,B,pk(B),Text4}sk(T),{Rb,A,pk(A),Text3}sk(T) );
|
||||
claim(A,Running,B,Ra,Rb,Text6);
|
||||
send_4(A,B, A, Text7,Ra,A,pk(A),{Rb,A,pk(A),Text3}sk(T),{Rb,Ra,B,A,Text6}sk(A) );
|
||||
recv_5(B,A, Ra,Rb,Text9,{A,Ra,Rb,B,Text8}sk(B) );
|
||||
|
||||
claim(A,Commit,B,Ra,Rb,Text8);
|
||||
claim(A,Alive);
|
||||
}
|
||||
role B
|
||||
{
|
||||
fresh Text1,Text8,Text9: Ticket;
|
||||
fresh Rb: Nonce;
|
||||
var Text3,Text4,Text6,Text7: Ticket;
|
||||
var Ra,Rpa: Nonce;
|
||||
|
||||
send_1(B,A, Rb,B,Text1 );
|
||||
recv_4(A,B, A, Text7,Ra,A,pk(A),{Rb,A,pk(A),Text3}sk(T),{Rb,Ra,B,A,Text6}sk(A) );
|
||||
claim(B,Running,A,Ra,Rb,Text8);
|
||||
send_5(B,A, Ra,Rb,Text9,{A,Ra,Rb,B,Text8}sk(B) );
|
||||
|
||||
claim(B,Commit,A,Ra,Rb,Text6);
|
||||
claim(B,Alive);
|
||||
}
|
||||
role T
|
||||
{
|
||||
var Rpa,Rb: Nonce;
|
||||
var Text2: Ticket;
|
||||
fresh Text3,Text4,Text5: Ticket;
|
||||
|
||||
recv_2(A,T, Rpa,Rb,A,Text2 );
|
||||
send_3(T,A, Text5, A,pk(A),B,pk(B),{Rpa,B,pk(B),Text4}sk(T),{Rb,A,pk(A),Text3}sk(T) );
|
||||
}
|
||||
}
|
12
gui/Protocols/ISO-9798/isoiec-9798-3-7-2.cpp
Normal file
12
gui/Protocols/ISO-9798/isoiec-9798-3-7-2.cpp
Normal file
@ -0,0 +1,12 @@
|
||||
#define NAME isoiec-9798-3-7-2
|
||||
#define IA A
|
||||
#define IB B
|
||||
#define ResA A,pk(A)
|
||||
#define ResB B,pk(B)
|
||||
#define TokenAB Rpa,Text7,TokenTA,{Rb,Ra,B,A,Text6}sk(A)
|
||||
#define TokenBA Ra,Rb,Text9,{Ra,Rb,A,B,Text8}sk(B)
|
||||
#define TokenTA ResA,ResB,{Rpa,Rb,ResA,ResB,Text3}sk(T)
|
||||
|
||||
#include "isoiec-9798-3-7.template"
|
||||
|
||||
|
68
gui/Protocols/ISO-9798/isoiec-9798-3-7-2.spdl
Normal file
68
gui/Protocols/ISO-9798/isoiec-9798-3-7-2.spdl
Normal file
@ -0,0 +1,68 @@
|
||||
|
||||
|
||||
/*
|
||||
* Modeled from ISO standard
|
||||
*
|
||||
* signature
|
||||
* ttp
|
||||
* five-pass
|
||||
* mutual
|
||||
*
|
||||
* B initiates and A communicates with T
|
||||
*
|
||||
* parameters:
|
||||
*
|
||||
* NAME
|
||||
* IA
|
||||
* IB
|
||||
* ResA
|
||||
* ResB
|
||||
* TokenAB
|
||||
* TokenBA (although identical in both cases)
|
||||
* TokenTA
|
||||
*
|
||||
*/
|
||||
protocol isoiec-9798-3-7-2(A,B,T)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Ra,Rpa: Nonce;
|
||||
var Rb: Nonce;
|
||||
var Text1,Text3,Text4,Text5,Text8,Text9: Ticket;
|
||||
fresh Text2,Text6,Text7: Ticket;
|
||||
|
||||
recv_1(B,A, Rb,B,Text1 );
|
||||
send_2(A,T, Rpa,Rb,A,Text2 );
|
||||
recv_3(T,A, Text5, A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text3}sk(T) );
|
||||
claim(A,Running,B,Ra,Rb,Text6);
|
||||
send_4(A,B, A, Rpa,Text7,A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text3}sk(T),{Rb,Ra,B,A,Text6}sk(A) );
|
||||
recv_5(B,A, Ra,Rb,Text9,{Ra,Rb,A,B,Text8}sk(B) );
|
||||
|
||||
claim(A,Commit,B,Ra,Rb,Text8);
|
||||
claim(A,Alive);
|
||||
}
|
||||
role B
|
||||
{
|
||||
fresh Text1,Text8,Text9: Ticket;
|
||||
fresh Rb: Nonce;
|
||||
var Text3,Text4,Text6,Text7: Ticket;
|
||||
var Ra,Rpa: Nonce;
|
||||
|
||||
send_1(B,A, Rb,B,Text1 );
|
||||
recv_4(A,B, A, Rpa,Text7,A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text3}sk(T),{Rb,Ra,B,A,Text6}sk(A) );
|
||||
claim(B,Running,A,Ra,Rb,Text8);
|
||||
send_5(B,A, Ra,Rb,Text9,{Ra,Rb,A,B,Text8}sk(B) );
|
||||
|
||||
claim(B,Commit,A,Ra,Rb,Text6);
|
||||
claim(B,Alive);
|
||||
}
|
||||
role T
|
||||
{
|
||||
var Rpa,Rb: Nonce;
|
||||
var Text2: Ticket;
|
||||
fresh Text3,Text4,Text5: Ticket;
|
||||
|
||||
recv_2(A,T, Rpa,Rb,A,Text2 );
|
||||
send_3(T,A, Text5, A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text3}sk(T) );
|
||||
}
|
||||
}
|
67
gui/Protocols/ISO-9798/isoiec-9798-3-7.template
Normal file
67
gui/Protocols/ISO-9798/isoiec-9798-3-7.template
Normal file
@ -0,0 +1,67 @@
|
||||
/*
|
||||
* Modeled from ISO standard
|
||||
*
|
||||
* signature
|
||||
* ttp
|
||||
* five-pass
|
||||
* mutual
|
||||
*
|
||||
* B initiates and A communicates with T
|
||||
*
|
||||
* parameters:
|
||||
*
|
||||
* NAME
|
||||
* IA
|
||||
* IB
|
||||
* ResA
|
||||
* ResB
|
||||
* TokenAB
|
||||
* TokenBA (although identical in both cases)
|
||||
* TokenTA
|
||||
*
|
||||
*/
|
||||
protocol NAME(A,B,T)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Ra,Rpa: Nonce;
|
||||
var Rb: Nonce;
|
||||
var Text1,Text3,Text4,Text5,Text8,Text9: Ticket;
|
||||
fresh Text2,Text6,Text7: Ticket;
|
||||
|
||||
recv_1(B,A, Rb,IB,Text1 );
|
||||
send_2(A,T, Rpa,Rb,IA,Text2 );
|
||||
recv_3(T,A, Text5, TokenTA );
|
||||
claim(A,Running,B,Ra,Rb,Text6);
|
||||
send_4(A,B, IA, TokenAB );
|
||||
recv_5(B,A, TokenBA );
|
||||
|
||||
claim(A,Commit,B,Ra,Rb,Text8);
|
||||
claim(A,Alive);
|
||||
}
|
||||
role B
|
||||
{
|
||||
fresh Text1,Text8,Text9: Ticket;
|
||||
fresh Rb: Nonce;
|
||||
var Text3,Text4,Text6,Text7: Ticket;
|
||||
var Ra,Rpa: Nonce;
|
||||
|
||||
send_1(B,A, Rb,IB,Text1 );
|
||||
recv_4(A,B, IA, TokenAB );
|
||||
claim(B,Running,A,Ra,Rb,Text8);
|
||||
send_5(B,A, TokenBA );
|
||||
|
||||
claim(B,Commit,A,Ra,Rb,Text6);
|
||||
claim(B,Alive);
|
||||
}
|
||||
role T
|
||||
{
|
||||
var Rpa,Rb: Nonce;
|
||||
var Text2: Ticket;
|
||||
fresh Text3,Text4,Text5: Ticket;
|
||||
|
||||
recv_2(A,T, Rpa,Rb,IA,Text2 );
|
||||
send_3(T,A, Text5, TokenTA );
|
||||
}
|
||||
}
|
||||
|
39
gui/Protocols/ISO-9798/isoiec-9798-4-1-udkey.spdl
Normal file
39
gui/Protocols/ISO-9798/isoiec-9798-4-1-udkey.spdl
Normal file
@ -0,0 +1,39 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* ccf
|
||||
* one-pass
|
||||
* unilateral
|
||||
*
|
||||
* Unidirectional key version.
|
||||
*
|
||||
* Modeling notes:
|
||||
*
|
||||
* - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
|
||||
*/
|
||||
hashfunction f;
|
||||
|
||||
protocol isoiec-9798-4-1-udkey(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Text1,Text2: Ticket;
|
||||
fresh TNA: Nonce;
|
||||
|
||||
claim(A,Running,B,TNA,Text1);
|
||||
send_1(A,B, TNA, Text2, f( TNA, Text1 ,k(A,B) ) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
var TNA: Nonce;
|
||||
var Text1,Text2: Ticket;
|
||||
|
||||
recv_1(A,B, TNA, Text2, f( TNA, Text1 ,k(A,B) ) );
|
||||
|
||||
claim(B,Commit,A,TNA,Text1);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
58
gui/Protocols/ISO-9798/isoiec-9798-4-1.spdl
Normal file
58
gui/Protocols/ISO-9798/isoiec-9798-4-1.spdl
Normal file
@ -0,0 +1,58 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010, Feb. 2011.
|
||||
*
|
||||
* History:
|
||||
*
|
||||
* - v2.0, Feb. 2011:
|
||||
* Added key symmetry emulation protocol.
|
||||
*
|
||||
* ccf
|
||||
* one-pass
|
||||
* unilateral
|
||||
*
|
||||
* The identifier B is optional and may be omitted if the key is unidirectional.
|
||||
*
|
||||
* Modeling notes:
|
||||
*
|
||||
* - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
|
||||
*/
|
||||
hashfunction f;
|
||||
|
||||
protocol @keysymm-41(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var X,Y,Z: Ticket;
|
||||
|
||||
recv_!1(B,A, f(X,Y,Z, k(A,B) ) );
|
||||
send_!2(A,B, f(X,Y,Z, k(B,A) ) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
}
|
||||
}
|
||||
|
||||
protocol isoiec-9798-4-1(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Text1,Text2: Ticket;
|
||||
fresh TNA: Nonce;
|
||||
|
||||
claim(A,Running,B,TNA,Text1);
|
||||
send_1(A,B, TNA, Text2, f( TNA, B, Text1 ,k(A,B) ) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
var TNA: Nonce;
|
||||
var Text1,Text2: Ticket;
|
||||
|
||||
recv_1(A,B, TNA, Text2, f( TNA, B, Text1 ,k(A,B) ) );
|
||||
|
||||
claim(B,Commit,A,TNA,Text1);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
43
gui/Protocols/ISO-9798/isoiec-9798-4-2-udkey.spdl
Normal file
43
gui/Protocols/ISO-9798/isoiec-9798-4-2-udkey.spdl
Normal file
@ -0,0 +1,43 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* ccf
|
||||
* unilateral
|
||||
* two-pass
|
||||
*
|
||||
* Unidirectional key version.
|
||||
*
|
||||
* Modeling notes:
|
||||
*
|
||||
* - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
|
||||
*/
|
||||
hashfunction f;
|
||||
|
||||
protocol isoiec-9798-4-2-udkey(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var Rb: Nonce;
|
||||
var Text1: Ticket;
|
||||
fresh Text2,Text3: Ticket;
|
||||
|
||||
recv_1(B,A, Rb,Text1 );
|
||||
claim(A,Running,B,Rb,Text2);
|
||||
send_2(A,B, Text3, f( Rb, Text2, k(A,B)) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
fresh Rb: Nonce;
|
||||
fresh Text1: Ticket;
|
||||
var Text2,Text3: Ticket;
|
||||
|
||||
send_1(B,A, Rb,Text1 );
|
||||
recv_2(A,B, Text3, f( Rb, Text2, k(A,B)) );
|
||||
|
||||
claim(B,Commit,A,Rb,Text2);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
62
gui/Protocols/ISO-9798/isoiec-9798-4-2.spdl
Normal file
62
gui/Protocols/ISO-9798/isoiec-9798-4-2.spdl
Normal file
@ -0,0 +1,62 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010, Feb. 2011.
|
||||
*
|
||||
* History:
|
||||
*
|
||||
* - v2.0, Feb. 2011:
|
||||
* Added key symmetry emulation protocol.
|
||||
*
|
||||
* ccf
|
||||
* unilateral
|
||||
* two-pass
|
||||
*
|
||||
* The identifier B is optional and may be omitted if the key is unidirectional.
|
||||
*
|
||||
* Modeling notes:
|
||||
*
|
||||
* - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
|
||||
*/
|
||||
hashfunction f;
|
||||
|
||||
protocol @keysymm-42(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var X,Y,Z: Ticket;
|
||||
|
||||
recv_!1(B,A, f(X,Y,Z, k(A,B) ) );
|
||||
send_!2(A,B, f(X,Y,Z, k(B,A) ) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
}
|
||||
}
|
||||
|
||||
protocol isoiec-9798-4-2(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var Rb: Nonce;
|
||||
var Text1: Ticket;
|
||||
fresh Text2,Text3: Ticket;
|
||||
|
||||
recv_1(B,A, Rb,Text1 );
|
||||
claim(A,Running,B,Rb,Text2);
|
||||
send_2(A,B, Text3, f( Rb, B, Text2, k(A,B)) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
fresh Rb: Nonce;
|
||||
fresh Text1: Ticket;
|
||||
var Text2,Text3: Ticket;
|
||||
|
||||
send_1(B,A, Rb,Text1 );
|
||||
recv_2(A,B, Text3, f( Rb, B, Text2, k(A,B)) );
|
||||
|
||||
claim(B,Commit,A,Rb,Text2);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
50
gui/Protocols/ISO-9798/isoiec-9798-4-3-udkey.spdl
Normal file
50
gui/Protocols/ISO-9798/isoiec-9798-4-3-udkey.spdl
Normal file
@ -0,0 +1,50 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* ccf
|
||||
* two-pass
|
||||
* mutual
|
||||
*
|
||||
* Unidirectional key version.
|
||||
*
|
||||
* Modeling notes:
|
||||
*
|
||||
* - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
|
||||
*/
|
||||
hashfunction f;
|
||||
|
||||
protocol isoiec-9798-4-3-udkey(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Text1,Text2: Ticket;
|
||||
var Text3,Text4: Ticket;
|
||||
fresh TNa: Nonce;
|
||||
var TNb: Nonce;
|
||||
|
||||
claim(A,Running,B,TNa,Text1);
|
||||
send_1(A,B, TNa, Text2, f(TNa,Text1, k(A,B) ) );
|
||||
recv_2(B,A, TNb, Text4, f(TNb,Text3, k(B,A) ) );
|
||||
|
||||
claim(A,Commit,B,TNb,Text3);
|
||||
claim(A,Alive);
|
||||
claim(A,Weakagree);
|
||||
}
|
||||
role B
|
||||
{
|
||||
var TNa: Nonce;
|
||||
fresh TNb: Nonce;
|
||||
var Text1,Text2: Ticket;
|
||||
fresh Text3,Text4: Ticket;
|
||||
|
||||
recv_1(A,B, TNa, Text2, f(TNa,Text1, k(A,B) ) );
|
||||
claim(B,Running,A,TNb,Text3);
|
||||
send_2(B,A, TNb, Text4, f(TNb,Text3, k(B,A) ) );
|
||||
|
||||
claim(B,Commit,A,TNa,Text1);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
69
gui/Protocols/ISO-9798/isoiec-9798-4-3.spdl
Normal file
69
gui/Protocols/ISO-9798/isoiec-9798-4-3.spdl
Normal file
@ -0,0 +1,69 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010, Feb. 2011.
|
||||
*
|
||||
* History:
|
||||
*
|
||||
* - v2.0, Feb. 2011:
|
||||
* Added key symmetry emulation protocol.
|
||||
*
|
||||
* ccf
|
||||
* two-pass
|
||||
* mutual
|
||||
*
|
||||
* The identifiers B,A are optional and may be (independently) be omitted if the key is unidirectional.
|
||||
*
|
||||
* Modeling notes:
|
||||
*
|
||||
* - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
|
||||
*/
|
||||
hashfunction f;
|
||||
|
||||
protocol @keysymm-43(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var X,Y,Z: Ticket;
|
||||
|
||||
recv_!1(B,A, f(X,Y,Z, k(A,B) ) );
|
||||
send_!2(A,B, f(X,Y,Z, k(B,A) ) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
}
|
||||
}
|
||||
|
||||
protocol isoiec-9798-4-3(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Text1,Text2: Ticket;
|
||||
var Text3,Text4: Ticket;
|
||||
fresh TNa: Nonce;
|
||||
var TNb: Nonce;
|
||||
|
||||
claim(A,Running,B,TNa,Text1);
|
||||
send_1(A,B, TNa, Text2, f(TNa,B,Text1, k(A,B) ) );
|
||||
recv_2(B,A, TNb, Text4, f(TNb,A,Text3, k(A,B) ) );
|
||||
|
||||
claim(A,Commit,B,TNb,Text3);
|
||||
claim(A,Alive);
|
||||
claim(A,Weakagree);
|
||||
}
|
||||
role B
|
||||
{
|
||||
var TNa: Nonce;
|
||||
fresh TNb: Nonce;
|
||||
var Text1,Text2: Ticket;
|
||||
fresh Text3,Text4: Ticket;
|
||||
|
||||
recv_1(A,B, TNa, Text2, f(TNa,B,Text1, k(A,B) ) );
|
||||
claim(B,Running,A,TNb,Text3);
|
||||
send_2(B,A, TNb, Text4, f(TNb,A,Text3, k(A,B) ) );
|
||||
|
||||
claim(B,Commit,A,TNa,Text1);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
52
gui/Protocols/ISO-9798/isoiec-9798-4-4-udkey.spdl
Normal file
52
gui/Protocols/ISO-9798/isoiec-9798-4-4-udkey.spdl
Normal file
@ -0,0 +1,52 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010
|
||||
*
|
||||
* ccf
|
||||
* mutual
|
||||
* three-pass
|
||||
*
|
||||
* Unidirectional key version.
|
||||
*
|
||||
* Modeling notes:
|
||||
*
|
||||
* - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
|
||||
*/
|
||||
hashfunction f;
|
||||
|
||||
protocol isoiec-9798-4-4-udkey(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Ra: Nonce;
|
||||
var Rb: Nonce;
|
||||
var Text1,Text4,Text5: Ticket;
|
||||
fresh Text2,Text3: Ticket;
|
||||
|
||||
recv_1(B,A, Rb, Text1 );
|
||||
claim(A,Running,B,Ra,Rb,Text2);
|
||||
send_2(A,B, Ra, Text3, f(Ra,Rb,Text2, k(A,B) ) );
|
||||
recv_3(B,A, Text5, f(Rb,Ra,Text4, k(B,A) ) );
|
||||
|
||||
claim(A,Commit,B,Ra,Rb,Text2,Text4);
|
||||
claim(A,Alive);
|
||||
claim(A,Weakagree);
|
||||
}
|
||||
role B
|
||||
{
|
||||
var Ra: Nonce;
|
||||
fresh Rb: Nonce;
|
||||
fresh Text1,Text4,Text5: Ticket;
|
||||
var Text2,Text3: Ticket;
|
||||
|
||||
send_1(B,A, Rb, Text1 );
|
||||
recv_2(A,B, Ra, Text3, f(Ra,Rb,Text2, k(A,B) ) );
|
||||
claim(B,Running,A,Ra,Rb,Text2,Text4);
|
||||
send_3(B,A, Text5, f(Rb,Ra,Text4, k(B,A) ) );
|
||||
|
||||
claim(B,Commit,A,Ra,Rb,Text2);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
75
gui/Protocols/ISO-9798/isoiec-9798-4-4.spdl
Normal file
75
gui/Protocols/ISO-9798/isoiec-9798-4-4.spdl
Normal file
@ -0,0 +1,75 @@
|
||||
/*
|
||||
* Modeled from ISO/IEC 9798
|
||||
* Modeler: Cas Cremers, Dec. 2010, Feb. 2011.
|
||||
*
|
||||
* History:
|
||||
*
|
||||
* - v2.0, Feb. 2011:
|
||||
* Added key symmetry emulation protocol.
|
||||
*
|
||||
* ccf
|
||||
* mutual
|
||||
* three-pass
|
||||
*
|
||||
* The identifier B is optional and may be omitted if the key is unidirectional.
|
||||
*
|
||||
* Modeling notes:
|
||||
*
|
||||
* - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
|
||||
*/
|
||||
hashfunction f;
|
||||
|
||||
protocol @keysymm-44(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
var X,Y,Z: Ticket;
|
||||
|
||||
recv_!1(B,A, f(X,Y,Z, k(A,B) ) );
|
||||
send_!2(A,B, f(X,Y,Z, k(B,A) ) );
|
||||
}
|
||||
role B
|
||||
{
|
||||
var X,Y,Z,ZZ: Ticket;
|
||||
|
||||
recv_!3(A,B, f(X,Y,Z,ZZ, k(A,B) ) );
|
||||
send_!4(B,A, f(X,Y,Z,ZZ, k(B,A) ) );
|
||||
}
|
||||
}
|
||||
|
||||
protocol isoiec-9798-4-4(A,B)
|
||||
{
|
||||
role A
|
||||
{
|
||||
fresh Ra: Nonce;
|
||||
var Rb: Nonce;
|
||||
var Text1,Text4,Text5: Ticket;
|
||||
fresh Text2,Text3: Ticket;
|
||||
|
||||
recv_1(B,A, Rb, Text1 );
|
||||
claim(A,Running,B,Ra,Rb,Text2);
|
||||
send_2(A,B, Ra, Text3, f(Ra,Rb,B,Text2, k(A,B) ) );
|
||||
recv_3(B,A, Text5, f(Rb,Ra,Text4, k(A,B) ) );
|
||||
|
||||
claim(A,Commit,B,Ra,Rb,Text2,Text4);
|
||||
claim(A,Alive);
|
||||
claim(A,Weakagree);
|
||||
}
|
||||
role B
|
||||
{
|
||||
var Ra: Nonce;
|
||||
fresh Rb: Nonce;
|
||||
fresh Text1,Text4,Text5: Ticket;
|
||||
var Text2,Text3: Ticket;
|
||||
|
||||
send_1(B,A, Rb, Text1 );
|
||||
recv_2(A,B, Ra, Text3, f(Ra,Rb,B,Text2, k(A,B) ) );
|
||||
claim(B,Running,A,Ra,Rb,Text2,Text4);
|
||||
send_3(B,A, Text5, f(Rb,Ra,Text4, k(A,B) ) );
|
||||
|
||||
claim(B,Commit,A,Ra,Rb,Text2);
|
||||
claim(B,Alive);
|
||||
claim(B,Weakagree);
|
||||
}
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user