andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Replaced all tabs by spaces.

Browse Source
This commit is contained in:
gijs 2005-05-23 12:35:58 +00:00
parent b05843d690
commit 3cb999f820
39 changed files with 893 additions and 893 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
spdl/SPORE/andrew-ban-concrete.spdl
View File

@ -24,33 +24,33 @@ secret k: Function;
protocol andrewConcrete(I,R) protocol andrewConcrete(I,R)
{ {
role I role I
{ {
const ni: Nonce; const ni: Nonce;
var nr: Nonce; var nr: Nonce;
var kir: SessionKey; var kir: SessionKey;
send_1(I,R, I,ni ); send_1(I,R, I,ni );
read_2(R,I, {ni,kir}k(I,R) ); read_2(R,I, {ni,kir}k(I,R) );
send_3(I,R, {ni}kir); send_3(I,R, {ni}kir);
claim_4(I,Secret,kir); claim_4(I,Secret,kir);
claim_5(I,Nisynch); claim_5(I,Nisynch);
read_6(R,I, nr); read_6(R,I, nr);
} }
role R role R
{ {
var ni: Nonce; var ni: Nonce;
const nr: Nonce; const nr: Nonce;
const kir: SessionKey; const kir: SessionKey;
read_1(I,R, I,ni ); read_1(I,R, I,ni );
send_2(R,I, {ni,kir}k(I,R) ); send_2(R,I, {ni,kir}k(I,R) );
read_3(I,R, {ni}kir); read_3(I,R, {ni}kir);
send_6(R,I, nr); send_6(R,I, nr);
claim_7(R,Secret,kir); claim_7(R,Secret,kir);
claim_8(R,Nisynch); claim_8(R,Nisynch);
} }
} }
const Alice,Bob,Eve: Agent; const Alice,Bob,Eve: Agent;

58
spdl/SPORE/andrew-ban.spdl
View File

@ -16,37 +16,37 @@ secret k: Function;
protocol andrewBan(I,R) protocol andrewBan(I,R)
{ {
role I role I
{ {
const ni: Nonce; const ni: Nonce;
var nr,nr2: Nonce; var nr,nr2: Nonce;
var kir: SessionKey; var kir: SessionKey;
send_1(I,R, I,{ni}k(I,R) ); send_1(I,R, I,{ni}k(I,R) );
read_2(R,I, {ni,nr}k(I,R) ); read_2(R,I, {ni,nr}k(I,R) );
send_3(I,R, {nr}k(I,R) ); send_3(I,R, {nr}k(I,R) );
read_4(R,I, {kir,nr2,ni}k(I,R) ); read_4(R,I, {kir,nr2,ni}k(I,R) );
claim_5(I,Nisynch); claim_5(I,Nisynch);
claim_5b(I,Niagree); claim_5b(I,Niagree);
claim_6(I,Secret, kir); claim_6(I,Secret, kir);
claim_7(I,Secret, k(I,R)); claim_7(I,Secret, k(I,R));
} }
role R role R
{ {
var ni: Nonce; var ni: Nonce;
const nr,nr2: Nonce; const nr,nr2: Nonce;
const kir: SessionKey; const kir: SessionKey;
read_1(I,R, I,{ni}k(I,R) ); read_1(I,R, I,{ni}k(I,R) );
send_2(R,I, {ni,nr}k(I,R) ); send_2(R,I, {ni,nr}k(I,R) );
read_3(I,R, {nr}k(I,R) ); read_3(I,R, {nr}k(I,R) );
send_4(R,I, {kir,nr2,ni}k(I,R) ); send_4(R,I, {kir,nr2,ni}k(I,R) );
claim_8(R,Nisynch); claim_8(R,Nisynch);
claim_8b(R,Niagree); claim_8b(R,Niagree);
claim_9(R,Secret, kir); claim_9(R,Secret, kir);
claim_10(R,Secret, k(I,R)); claim_10(R,Secret, k(I,R));
} }
} }
const Alice,Bob,Eve: Agent; const Alice,Bob,Eve: Agent;

50
spdl/SPORE/andrew-lowe-ban.spdl
View File

@ -23,33 +23,33 @@ secret k: Function;
protocol andrewLoweBan(I,R) protocol andrewLoweBan(I,R)
{ {
role I role I
{ {
const ni: Nonce; const ni: Nonce;
var nr: Nonce; var nr: Nonce;
var kir: SessionKey; var kir: SessionKey;
send_1(I,R, I,ni ); send_1(I,R, I,ni );
read_2(R,I, {ni,kir,R}k(I,R) ); read_2(R,I, {ni,kir,R}k(I,R) );
send_3(I,R, {ni}kir ); send_3(I,R, {ni}kir );
claim_5(I,Nisynch); claim_5(I,Nisynch);
claim_6(I,Secret, kir); claim_6(I,Secret, kir);
read_4(R,I, nr ); read_4(R,I, nr );
} }
role R role R
{ {
var ni: Nonce; var ni: Nonce;
const nr: Nonce; const nr: Nonce;
const kir: SessionKey; const kir: SessionKey;
read_1(I,R, I,ni ); read_1(I,R, I,ni );
send_2(R,I, {ni,kir,R}k(I,R) ); send_2(R,I, {ni,kir,R}k(I,R) );
read_3(I,R, {ni}kir ); read_3(I,R, {ni}kir );
send_4(R,I, nr ); send_4(R,I, nr );
claim_8(R,Nisynch); claim_8(R,Nisynch);
claim_9(R,Secret, kir); claim_9(R,Secret, kir);
} }
} }
const Alice,Bob,Eve: Agent; const Alice,Bob,Eve: Agent;

50
spdl/SPORE/andrew.spdl
View File

@ -15,33 +15,33 @@ const succ: Function;
protocol andrew(I,R) protocol andrew(I,R)
{ {
role I role I
{ {
const ni: Nonce; const ni: Nonce;
var nr,nr2: Nonce; var nr,nr2: Nonce;
var kir: SessionKey; var kir: SessionKey;
send_1(I,R, I,{ni}k(I,R) ); send_1(I,R, I,{ni}k(I,R) );
read_2(R,I, {succ(ni),nr}k(I,R) ); read_2(R,I, {succ(ni),nr}k(I,R) );
send_3(I,R, {succ(nr)}k(I,R) ); send_3(I,R, {succ(nr)}k(I,R) );
read_4(R,I, {kir,nr2}k(I,R) ); read_4(R,I, {kir,nr2}k(I,R) );
claim_5(I,Secret,kir); claim_5(I,Secret,kir);
claim_6(I,Nisynch); claim_6(I,Nisynch);
} }
role R role R
{ {
var ni: Nonce; var ni: Nonce;
const nr,nr2: Nonce; const nr,nr2: Nonce;
const kir: SessionKey; const kir: SessionKey;
read_1(I,R, I,{ni}k(I,R) ); read_1(I,R, I,{ni}k(I,R) );
send_2(R,I, {succ(ni),nr}k(I,R) ); send_2(R,I, {succ(ni),nr}k(I,R) );
read_3(I,R, {succ(nr)}k(I,R) ); read_3(I,R, {succ(nr)}k(I,R) );
send_4(R,I, {kir,nr2}k(I,R) ); send_4(R,I, {kir,nr2}k(I,R) );
claim_7(R,Secret,kir); claim_7(R,Secret,kir);
claim_8(R,Nisynch); claim_8(R,Nisynch);
} }
} }
const Alice,Bob,Eve: Agent; const Alice,Bob,Eve: Agent;

24
spdl/SPORE/ccitt509-1.spdl
View File

@ -16,24 +16,24 @@ usertype Timestamp;
protocol ccitt5091(I,R) protocol ccitt5091(I,R)
{ {
role I role I
{ {
const Ta: Timestamp; const Ta: Timestamp;
const Na,Xa,Ya: Nonce; const Na,Xa,Ya: Nonce;
send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
# claim_2(I,Nisynch); # claim_2(I,Nisynch);
# This claim is useless as there are no preceding read events # This claim is useless as there are no preceding read events
} }
role R role R
{ {
var Ta: Timestamp; var Ta: Timestamp;
var Na,Xa,Ya: Nonce; var Na,Xa,Ya: Nonce;
read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
claim_3(R,Nisynch); claim_3(R,Nisynch);
# There should also be Fresh Xa and Fresh Ya claims here # There should also be Fresh Xa and Fresh Ya claims here
} }
} }
const Alice,Bob,Eve: Agent; const Alice,Bob,Eve: Agent;

24
spdl/SPORE/ccitt509-1c.spdl
View File

@ -15,24 +15,24 @@ usertype Timestamp;
protocol ccitt5091c(I,R) protocol ccitt5091c(I,R)
{ {
role I role I
{ {
const Ta: Timestamp; const Ta: Timestamp;
const Na,Xa,Ya: Nonce; const Na,Xa,Ya: Nonce;
send_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I)); send_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I));
# claim_2(I,Nisynch); # claim_2(I,Nisynch);
# This claim is useless as there are no preceding read events # This claim is useless as there are no preceding read events
} }
role R role R
{ {
var Ta: Timestamp; var Ta: Timestamp;
var Na,Xa,Ya: Nonce; var Na,Xa,Ya: Nonce;
read_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I)); read_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I));
claim_3(R,Nisynch); claim_3(R,Nisynch);
# There should also be Fresh Xa and Fresh Ya claims here # There should also be Fresh Xa and Fresh Ya claims here
} }
} }
const Alice,Bob,Eve: Agent; const Alice,Bob,Eve: Agent;

24
spdl/SPORE/ccitt509-3.spdl
View File

@ -15,31 +15,31 @@ usertype Timestamp;
protocol ccitt5093(I,R) protocol ccitt5093(I,R)
{ {
role I role I
{ {
const Ta: Timestamp; const Ta: Timestamp;
var Tb: Timestamp; var Tb: Timestamp;
const Na,Xa,Ya: Nonce; const Na,Xa,Ya: Nonce;
var Xb,Nb,Yb: Nonce; var Xb,Nb,Yb: Nonce;
send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
read_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); read_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
send_3(I,R, I, {Nb}sk(I)); send_3(I,R, I, {Nb}sk(I));
claim_4(I,Nisynch); claim_4(I,Nisynch);
} }
role R role R
{ {
var Ta: Timestamp; var Ta: Timestamp;
const Tb: Timestamp; const Tb: Timestamp;
var Na,Xa,Ya: Nonce; var Na,Xa,Ya: Nonce;
const Xb,Yb,Nb: Nonce; const Xb,Yb,Nb: Nonce;
read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
send_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); send_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
read_3(I,R, I, {Nb}sk(I)); read_3(I,R, I, {Nb}sk(I));
claim_5(R,Nisynch); claim_5(R,Nisynch);
# There should also be Fresh Xa and Fresh Ya claims here # There should also be Fresh Xa and Fresh Ya claims here
} }
} }
const Alice,Bob,Eve: Agent; const Alice,Bob,Eve: Agent;

20
spdl/SPORE/ccitt509-ban3.spdl
View File

@ -17,28 +17,28 @@ inversekeys(pk,sk);
protocol ccitt509ban3(I,R) protocol ccitt509ban3(I,R)
{ {
role I role I
{ {
const Na,Xa,Ya: Nonce; const Na,Xa,Ya: Nonce;
var Xb,Nb,Yb: Nonce; var Xb,Nb,Yb: Nonce;
send_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I)); send_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I));
read_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); read_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
send_3(I,R, I,{R, Nb}sk(I)); send_3(I,R, I,{R, Nb}sk(I));
claim_4(I,Nisynch); claim_4(I,Nisynch);
} }
role R role R
{ {
var Na,Xa,Ya: Nonce; var Na,Xa,Ya: Nonce;
const Xb,Yb,Nb: Nonce; const Xb,Yb,Nb: Nonce;
read_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I)); read_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I));
send_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); send_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
read_3(I,R, I,{R, Nb}sk(I)); read_3(I,R, I,{R, Nb}sk(I));
claim_5(R,Nisynch); claim_5(R,Nisynch);
# There should also be Fresh Xa and Fresh Ya claims here # There should also be Fresh Xa and Fresh Ya claims here
} }
} }
const Alice,Bob,Eve: Agent; const Alice,Bob,Eve: Agent;

40
spdl/SPORE/denning-sacco-lowe.spdl
View File

@ -21,42 +21,42 @@ const dec: PseudoFunction;
protocol denningSaccoLowe(I,R,S) protocol denningSaccoLowe(I,R,S)
{ {
role I role I
{ {
var W: Ticket; var W: Ticket;
var Kir: SessionKey; var Kir: SessionKey;
var T: TimeStamp; var T: TimeStamp;
var Nr: Nonce; var Nr: Nonce;
send_1(I,S, I,R ); send_1(I,S, I,R );
read_2(S,I, {R, Kir, T, W}k(I,S) ); read_2(S,I, {R, Kir, T, W}k(I,S) );
send_3(I,R, W); send_3(I,R, W);
read_4(R,I, {Nr}Kir); read_4(R,I, {Nr}Kir);
send_5(I,R, {{Nr}dec}Kir); send_5(I,R, {{Nr}dec}Kir);
claim_6(I,Niagree); claim_6(I,Niagree);
} }
role R role R
{ {
var Kir: SessionKey; var Kir: SessionKey;
var T: TimeStamp; var T: TimeStamp;
const Nr: Nonce; const Nr: Nonce;
read_3(I,R, {Kir,I,T}k(R,S)); read_3(I,R, {Kir,I,T}k(R,S));
send_4(R,I, {Nr}Kir); send_4(R,I, {Nr}Kir);
read_5(I,R, {{Nr}dec}Kir); read_5(I,R, {{Nr}dec}Kir);
claim_8(R,Niagree); claim_8(R,Niagree);
} }
role S role S
{ {
var W: Ticket; var W: Ticket;
const Kir: SessionKey; const Kir: SessionKey;
const T: TimeStamp; const T: TimeStamp;
read_1(I,S, I,R ); read_1(I,S, I,R );
send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S)); send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
} }
} }
const Alice,Bob,Simon,Eve: Agent; const Alice,Bob,Simon,Eve: Agent;

44
spdl/SPORE/denning-sacco.spdl
View File

@ -16,36 +16,36 @@ secret k: Function;
protocol denningSacco(I,R,S) protocol denningSacco(I,R,S)
{ {
role I role I
{ {
var W: Ticket; var W: Ticket;
var Kir: SessionKey;
var T: TimeStamp;
send_1(I,S, I,R );
read_2(S,I, {R, Kir, T, W}k(I,S) );
send_3(I,R, W);
claim_4(I,Nisynch);
}
role R
{
var Kir: SessionKey; var Kir: SessionKey;
var T: TimeStamp; var T: TimeStamp;
read_3(I,R, {Kir,I,T}k(R,S)); send_1(I,S, I,R );
claim_8(R,Nisynch); read_2(S,I, {R, Kir, T, W}k(I,S) );
} send_3(I,R, W);
claim_4(I,Nisynch);
}
role R
{
var Kir: SessionKey;
var T: TimeStamp;
read_3(I,R, {Kir,I,T}k(R,S));
claim_8(R,Nisynch);
}
role S role S
{ {
var W: Ticket; var W: Ticket;
const Kir: SessionKey; const Kir: SessionKey;
const T: TimeStamp; const T: TimeStamp;
read_1(I,S, I,R ); read_1(I,S, I,R );
send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S)); send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
} }
} }
const Alice,Bob,Simon,Eve: Agent; const Alice,Bob,Simon,Eve: Agent;

66
spdl/SPORE/kaochow-v2.spdl
View File

@ -14,45 +14,45 @@ secret k: Function;
protocol kaochow2(I,R,S) protocol kaochow2(I,R,S)
{ {
role I role I
{ {
const ni: Nonce; const ni: Nonce;
var nr: Nonce; var nr: Nonce;
var kir,kt: Sessionkey; var kir,kt: Sessionkey;
send_1 (I,S, I,R,ni); send_1 (I,S, I,R,ni);
read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr ); read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr );
send_4 (I,R, {nr,kir}kt ); send_4 (I,R, {nr,kir}kt );
claim_5 (I, Nisynch); claim_5 (I, Nisynch);
claim_6 (I, Niagree); claim_6 (I, Niagree);
claim_7 (I, Secret, kir); claim_7 (I, Secret, kir);
} }
role R role R
{ {
var ni: Nonce; var ni: Nonce;
const nr: Nonce; const nr: Nonce;
var kir,kt: Sessionkey; var kir,kt: Sessionkey;
var T: Ticket; var T: Ticket;
read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) );
send_3 (R,I, R, T, {ni, kir}kt, nr ); send_3 (R,I, R, T, {ni, kir}kt, nr );
read_4 (I,R, {nr,kir}kt ); read_4 (I,R, {nr,kir}kt );
claim_8 (R, Nisynch); claim_8 (R, Nisynch);
claim_9 (R, Niagree); claim_9 (R, Niagree);
claim_10 (R, Secret, kir); claim_10 (R, Secret, kir);
} }
role S role S
{ {
var ni: Nonce; var ni: Nonce;
const kir, kt: Sessionkey; const kir, kt: Sessionkey;
read_1 (I,S, I,R,ni); read_1 (I,S, I,R,ni);
send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) );
} }
} }
const Alice,Bob,Simon,Eve: Agent; const Alice,Bob,Simon,Eve: Agent;

70
spdl/SPORE/kaochow-v3.spdl
View File

@ -15,47 +15,47 @@ secret k: Function;
protocol kaochow3(I,R,S) protocol kaochow3(I,R,S)
{ {
role I role I
{ {
const ni: Nonce; const ni: Nonce;
var nr: Nonce; var nr: Nonce;
var kir,kt: Sessionkey; var kir,kt: Sessionkey;
var T2: Ticket; var T2: Ticket;
send_1 (I,S, I,R,ni); send_1 (I,S, I,R,ni);
read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 ); read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 );
send_4 (I,R, {nr,kir}kt, T2 ); send_4 (I,R, {nr,kir}kt, T2 );
claim_5 (I, Nisynch); claim_5 (I, Nisynch);
claim_6 (I, Niagree); claim_6 (I, Niagree);
claim_7 (I, Secret, kir); claim_7 (I, Secret, kir);
} }
role R role R
{ {
var ni: Nonce; var ni: Nonce;
const nr: Nonce; const nr: Nonce;
var kir,kt: Sessionkey; var kir,kt: Sessionkey;
var T: Ticket; var T: Ticket;
const tr: Timestamp; const tr: Timestamp;
read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) );
send_3 (R,I, R, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) ); send_3 (R,I, R, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) );
read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) ); read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) );
claim_8 (R, Nisynch); claim_8 (R, Nisynch);
claim_9 (R, Niagree); claim_9 (R, Niagree);
claim_10 (R, Secret, kir); claim_10 (R, Secret, kir);
} }
role S role S
{ {
var ni: Nonce; var ni: Nonce;
const kir, kt: Sessionkey; const kir, kt: Sessionkey;
read_1 (I,S, I,R,ni); read_1 (I,S, I,R,ni);
send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) );
} }
} }
const Alice,Bob,Simon,Eve: Agent; const Alice,Bob,Simon,Eve: Agent;

66
spdl/SPORE/kaochow.spdl
View File

@ -14,45 +14,45 @@ secret k: Function;
protocol kaochow(I,R,S) protocol kaochow(I,R,S)
{ {
role I role I
{ {
const ni: Nonce; const ni: Nonce;
var nr: Nonce; var nr: Nonce;
var kir: Sessionkey; var kir: Sessionkey;
send_1 (I,S, I,R,ni); send_1 (I,S, I,R,ni);
read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr ); read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr );
send_4 (I,R, {nr}kir ); send_4 (I,R, {nr}kir );
claim_5 (I, Nisynch); claim_5 (I, Nisynch);
claim_6 (I, Niagree); claim_6 (I, Niagree);
claim_7 (I, Secret, kir); claim_7 (I, Secret, kir);
} }
role R role R
{ {
var ni: Nonce; var ni: Nonce;
const nr: Nonce; const nr: Nonce;
var kir: Sessionkey; var kir: Sessionkey;
var T; var T;
read_2 (S,R, T, { I,R,ni,kir }k(R,S) ); read_2 (S,R, T, { I,R,ni,kir }k(R,S) );
send_3 (R,I, T, {ni}kir, nr ); send_3 (R,I, T, {ni}kir, nr );
read_4 (I,R, {nr}kir ); read_4 (I,R, {nr}kir );
claim_8 (R, Nisynch); claim_8 (R, Nisynch);
claim_9 (R, Niagree); claim_9 (R, Niagree);
claim_10 (R, Secret, kir); claim_10 (R, Secret, kir);
} }
role S role S
{ {
var ni: Nonce; var ni: Nonce;
const kir: Sessionkey; const kir: Sessionkey;
read_1 (I,S, I,R,ni); read_1 (I,S, I,R,ni);
send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) ); send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) );
} }
} }
const Alice,Bob,Simon,Eve: Agent; const Alice,Bob,Simon,Eve: Agent;

94
spdl/SPORE/ksl-lowe.spdl
View File

@ -25,58 +25,58 @@ compromised k(e,s);
protocol kslLowe(A,B,S) protocol kslLowe(A,B,S)
{ {
role A role A
{ {
const Na, Ma: Nonce; const Na, Ma: Nonce;
var Nc, Mb: Nonce; var Nc, Mb: Nonce;
var T: Ticket; var T: Ticket;
var Kab: SessionKey; var Kab: SessionKey;
send_1(A,B, Na, A); send_1(A,B, Na, A);
read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {B,Na}Kab ); read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {B,Na}Kab );
send_5(A,B, { Nc }Kab ); send_5(A,B, { Nc }Kab );
send_6(A,B, Ma,T ); send_6(A,B, Ma,T );
read_7(B,A, Mb,{Ma, B}Kab ); read_7(B,A, Mb,{Ma, B}Kab );
send_8(A,B, {A,Mb}Kab ); send_8(A,B, {A,Mb}Kab );
claim_A1(A,Secret, Kab); claim_A1(A,Secret, Kab);
claim_A2(A,Niagree); claim_A2(A,Niagree);
claim_A3(A,Nisynch); claim_A3(A,Nisynch);
} }
role B role B
{ {
var Na,Ma: Nonce; var Na,Ma: Nonce;
const Nb,Nc,Mb: Nonce; const Nb,Nc,Mb: Nonce;
var Kab: SessionKey; var Kab: SessionKey;
const Kbb: TicketKey; const Kbb: TicketKey;
const Tb: GeneralizedTimestamp; const Tb: GeneralizedTimestamp;
var T: Ticket; var T: Ticket;
read_1(A,B, Na, A); read_1(A,B, Na, A);
send_2(B,S, Na, A, Nb, B ); send_2(B,S, Na, A, Nb, B );
read_3(S,B, { A, Nb, Kab }k(B,S), T ); read_3(S,B, { A, Nb, Kab }k(B,S), T );
send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {B, Na}Kab ); send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {B, Na}Kab );
read_5(A,B, { Nc }Kab ); read_5(A,B, { Nc }Kab );
read_6(A,B, Ma,{ Tb, A, Kab }Kbb ); read_6(A,B, Ma,{ Tb, A, Kab }Kbb );
send_7(B,A, Mb,{Ma,B}Kab ); send_7(B,A, Mb,{Ma,B}Kab );
read_8(A,B, {A,Mb}Kab ); read_8(A,B, {A,Mb}Kab );
claim_B1(B,Secret, Kab); claim_B1(B,Secret, Kab);
claim_B2(B,Niagree); claim_B2(B,Niagree);
claim_B3(B,Nisynch); claim_B3(B,Nisynch);
} }
role S role S
{ {
var Na, Nb: Nonce; var Na, Nb: Nonce;
const Kab: SessionKey; const Kab: SessionKey;
read_2(B,S, Na, A, Nb, B ); read_2(B,S, Na, A, Nb, B );
send_3(S,B, { A, Nb, Kab }k(B,S), { Na,B,Kab }k(A,S) ); send_3(S,B, { A, Nb, Kab }k(B,S), { Na,B,Kab }k(A,S) );
} }
} }
run kslLowe.A(a,b,s); run kslLowe.A(a,b,s);

94
spdl/SPORE/ksl.spdl
View File

@ -22,58 +22,58 @@ compromised k(e,s);
protocol ksl(A,B,S) protocol ksl(A,B,S)
{ {
role A role A
{ {
const Na, Ma: Nonce; const Na, Ma: Nonce;
var Nc, Mb: Nonce; var Nc, Mb: Nonce;
var T: Ticket; var T: Ticket;
var Kab: SessionKey; var Kab: SessionKey;
send_1(A,B, Na, A); send_1(A,B, Na, A);
read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab ); read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab );
send_5(A,B, { Nc }Kab ); send_5(A,B, { Nc }Kab );
send_6(A,B, Ma,T ); send_6(A,B, Ma,T );
read_7(B,A, Mb,{Ma}Kab ); read_7(B,A, Mb,{Ma}Kab );
send_8(A,B, {Mb}Kab ); send_8(A,B, {Mb}Kab );
claim_A1(A,Secret, Kab); claim_A1(A,Secret, Kab);
claim_A2(A,Niagree); claim_A2(A,Niagree);
claim_A3(A,Nisynch); claim_A3(A,Nisynch);
} }
role B role B
{ {
var Na,Ma: Nonce; var Na,Ma: Nonce;
const Nb,Nc,Mb: Nonce; const Nb,Nc,Mb: Nonce;
var Kab: SessionKey; var Kab: SessionKey;
const Kbb: TicketKey; const Kbb: TicketKey;
const Tb: GeneralizedTimestamp; const Tb: GeneralizedTimestamp;
var T: Ticket; var T: Ticket;
read_1(A,B, Na, A); read_1(A,B, Na, A);
send_2(B,S, Na, A, Nb, B ); send_2(B,S, Na, A, Nb, B );
read_3(S,B, { Nb, A, Kab }k(B,S), T ); read_3(S,B, { Nb, A, Kab }k(B,S), T );
send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {Na}Kab ); send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {Na}Kab );
read_5(A,B, { Nc }Kab ); read_5(A,B, { Nc }Kab );
read_6(A,B, Ma,{ Tb, A, Kab }Kbb ); read_6(A,B, Ma,{ Tb, A, Kab }Kbb );
send_7(B,A, Mb,{Ma}Kab ); send_7(B,A, Mb,{Ma}Kab );
read_8(A,B, {Mb}Kab ); read_8(A,B, {Mb}Kab );
claim_B1(B,Secret, Kab); claim_B1(B,Secret, Kab);
claim_B2(B,Niagree); claim_B2(B,Niagree);
claim_B3(B,Nisynch); claim_B3(B,Nisynch);
} }
role S role S
{ {
var Na, Nb: Nonce; var Na, Nb: Nonce;
const Kab: SessionKey; const Kab: SessionKey;
read_2(B,S, Na, A, Nb, B ); read_2(B,S, Na, A, Nb, B );
send_3(S,B, { Nb, A, Kab }k(B,S), { Na,B,Kab }k(A,S) ); send_3(S,B, { Nb, A, Kab }k(B,S), { Na,B,Kab }k(A,S) );
} }
} }
run ksl.A(a,b,s); run ksl.A(a,b,s);

16
spdl/SPORE/needham-schroeder-lowe.spdl
View File

@ -16,22 +16,22 @@ inversekeys(pk,sk);
protocol needhamschroederpkLowe(I,R,S) protocol needhamschroederpkLowe(I,R,S)
{ {
role I role I
{ {
const Ni: Nonce; const Ni: Nonce;
var Nr: Nonce; var Nr: Nonce;
send_1(I,S, (I,R)); send_1(I,S, (I,R));
read_2(S,I, {pk(R), R}sk(S)); read_2(S,I, {pk(R), R}sk(S));
send_3(I,R,{Ni,I}pk(R)); send_3(I,R,{Ni,I}pk(R));
read_6(R,I, {Ni,Nr,R}pk(I)); read_6(R,I, {Ni,Nr,R}pk(I));
send_7(I,R, {Nr}pk(R)); send_7(I,R, {Nr}pk(R));
claim_I1(I,Secret,Ni); claim_I1(I,Secret,Ni);
claim_I2(I,Secret,Nr); claim_I2(I,Secret,Nr);
} }
role R role R
{ {
const Nr: Nonce; const Nr: Nonce;
var Ni: Nonce; var Ni: Nonce;
@ -42,7 +42,7 @@ protocol needhamschroederpkLowe(I,R,S)
read_7(I,R,{Nr}pk(R)); read_7(I,R,{Nr}pk(R));
claim_R1(R,Secret,Nr); claim_R1(R,Secret,Nr);
claim_R2(R,Secret,Ni); claim_R2(R,Secret,Ni);
} }
role S role S
{ {

14
spdl/SPORE/needham-schroeder-sk-amend.spdl
View File

@ -23,8 +23,8 @@ usertype Ticket;
protocol needhamschroederskamend(I,R,S) protocol needhamschroederskamend(I,R,S)
{ {
role I role I
{ {
const Ni: Nonce; const Ni: Nonce;
var Nr: Nonce; var Nr: Nonce;
var Kir: SessionKey; var Kir: SessionKey;
@ -40,10 +40,10 @@ protocol needhamschroederskamend(I,R,S)
claim_I2(I,Secret,Kir); claim_I2(I,Secret,Kir);
claim_I3(I,Nisynch); claim_I3(I,Nisynch);
} }
role R role R
{ {
const Nr: Nonce; const Nr: Nonce;
var Kir: SessionKey; var Kir: SessionKey;
@ -54,7 +54,7 @@ protocol needhamschroederskamend(I,R,S)
read_7(I,R,{{Nr}dec}Kir); read_7(I,R,{{Nr}dec}Kir);
claim_R1(R,Secret,Nr); claim_R1(R,Secret,Nr);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
} }
role S role S
{ {

16
spdl/SPORE/needham-schroeder-sk.spdl
View File

@ -19,24 +19,24 @@ usertype Ticket;
protocol needhamschroedersk(I,R,S) protocol needhamschroedersk(I,R,S)
{ {
role I role I
{ {
const Ni: Nonce; const Ni: Nonce;
var Nr: Nonce; var Nr: Nonce;
var Kir: SessionKey; var Kir: SessionKey;
var T: Ticket; var T: Ticket;
send_1(I,S,(I,R,Ni)); send_1(I,S,(I,R,Ni));
read_2(S,I, {Ni,R,Kir,T}k(I,S)); read_2(S,I, {Ni,R,Kir,T}k(I,S));
send_3(I,R,T); send_3(I,R,T);
read_4(R,I,{Nr}Kir); read_4(R,I,{Nr}Kir);
send_5(I,R,{{Nr}dec}Kir); send_5(I,R,{{Nr}dec}Kir);
claim_I2(I,Secret,Kir); claim_I2(I,Secret,Kir);
claim_I3(I,Nisynch); claim_I3(I,Nisynch);
} }
role R role R
{ {
const Nr: Nonce; const Nr: Nonce;
var Kir: SessionKey; var Kir: SessionKey;
@ -45,7 +45,7 @@ protocol needhamschroedersk(I,R,S)
read_5(I,R,{{Nr}dec}Kir); read_5(I,R,{{Nr}dec}Kir);
claim_R1(R,Secret,Kir); claim_R1(R,Secret,Kir);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
} }
role S role S
{ {

16
spdl/SPORE/needham-schroeder.spdl
View File

@ -16,22 +16,22 @@ inversekeys(pk,sk);
protocol needhamschroederpk(I,R,S) protocol needhamschroederpk(I,R,S)
{ {
role I role I
{ {
const Ni: Nonce; const Ni: Nonce;
var Nr: Nonce; var Nr: Nonce;
send_1(I,S,(I,R)); send_1(I,S,(I,R));
read_2(S,I, {pk(R), R}sk(S)); read_2(S,I, {pk(R), R}sk(S));
send_3(I,R,{Ni,I}pk(R)); send_3(I,R,{Ni,I}pk(R));
read_6(R,I, {Ni, Nr}pk(I)); read_6(R,I, {Ni, Nr}pk(I));
send_7(I,R, {Nr}pk(R)); send_7(I,R, {Nr}pk(R));
claim_I1(I,Secret,Ni); claim_I1(I,Secret,Ni);
claim_I2(I,Secret,Nr); claim_I2(I,Secret,Nr);
} }
role R role R
{ {
const Nr: Nonce; const Nr: Nonce;
var Ni: Nonce; var Ni: Nonce;
@ -42,7 +42,7 @@ protocol needhamschroederpk(I,R,S)
read_7(I,R,{Nr}pk(R)); read_7(I,R,{Nr}pk(R));
claim_R1(R,Secret,Nr); claim_R1(R,Secret,Nr);
claim_R2(R,Secret,Ni); claim_R2(R,Secret,Ni);
} }
role S role S
{ {

76
spdl/SPORE/neumannstub-hwang.spdl
View File

@ -25,55 +25,55 @@ compromised k(e,s);
protocol neustubHwang(I,R,S) protocol neustubHwang(I,R,S)
{ {
role I role I
{ {
const Ni,Mi: Nonce; const Ni,Mi: Nonce;
var Nr,Mr: Nonce; var Nr,Mr: Nonce;
var T: Ticket; var T: Ticket;
var Tb: TimeStamp; var Tb: TimeStamp;
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I, Ni); send_1(I,R, I, Ni);
read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
send_4(I,R,T,{Nr}Kir); send_4(I,R,T,{Nr}Kir);
send_5(I,R,Mi,T); send_5(I,R,Mi,T);
read_6(R,I,Mr,{Mr}Kir); read_6(R,I,Mr,{Mr}Kir);
send_7(I,R,{Mr}Kir); send_7(I,R,{Mr}Kir);
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
claim_I2(I,Niagree); claim_I2(I,Niagree);
claim_I3(I,Nisynch); claim_I3(I,Nisynch);
} }
role R role R
{ {
var Ni,Mi: Nonce; var Ni,Mi: Nonce;
const Nr,Mr: Nonce; const Nr,Mr: Nonce;
var Kir: SessionKey; var Kir: SessionKey;
const Tb: TimeStamp; const Tb: TimeStamp;
var T: Ticket; var T: Ticket;
read_1(I,R, I, Ni); read_1(I,R, I, Ni);
send_2(R,S, R, {I, Ni, Tb, Nr}k(R,S)); send_2(R,S, R, {I, Ni, Tb, Nr}k(R,S));
read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
read_5(I,R,Mi,T); read_5(I,R,Mi,T);
send_6(R,I,Mr,{Mr}Kir); send_6(R,I,Mr,{Mr}Kir);
read_7(I,R,{Mr}Kir); read_7(I,R,{Mr}Kir);
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
} }
role S role S
{ {
var Ni, Nr: Nonce; var Ni, Nr: Nonce;
const Kir: SessionKey; const Kir: SessionKey;
var Tb: TimeStamp; var Tb: TimeStamp;
read_2(R,S, R, {I,Ni,Tb,Nr}k(R,S)); read_2(R,S, R, {I,Ni,Tb,Nr}k(R,S));
send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
} }
} }
run neustubHwang.A(a,b,s); run neustubHwang.A(a,b,s);

76
spdl/SPORE/neumannstub.spdl
View File

@ -22,55 +22,55 @@ compromised k(e,s);
protocol neustub(I,R,S) protocol neustub(I,R,S)
{ {
role I role I
{ {
const Ni,Mi: Nonce; const Ni,Mi: Nonce;
var Nr,Mr: Nonce; var Nr,Mr: Nonce;
var T: Ticket; var T: Ticket;
var Tb: TimeStamp; var Tb: TimeStamp;
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I, Ni); send_1(I,R, I, Ni);
read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
send_4(I,R,T,{Nr}Kir); send_4(I,R,T,{Nr}Kir);
send_5(I,R,Mi,T); send_5(I,R,Mi,T);
read_6(R,I,Mr,{Mi}Kir); read_6(R,I,Mr,{Mi}Kir);
send_7(I,R,{Mr}Kir); send_7(I,R,{Mr}Kir);
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
claim_I2(I,Niagree); claim_I2(I,Niagree);
claim_I3(I,Nisynch); claim_I3(I,Nisynch);
} }
role R role R
{ {
var Ni,Mi: Nonce; var Ni,Mi: Nonce;
const Nr,Mr: Nonce; const Nr,Mr: Nonce;
var Kir: SessionKey; var Kir: SessionKey;
const Tb: TimeStamp; const Tb: TimeStamp;
var T: Ticket; var T: Ticket;
read_1(I,R, I, Ni); read_1(I,R, I, Ni);
send_2(R,S, R, {I, Ni, Tb}k(R,S),Nr); send_2(R,S, R, {I, Ni, Tb}k(R,S),Nr);
read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
read_5(I,R,Mi,T); read_5(I,R,Mi,T);
send_6(R,I,Mr,{Mi}Kir); send_6(R,I,Mr,{Mi}Kir);
read_7(I,R,{Mr}Kir); read_7(I,R,{Mr}Kir);
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
} }
role S role S
{ {
var Ni, Nr: Nonce; var Ni, Nr: Nonce;
const Kir: SessionKey; const Kir: SessionKey;
var Tb: TimeStamp; var Tb: TimeStamp;
read_2(R,S, R, {I,Ni,Tb}k(R,S), Nr); read_2(R,S, R, {I,Ni,Tb}k(R,S), Nr);
send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
} }
} }
run neustub.A(a,b,s); run neustub.A(a,b,s);

60
spdl/SPORE/otwayrees.spdl
View File

@ -16,44 +16,44 @@ usertype String,SessionKey,Ticket;
protocol otwayrees(I,R,S) protocol otwayrees(I,R,S)
{ {
role I role I
{ {
const Ni : Nonce; const Ni : Nonce;
const M : String; const M : String;
var Kir : SessionKey; var Kir : SessionKey;
send_1(I,R, M,I,R,{Ni,M,I,R}k(I,S) ); send_1(I,R, M,I,R,{Ni,M,I,R}k(I,S) );
read_4(R,I, M,{Ni,Kir}k(I,S) ); read_4(R,I, M,{Ni,Kir}k(I,S) );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
#claim_I2(I, Nisynch); #claim_I2(I, Nisynch);
} }
role R role R
{ {
var M : String; var M : String;
const Nr : Nonce; const Nr : Nonce;
var Kir : SessionKey; var Kir : SessionKey;
var T1,T2: Ticket; var T1,T2: Ticket;
read_1(I,R, M,I,R, T1 ); read_1(I,R, M,I,R, T1 );
send_2(R,S, M,I,R, T1, { Nr,M,I,R }k(R,S) ); send_2(R,S, M,I,R, T1, { Nr,M,I,R }k(R,S) );
read_3(S,R, M, T2, { Nr,Kir }k(R,S) ); read_3(S,R, M, T2, { Nr,Kir }k(R,S) );
send_4(R,I, M, T2 ); send_4(R,I, M, T2 );
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
#claim_R2(R, Nisynch); #claim_R2(R, Nisynch);
} }
role S role S
{ {
var Ni,Nr : Nonce; var Ni,Nr : Nonce;
var M : String; var M : String;
const Kir : SessionKey; const Kir : SessionKey;
read_2(R,S, M,I,R, { Ni,M,I,R}k(I,S), { Nr,M,I,R }k(R,S) ); read_2(R,S, M,I,R, { Ni,M,I,R}k(I,S), { Nr,M,I,R }k(R,S) );
send_3(S,R, M, { Ni,Kir }k(I,S) , { Nr,Kir }k(R,S) ); send_3(S,R, M, { Ni,Kir }k(I,S) , { Nr,Kir }k(R,S) );
} }
} }
const Alice, Bob, Eve, Simon: Agent; const Alice, Bob, Eve, Simon: Agent;

18
spdl/SPORE/smartright.spdl
View File

@ -25,9 +25,9 @@ const Vor: XorKey;
protocol smartright(I,R) protocol smartright(I,R)
{ {
role I role I
{ {
const VoKey: SessionKey; const VoKey: SessionKey;
const VoR: XorKey; const VoR: XorKey;
const CW; const CW;
var VoRi: Nonce; var VoRi: Nonce;
@ -35,10 +35,10 @@ protocol smartright(I,R)
send_1(I,R, {VoKey,{CW}VoR}k(I,R)); send_1(I,R, {VoKey,{CW}VoR}k(I,R));
read_2(R,I, VoRi); read_2(R,I, VoRi);
send_3(I,R, VoR, {{VoRi}hash}VoKey); send_3(I,R, VoR, {{VoRi}hash}VoKey);
} }
role R role R
{ {
var T: Ticket; var T: Ticket;
var VoR: XorKey; var VoR: XorKey;
var VoKey: SessionKey; var VoKey: SessionKey;
@ -48,8 +48,8 @@ protocol smartright(I,R)
send_2(R,I, VoRi); send_2(R,I, VoRi);
read_3(I,R, VoR,{{VoRi}hash}VoKey); read_3(I,R, VoR,{{VoRi}hash}VoKey);
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
} }
const Alice,Bob,Eve: Agent; const Alice,Bob,Eve: Agent;

72
spdl/SPORE/splice-as-cj.spdl
View File

@ -21,50 +21,50 @@ inversekeys (inc,dec);
protocol spliceASCJ(I,R,S) protocol spliceASCJ(I,R,S)
{ {
role I role I
{ {
const N1,N2: Nonce; const N1,N2: Nonce;
const T: TimeStamp; const T: TimeStamp;
const L: LifeTime; const L: LifeTime;
send_1(I,S, I, R, N1 ); send_1(I,S, I, R, N1 );
read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
send_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) ); send_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) );
read_6(R,I, R, I, {{N2}inc}pk(I) ); read_6(R,I, R, I, {{N2}inc}pk(I) );
claim_7(I, Secret, N2); claim_7(I, Secret, N2);
claim_9(I, Niagree); claim_9(I, Niagree);
claim_10(I, Nisynch); claim_10(I, Nisynch);
} }
role S role S
{ {
var N1,N3: Nonce; var N1,N3: Nonce;
read_1(I,S, I, R, N1 ); read_1(I,S, I, R, N1 );
send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
read_4(R,S, R, I, N3 ); read_4(R,S, R, I, N3 );
send_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); send_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
} }
role R role R
{ {
const N3: Nonce; const N3: Nonce;
var N2: Nonce; var N2: Nonce;
var T: TimeStamp; var T: TimeStamp;
var L: LifeTime; var L: LifeTime;
var ni: Nonce; var ni: Nonce;
const nr: Nonce; const nr: Nonce;
read_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) ); read_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) );
send_4(R,S, R, I, N3 ); send_4(R,S, R, I, N3 );
read_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); read_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
send_6(R,I, R, I, {{N2}inc}pk(I) ); send_6(R,I, R, I, {{N2}inc}pk(I) );
claim_8(R, Secret, N2); claim_8(R, Secret, N2);
claim_11(R, Niagree); claim_11(R, Niagree);
claim_12(R, Nisynch); claim_12(R, Nisynch);
} }
} }
const Alice,Bob,Simon,Eve: Agent; const Alice,Bob,Simon,Eve: Agent;

72
spdl/SPORE/splice-as-hc.spdl
View File

@ -16,50 +16,50 @@ inversekeys (inc,dec);
protocol spliceASHC(I,R,S) protocol spliceASHC(I,R,S)
{ {
role I role I
{ {
const N1,N2: Nonce; const N1,N2: Nonce;
const T: TimeStamp; const T: TimeStamp;
const L: LifeTime; const L: LifeTime;
send_1(I,S, I, R, N1 ); send_1(I,S, I, R, N1 );
read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
read_6(R,I, R, I, {R, {N2}inc}pk(I) ); read_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_7(I, Secret, N2); claim_7(I, Secret, N2);
claim_9(I, Niagree); claim_9(I, Niagree);
claim_10(I, Nisynch); claim_10(I, Nisynch);
} }
role S role S
{ {
var N1,N3: Nonce; var N1,N3: Nonce;
read_1(I,S, I, R, N1 ); read_1(I,S, I, R, N1 );
send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
read_4(R,S, R, I, N3 ); read_4(R,S, R, I, N3 );
send_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) ); send_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) );
} }
role R role R
{ {
const N3: Nonce; const N3: Nonce;
var N2: Nonce; var N2: Nonce;
var T: TimeStamp; var T: TimeStamp;
var L: LifeTime; var L: LifeTime;
var ni: Nonce; var ni: Nonce;
const nr: Nonce; const nr: Nonce;
read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
send_4(R,S, R, I, N3 ); send_4(R,S, R, I, N3 );
read_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) ); read_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) );
send_6(R,I, R, I, {R, {N2}inc}pk(I) ); send_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_8(R, Secret, N2); claim_8(R, Secret, N2);
claim_11(R, Niagree); claim_11(R, Niagree);
claim_12(R, Nisynch); claim_12(R, Nisynch);
} }
} }
const Alice,Bob,Simon,Eve: Agent; const Alice,Bob,Simon,Eve: Agent;

72
spdl/SPORE/splice-as.spdl
View File

@ -21,50 +21,50 @@ inversekeys (inc,dec);
protocol spliceAS(I,R,S) protocol spliceAS(I,R,S)
{ {
role I role I
{ {
const N1,N2: Nonce; const N1,N2: Nonce;
const T: TimeStamp; const T: TimeStamp;
const L: LifeTime; const L: LifeTime;
send_1(I,S, I, R, N1 ); send_1(I,S, I, R, N1 );
read_2(S,I, S, {S, I, N1, pk(R)}sk(S) ); read_2(S,I, S, {S, I, N1, pk(R)}sk(S) );
send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
read_6(R,I, R, I, {R, {N2}inc}pk(I) ); read_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_7(I, Secret, N2); claim_7(I, Secret, N2);
claim_9(I, Niagree); claim_9(I, Niagree);
claim_10(I, Nisynch); claim_10(I, Nisynch);
} }
role S role S
{ {
var N1,N3: Nonce; var N1,N3: Nonce;
read_1(I,S, I, R, N1 ); read_1(I,S, I, R, N1 );
send_2(S,I, S, {S, I, N1, pk(R)}sk(S) ); send_2(S,I, S, {S, I, N1, pk(R)}sk(S) );
read_4(R,S, R, I, N3 ); read_4(R,S, R, I, N3 );
send_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); send_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
} }
role R role R
{ {
const N3: Nonce; const N3: Nonce;
var N2: Nonce; var N2: Nonce;
var T: TimeStamp; var T: TimeStamp;
var L: LifeTime; var L: LifeTime;
var ni: Nonce; var ni: Nonce;
const nr: Nonce; const nr: Nonce;
read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
send_4(R,S, R, I, N3 ); send_4(R,S, R, I, N3 );
read_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); read_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
send_6(R,I, R, I, {R, {N2}inc}pk(I) ); send_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_8(R, Secret, N2); claim_8(R, Secret, N2);
claim_11(R, Niagree); claim_11(R, Niagree);
claim_12(R, Nisynch); claim_12(R, Nisynch);
} }
} }
const Alice,Bob,Simon,Eve: Agent; const Alice,Bob,Simon,Eve: Agent;

50
spdl/SPORE/tmn.spdl
View File

@ -12,37 +12,37 @@ inversekeys(pk,sk);
protocol tmn(I,R,S) protocol tmn(I,R,S)
{ {
role I role I
{ {
const Ki: Key; const Ki: Key;
var Kr: Key; var Kr: Key;
send_1(I,S, R,{Ki}pk(S) ); send_1(I,S, R,{Ki}pk(S) );
read_4(S,I, R,{Kr}Ki ); read_4(S,I, R,{Kr}Ki );
claim_I1(I,Secret,Ki); claim_I1(I,Secret,Ki);
claim_I2(I,Secret,Kr); claim_I2(I,Secret,Kr);
} }
role R role R
{ {
const Kr: Key; const Kr: Key;
read_2(S,R, I ); read_2(S,R, I );
send_3(R,S, I, { Kr }pk(S) ); send_3(R,S, I, { Kr }pk(S) );
claim_R1(R,Secret,Kr); claim_R1(R,Secret,Kr);
} }
role S role S
{ {
var Ki,Kr: Key; var Ki,Kr: Key;
read_1(I,S, R,{Ki}pk(S) ); read_1(I,S, R,{Ki}pk(S) );
send_2(S,R, I ); send_2(S,R, I );
read_3(R,S, I, { Kr }pk(S) ); read_3(R,S, I, { Kr }pk(S) );
send_4(S,I, R,{Kr}Ki ); send_4(S,I, R,{Kr}Ki );
} }
} }
const Alice,Bob,Eve,Simon: Agent; const Alice,Bob,Eve,Simon: Agent;

36
spdl/SPORE/wmf-lowe.spdl
View File

@ -18,44 +18,44 @@ secret k: Function;
protocol wmfLowe(I,R,S) protocol wmfLowe(I,R,S)
{ {
role I role I
{ {
const Kir: Key; const Kir: Key;
const Ti: TimeStamp; const Ti: TimeStamp;
var Kr: Key; var Kr: Key;
var Nr: Nonce; var Nr: Nonce;
send_1(I,S, I, {Ti, R, Kir}k(I,S)); send_1(I,S, I, {Ti, R, Kir}k(I,S));
read_3(R,I,{Nr}Kir); read_3(R,I,{Nr}Kir);
send_4(I,R,{{Nr}succ}Kir); send_4(I,R,{{Nr}succ}Kir);
claim_I1(I,Secret,Kir); claim_I1(I,Secret,Kir);
claim_I2(I,Nisynch); claim_I2(I,Nisynch);
} }
role R role R
{ {
var Ts: TimeStamp; var Ts: TimeStamp;
var Kir: Key; var Kir: Key;
const Nr: Nonce; const Nr: Nonce;
read_2(S,R, {Ts, I, Kir}k(R,S) ); read_2(S,R, {Ts, I, Kir}k(R,S) );
send_3(R,I, {Nr}Kir); send_3(R,I, {Nr}Kir);
read_4(I,R, {{Nr}succ}Kir); read_4(I,R, {{Nr}succ}Kir);
claim_R1(R,Secret,Kir); claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
} }
role S role S
{ {
var Kir: Key; var Kir: Key;
const Ts: TimeStamp; const Ts: TimeStamp;
var Ti: TimeStamp; var Ti: TimeStamp;
read_1(I,S, I,{Ti, R, Kir}k(I,S) ); read_1(I,S, I,{Ti, R, Kir}k(I,S) );
send_2(S,R, {Ts, I, Kir}k(R,S)); send_2(S,R, {Ts, I, Kir}k(R,S));
} }
} }
const Alice,Bob,Eve,Simon: Agent; const Alice,Bob,Eve,Simon: Agent;

36
spdl/SPORE/wmf.spdl
View File

@ -11,37 +11,37 @@ secret k: Function;
protocol wmf(I,R,S) protocol wmf(I,R,S)
{ {
role I role I
{ {
const Kir: Key; const Kir: Key;
const Ti: TimeStamp; const Ti: TimeStamp;
var Kr: Key; var Kr: Key;
send_1(I,S, I, {Ti, R, Kir}k(I,S)); send_1(I,S, I, {Ti, R, Kir}k(I,S));
claim_I1(I,Secret,Kir); claim_I1(I,Secret,Kir);
} }
role R role R
{ {
var Ts: TimeStamp; var Ts: TimeStamp;
var Kir: Key; var Kir: Key;
read_2(S,R, {Ts, I, Kir}k(R,S) ); read_2(S,R, {Ts, I, Kir}k(R,S) );
claim_R1(R,Secret,Kir); claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
} }
role S role S
{ {
var Kir: Key; var Kir: Key;
const Ts: TimeStamp; const Ts: TimeStamp;
var Ti: TimeStamp; var Ti: TimeStamp;
read_1(I,S, I,{Ti, R, Kir}k(I,S) ); read_1(I,S, I,{Ti, R, Kir}k(I,S) );
send_2(S,R, {Ts, I, Kir}k(R,S)); send_2(S,R, {Ts, I, Kir}k(R,S));
} }
} }
const Alice,Bob,Eve,Simon: Agent; const Alice,Bob,Eve,Simon: Agent;

24
spdl/SPORE/woo-lam-pi-1.spdl
View File

@ -14,18 +14,18 @@ secret k: Function;
protocol woolamPi1(I,R,S) protocol woolamPi1(I,R,S)
{ {
role I role I
{ {
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); read_2(R,I, Nr);
send_3(I,R, {I,R,Nr}k(I,S)); send_3(I,R, {I,R,Nr}k(I,S));
} }
role R role R
{ {
const Nr: Nonce; const Nr: Nonce;
var T: Ticket; var T: Ticket;
@ -36,15 +36,15 @@ protocol woolamPi1(I,R,S)
read_5(S,R, {I,R, Nr}k(R,S)); read_5(S,R, {I,R, Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
role S role S
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I,R, {I,R,Nr}k(I,S)}k(R,S)); read_4(R,S, {I,R, {I,R,Nr}k(I,S)}k(R,S));
send_5(S,R, {I,R,Nr}k(R,S)); send_5(S,R, {I,R,Nr}k(R,S));
} }
} }
const Alice,Bob,Eve,Simon: Agent; const Alice,Bob,Eve,Simon: Agent;

24
spdl/SPORE/woo-lam-pi-2.spdl
View File

@ -14,18 +14,18 @@ secret k: Function;
protocol woolamPi2(I,R,S) protocol woolamPi2(I,R,S)
{ {
role I role I
{ {
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); read_2(R,I, Nr);
send_3(I,R, {I,Nr}k(I,S)); send_3(I,R, {I,Nr}k(I,S));
} }
role R role R
{ {
const Nr: Nonce; const Nr: Nonce;
var T: Ticket; var T: Ticket;
@ -36,15 +36,15 @@ protocol woolamPi2(I,R,S)
read_5(S,R, {I, Nr}k(R,S)); read_5(S,R, {I, Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
role S role S
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I, {I,Nr}k(I,S)}k(R,S)); read_4(R,S, {I, {I,Nr}k(I,S)}k(R,S));
send_5(S,R, {I,Nr}k(R,S)); send_5(S,R, {I,Nr}k(R,S));
} }
} }
const Alice,Bob,Eve,Simon: Agent; const Alice,Bob,Eve,Simon: Agent;

24
spdl/SPORE/woo-lam-pi-3.spdl
View File

@ -14,18 +14,18 @@ secret k: Function;
protocol woolamPi3(I,R,S) protocol woolamPi3(I,R,S)
{ {
role I role I
{ {
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); read_2(R,I, Nr);
send_3(I,R, {Nr}k(I,S)); send_3(I,R, {Nr}k(I,S));
} }
role R role R
{ {
const Nr: Nonce; const Nr: Nonce;
var T: Ticket; var T: Ticket;
@ -36,15 +36,15 @@ protocol woolamPi3(I,R,S)
read_5(S,R, {I, Nr}k(R,S)); read_5(S,R, {I, Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
role S role S
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I, {Nr}k(I,S)}k(R,S)); read_4(R,S, {I, {Nr}k(I,S)}k(R,S));
send_5(S,R, {I,Nr}k(R,S)); send_5(S,R, {I,Nr}k(R,S));
} }
} }
const Alice,Bob,Eve,Simon: Agent; const Alice,Bob,Eve,Simon: Agent;

24
spdl/SPORE/woo-lam-pi-f.spdl
View File

@ -14,18 +14,18 @@ secret k: Function;
protocol woolamPif(I,R,S) protocol woolamPif(I,R,S)
{ {
role I role I
{ {
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); read_2(R,I, Nr);
send_3(I,R, {I,R,Nr}k(I,S)); send_3(I,R, {I,R,Nr}k(I,S));
} }
role R role R
{ {
const Nr: Nonce; const Nr: Nonce;
var T: Ticket; var T: Ticket;
@ -36,15 +36,15 @@ protocol woolamPif(I,R,S)
read_5(S,R, {I, R, Nr}k(R,S)); read_5(S,R, {I, R, Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
role S role S
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I, R, Nr,{I,R,Nr}k(I,S)}k(R,S)); read_4(R,S, {I, R, Nr,{I,R,Nr}k(I,S)}k(R,S));
send_5(S,R, {I, R, Nr}k(R,S)); send_5(S,R, {I, R, Nr}k(R,S));
} }
} }
const Alice,Bob,Eve,Simon: Agent; const Alice,Bob,Eve,Simon: Agent;

24
spdl/SPORE/woo-lam-pi.spdl
View File

@ -18,18 +18,18 @@ secret k: Function;
protocol woolamPi(I,R,S) protocol woolamPi(I,R,S)
{ {
role I role I
{ {
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); read_2(R,I, Nr);
send_3(I,R, {Nr}k(I,S)); send_3(I,R, {Nr}k(I,S));
} }
role R role R
{ {
const Nr: Nonce; const Nr: Nonce;
var T: Ticket; var T: Ticket;
@ -40,15 +40,15 @@ protocol woolamPi(I,R,S)
read_5(S,R, {Nr}k(R,S)); read_5(S,R, {Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
role S role S
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I,{Nr}k(I,S)}k(R,S)); read_4(R,S, {I,{Nr}k(I,S)}k(R,S));
send_5(S,R, {Nr}k(R,S)); send_5(S,R, {Nr}k(R,S));
} }
} }
const Alice,Bob,Eve,Simon: Agent; const Alice,Bob,Eve,Simon: Agent;

30
spdl/SPORE/woo-lam.spdl
View File

@ -16,25 +16,25 @@ secret k: Function;
protocol woolam(I,R,S) protocol woolam(I,R,S)
{ {
role I role I
{ {
const N1: Nonce; const N1: Nonce;
var Kir: Key; var Kir: Key;
var N2: Nonce; var N2: Nonce;
send_1(I,R, I, N1); send_1(I,R, I, N1);
read_2(R,I, R, N2); read_2(R,I, R, N2);
send_3(I,R, {I, R, N1, N2}k(I,S)); send_3(I,R, {I, R, N1, N2}k(I,S));
read_6(R,I, {R, N1, N2, Kir}k(I,S), {N1,N2}Kir); read_6(R,I, {R, N1, N2, Kir}k(I,S), {N1,N2}Kir);
send_7(I,R, {N2}Kir); send_7(I,R, {N2}Kir);
claim_I1(I,Secret,Kir); claim_I1(I,Secret,Kir);
claim_I2(I,Nisynch); claim_I2(I,Nisynch);
} }
role R role R
{ {
const N2: Nonce; const N2: Nonce;
var N1: Nonce; var N1: Nonce;
var Kir: Key; var Kir: Key;
@ -48,18 +48,18 @@ protocol woolam(I,R,S)
send_6(R,I, T2, {N1,N2}Kir); send_6(R,I, T2, {N1,N2}Kir);
read_7(I,R, {N2}Kir); read_7(I,R, {N2}Kir);
claim_R1(R,Secret,Kir); claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
} }
role S role S
{ {
const Kir: Key; const Kir: Key;
var N1,N2: Nonce; var N1,N2: Nonce;
read_4(R,S, {I, R, N1, N2}k(I,S), {I, R, N1, N2}k(R,S)); read_4(R,S, {I, R, N1, N2}k(I,S), {I, R, N1, N2}k(R,S));
send_5(S,R, {R, N1, N2, Kir}k(I,S), {I, N1, N2, Kir}k(R,S)); send_5(S,R, {R, N1, N2, Kir}k(I,S), {I, N1, N2, Kir}k(R,S));
} }
} }
const Alice,Bob,Eve,Simon: Agent; const Alice,Bob,Eve,Simon: Agent;

60
spdl/SPORE/yahalom-ban.spdl
View File

@ -15,44 +15,44 @@ usertype Ticket, Key;
protocol yahalomBAN(I,R,S) protocol yahalomBAN(I,R,S)
{ {
role I role I
{ {
const Ni: Nonce; const Ni: Nonce;
var Nr: Nonce; var Nr: Nonce;
var T: Ticket; var T: Ticket;
var Kir: Key; var Kir: Key;
send_1(I,R, I,Ni); send_1(I,R, I,Ni);
read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T ); read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T );
send_4(I,R, T, {Nr}Kir ); send_4(I,R, T, {Nr}Kir );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch); claim_I2(I, Nisynch);
} }
role R role R
{ {
const Nr: Nonce; const Nr: Nonce;
var Ni: Nonce; var Ni: Nonce;
var T: Ticket; var T: Ticket;
var Kir: Key; var Kir: Key;
read_1(I,R, I,Ni); read_1(I,R, I,Ni);
send_2(R,S, R, Nr, {I,Ni}k(R,S) ); send_2(R,S, R, Nr, {I,Ni}k(R,S) );
read_4(I,R, {I,Kir,Nr}k(R,S) , {Nr}Kir ); read_4(I,R, {I,Kir,Nr}k(R,S) , {Nr}Kir );
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch); claim_R2(R, Nisynch);
} }
role S role S
{ {
const Kir: Key; const Kir: Key;
var Ni,Nr: Nonce; var Ni,Nr: Nonce;
read_2(R,S, R, {I,Ni,Nr}k(R,S) ); read_2(R,S, R, {I,Ni,Nr}k(R,S) );
send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) ); send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) );
} }
} }
const Alice,Bob,Simon : Agent; const Alice,Bob,Simon : Agent;

58
spdl/SPORE/yahalom-lowe.spdl
View File

@ -12,44 +12,44 @@ usertype Key;
protocol yahalomLowe(I,R,S) protocol yahalomLowe(I,R,S)
{ {
role I role I
{ {
const Ni: Nonce; const Ni: Nonce;
var Nr: Nonce; var Nr: Nonce;
var Kir: Key; var Kir: Key;
send_1(I,R, I,Ni); send_1(I,R, I,Ni);
read_3(S,I, {R,Kir,Ni,Nr}k(I,S) ); read_3(S,I, {R,Kir,Ni,Nr}k(I,S) );
send_5(I,R, {I, R, S, Nr}Kir ); send_5(I,R, {I, R, S, Nr}Kir );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch); claim_I2(I, Nisynch);
} }
role R role R
{ {
const Nr: Nonce; const Nr: Nonce;
var Ni: Nonce; var Ni: Nonce;
var Kir: Key; var Kir: Key;
read_1(I,R, I,Ni); read_1(I,R, I,Ni);
send_2(R,S, {I,Ni,Nr}k(R,S) ); send_2(R,S, {I,Ni,Nr}k(R,S) );
read_4(S,R, {I,Kir}k(R,S)); read_4(S,R, {I,Kir}k(R,S));
read_5(I,R, {I, R, S, Nr}Kir); read_5(I,R, {I, R, S, Nr}Kir);
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch); claim_R2(R, Nisynch);
} }
role S role S
{ {
const Kir: Key; const Kir: Key;
var Ni,Nr: Nonce; var Ni,Nr: Nonce;
read_2(R,S, {I,Ni,Nr}k(R,S) ); read_2(R,S, {I,Ni,Nr}k(R,S) );
send_3(S,I, {R,Kir,Ni,Nr}k(I,S)); send_3(S,I, {R,Kir,Ni,Nr}k(I,S));
send_4(S,R, {I,Kir}k(R,S)); send_4(S,R, {I,Kir}k(R,S));
} }
} }
const Alice,Bob,Simon : Agent; const Alice,Bob,Simon : Agent;

60
spdl/SPORE/yahalom-paulson.spdl
View File

@ -15,44 +15,44 @@ usertype Ticket, Key;
protocol yahalomPaulson(I,R,S) protocol yahalomPaulson(I,R,S)
{ {
role I role I
{ {
const Ni: Nonce; const Ni: Nonce;
var Nr: Nonce; var Nr: Nonce;
var T: Ticket; var T: Ticket;
var Kir: Key; var Kir: Key;
send_1(I,R, I,Ni); send_1(I,R, I,Ni);
read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T ); read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T );
send_4(I,R, T, {Nr}Kir ); send_4(I,R, T, {Nr}Kir );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch); claim_I2(I, Nisynch);
} }
role R role R
{ {
const Nr: Nonce; const Nr: Nonce;
var Ni: Nonce; var Ni: Nonce;
var T: Ticket; var T: Ticket;
var Kir: Key; var Kir: Key;
read_1(I,R, I,Ni); read_1(I,R, I,Ni);
send_2(R,S, R, Nr, {I,Ni}k(R,S) ); send_2(R,S, R, Nr, {I,Ni}k(R,S) );
read_4(I,R, {I,R, Kir, Nr}k(R,S) , {Nr}Kir ); read_4(I,R, {I,R, Kir, Nr}k(R,S) , {Nr}Kir );
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch); claim_R2(R, Nisynch);
} }
role S role S
{ {
const Kir: Key; const Kir: Key;
var Ni,Nr: Nonce; var Ni,Nr: Nonce;
read_2(R,S, R, Nr, {I,Ni}k(R,S) ); read_2(R,S, R, Nr, {I,Ni}k(R,S) );
send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,R,Kir,Nr}k(R,S) ); send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,R,Kir,Nr}k(R,S) );
} }
} }
const Alice,Bob,Simon : Agent; const Alice,Bob,Simon : Agent;

60
spdl/SPORE/yahalom.spdl
View File

@ -15,44 +15,44 @@ usertype Ticket, Key;
protocol yahalom(I,R,S) protocol yahalom(I,R,S)
{ {
role I role I
{ {
const Ni: Nonce; const Ni: Nonce;
var Nr: Nonce; var Nr: Nonce;
var T: Ticket; var T: Ticket;
var Kir: Key; var Kir: Key;
send_1(I,R, I,Ni); send_1(I,R, I,Ni);
read_3(S,I, {R,Kir,Ni,Nr}k(I,S), T ); read_3(S,I, {R,Kir,Ni,Nr}k(I,S), T );
send_4(I,R, T, {Nr}Kir ); send_4(I,R, T, {Nr}Kir );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch); claim_I2(I, Nisynch);
} }
role R role R
{ {
const Nr: Nonce; const Nr: Nonce;
var Ni: Nonce; var Ni: Nonce;
var T: Ticket; var T: Ticket;
var Kir: Key; var Kir: Key;
read_1(I,R, I,Ni); read_1(I,R, I,Ni);
send_2(R,S, R, {I,Ni,Nr}k(R,S) ); send_2(R,S, R, {I,Ni,Nr}k(R,S) );
read_4(I,R, {I,Kir}k(R,S) , {Nr}Kir ); read_4(I,R, {I,Kir}k(R,S) , {Nr}Kir );
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch); claim_R2(R, Nisynch);
} }
role S role S
{ {
const Kir: Key; const Kir: Key;
var Ni,Nr: Nonce; var Ni,Nr: Nonce;
read_2(R,S, R, {I,Ni,Nr}k(R,S) ); read_2(R,S, R, {I,Ni,Nr}k(R,S) );
send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) ); send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) );
} }
} }
const Alice,Bob,Simon : Agent; const Alice,Bob,Simon : Agent;