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

- Add freshness claims to the protocols that should guarantee freshness

Browse Source
This commit is contained in:
gijs 2005-06-23 12:45:32 +00:00
parent 464920907b
commit 4c224dc6f4
23 changed files with 134 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -18,17 +18,21 @@
usertype SessionKey;
secret k: Function;
const Fresh: Function;
protocol andrewConcrete(I,R,X)
protocol swapkey(X)
{
# Role added to work around the symmetry problems where k(I,R) != k(R,I)
# Protocol added to work around the symmetry problems where k(I,R) != k(R,I)
role X
{
var T: Ticket;
read_X1(X,X, {T}k(I,R));
send_X2(X,X, {T}k(R,I));
var I,R: Agent;
var T:Ticket;
read_X1(X,X,I,R,{T}k(I,R));
send_X2(X,X,{T}k(R,I));
}
}
protocol andrewConcrete(I,R)
{
role I
{
@ -39,8 +43,9 @@ protocol andrewConcrete(I,R,X)
send_1(I,R, I,ni );
read_2(R,I, {ni,kir}k(I,R) );
send_3(I,R, {ni}kir);
claim_4(I,Secret,kir);
claim_5(I,Nisynch);
claim_I1(I,Secret,kir);
claim_I2(I,Nisynch);
claim_I3(I,Empty,(Fresh,kir));
read_6(R,I, nr);
}
@ -54,8 +59,9 @@ protocol andrewConcrete(I,R,X)
send_2(R,I, {ni,kir}k(I,R) );
read_3(I,R, {ni}kir);
send_6(R,I, nr);
claim_7(R,Secret,kir);
claim_8(R,Nisynch);
claim_R1(R,Secret,kir);
claim_R2(R,Nisynch);
claim_R3(R,Empty,(Fresh,kir));
}
}

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

@ -13,6 +13,7 @@
#
usertype SessionKey;
secret k: Function;
const Fresh: Function;
protocol andrewBan(I,R)
{
@ -26,10 +27,11 @@ protocol andrewBan(I,R)
read_2(R,I, {ni,nr}k(I,R) );
send_3(I,R, {nr}k(I,R) );
read_4(R,I, {kir,nr2,ni}k(I,R) );
claim_5(I,Nisynch);
claim_5b(I,Niagree);
claim_6(I,Secret, kir);
claim_7(I,Secret, k(I,R));
claim_I1(I,Nisynch);
claim_I2(I,Niagree);
claim_I3(I,Secret, kir);
claim_I4(I,Secret, k(I,R));
claim_I5(I,Empty, (Fresh,kir));
}
role R
@ -42,10 +44,11 @@ protocol andrewBan(I,R)
send_2(R,I, {ni,nr}k(I,R) );
read_3(I,R, {nr}k(I,R) );
send_4(R,I, {kir,nr2,ni}k(I,R) );
claim_8(R,Nisynch);
claim_8b(R,Niagree);
claim_9(R,Secret, kir);
claim_10(R,Secret, k(I,R));
claim_R1(R,Nisynch);
claim_R2(R,Niagree);
claim_R3(R,Secret, kir);
claim_R4(R,Secret, k(I,R));
claim_R5(R,Empty, (Fresh,kir));
}
}

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

@ -20,6 +20,7 @@
usertype SessionKey;
secret k: Function;
const Fresh: Function;
protocol andrewLoweBan(I,R)
{
@ -32,8 +33,9 @@ protocol andrewLoweBan(I,R)
send_1(I,R, I,ni );
read_2(R,I, {ni,kir,R}k(I,R) );
send_3(I,R, {ni}kir );
claim_5(I,Nisynch);
claim_6(I,Secret, kir);
claim_I1(I,Nisynch);
claim_I2(I,Secret, kir);
claim_I3(I,Empty, (Fresh,kir));
read_4(R,I, nr );
}
@ -47,8 +49,9 @@ protocol andrewLoweBan(I,R)
send_2(R,I, {ni,kir,R}k(I,R) );
read_3(I,R, {ni}kir );
send_4(R,I, nr );
claim_8(R,Nisynch);
claim_9(R,Secret, kir);
claim_R1(R,Nisynch);
claim_R2(R,Secret, kir);
claim_R3(R,Empty, (Fresh,kir));
}
}

13
spdl/SPORE/andrew.spdl
View File

@ -12,6 +12,7 @@
usertype SessionKey;
secret k: Function;
const succ: Function;
const Fresh: Function;
protocol andrew(I,R)
{
@ -25,8 +26,10 @@ protocol andrew(I,R)
read_2(R,I, {succ(ni),nr}k(I,R) );
send_3(I,R, {succ(nr)}k(I,R) );
read_4(R,I, {kir,nr2}k(I,R) );
claim_5(I,Secret,kir);
claim_6(I,Nisynch);
claim_I1(I,Secret,kir);
claim_I2(I,Nisynch);
claim_I3(I,Niagree);
claim_I4(I,Empty,(Fresh,kir));
}
role R
@ -39,8 +42,10 @@ protocol andrew(I,R)
send_2(R,I, {succ(ni),nr}k(I,R) );
read_3(I,R, {succ(nr)}k(I,R) );
send_4(R,I, {kir,nr2}k(I,R) );
claim_7(R,Secret,kir);
claim_8(R,Nisynch);
claim_R1(R,Secret,kir);
claim_R2(R,Nisynch);
claim_R3(R,Niagree);
claim_R4(R,Empty,(Fresh,kir));
}
}

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

@ -17,6 +17,7 @@ usertype TimeStamp;
secret k: Function;
usertype PseudoFunction;
const dec: PseudoFunction;
const Fresh: Function;
protocol denningSaccoLowe(I,R,S)
{
@ -32,7 +33,10 @@ protocol denningSaccoLowe(I,R,S)
send_3(I,R, W);
read_4(R,I, {Nr}Kir);
send_5(I,R, {{Nr}dec}Kir);
claim_6(I,Niagree);
claim_I1(I,Niagree);
claim_I2(I,Nisynch);
claim_I3(I,Secret,Kir);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
@ -44,7 +48,10 @@ protocol denningSaccoLowe(I,R,S)
read_3(I,R, {Kir,I,T}k(R,S));
send_4(R,I, {Nr}Kir);
read_5(I,R, {{Nr}dec}Kir);
claim_8(R,Niagree);
claim_R1(R,Niagree);
claim_R2(R,Nisynch);
claim_R3(R,Secret,Kir);
claim_R4(R,Empty,(Fresh,Kir));
}
role S

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

@ -12,6 +12,7 @@ usertype Key;
usertype SessionKey;
usertype TimeStamp;
secret k: Function;
const Fresh: Function;
protocol denningSacco(I,R,S)
{
@ -26,6 +27,8 @@ protocol denningSacco(I,R,S)
send_3(I,R, W);
claim_I1(I,Niagree);
claim_I2(I,Nisynch);
claim_I3(I,Secret,Kir);
claim_I4(I,Empty, (Fresh,Kir));
}
role R
@ -36,7 +39,8 @@ protocol denningSacco(I,R,S)
read_3(I,R, {Kir,I,T}k(R,S));
claim_R1(R,Niagree);
claim_R2(R,Nisynch);
claim_R3(R,Secret,Kir);
claim_R4(R,Empty, (Fresh,Kir));
}
role S

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

@ -10,6 +10,7 @@
usertype Sessionkey;
secret k: Function;
const Fresh: Function;
protocol kaochow2(I,R,S)
{
@ -23,9 +24,10 @@ protocol kaochow2(I,R,S)
read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr );
send_4 (I,R, {nr,kir}kt );
claim_5 (I, Nisynch);
claim_6 (I, Niagree);
claim_7 (I, Secret, kir);
claim_I1 (I, Nisynch);
claim_I2 (I, Niagree);
claim_I3 (I, Secret, kir);
claim_I4 (I, Empty, (Fresh,kir));
}
role R
@ -39,9 +41,10 @@ protocol kaochow2(I,R,S)
send_3 (R,I, R, T, {ni, kir}kt, nr );
read_4 (I,R, {nr,kir}kt );
claim_8 (R, Nisynch);
claim_9 (R, Niagree);
claim_10 (R, Secret, kir);
claim_R1 (R, Nisynch);
claim_R2 (R, Niagree);
claim_R3 (R, Secret, kir);
claim_R4 (R, Empty, (Fresh,kir));
}
role S

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

@ -11,6 +11,7 @@
usertype Sessionkey;
usertype Timestamp;
secret k: Function;
const Fresh: Function;
protocol kaochow3(I,R,S)
{
@ -25,9 +26,10 @@ protocol kaochow3(I,R,S)
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 );
claim_5 (I, Nisynch);
claim_6 (I, Niagree);
claim_7 (I, Secret, kir);
claim_I1 (I, Nisynch);
claim_I2 (I, Niagree);
claim_I3 (I, Secret, kir);
claim_I4 (I, Empty, (Fresh,kir));
}
role R
@ -42,9 +44,10 @@ protocol kaochow3(I,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) );
claim_8 (R, Nisynch);
claim_9 (R, Niagree);
claim_10 (R, Secret, kir);
claim_R1 (R, Nisynch);
claim_R2 (R, Niagree);
claim_R3 (R, Secret, kir);
claim_R4 (R, Empty, (Fresh,kir));
}
role S

15
spdl/SPORE/kaochow.spdl
View File

@ -10,6 +10,7 @@
usertype Sessionkey;
secret k: Function;
const Fresh: Function;
protocol kaochow(I,R,S)
{
@ -23,9 +24,10 @@ protocol kaochow(I,R,S)
read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr );
send_4 (I,R, {nr}kir );
claim_5 (I, Nisynch);
claim_6 (I, Niagree);
claim_7 (I, Secret, kir);
claim_I1 (I, Nisynch);
claim_I2 (I, Niagree);
claim_I3 (I, Secret, kir);
claim_I4 (I, Empty, (Fresh,kir));
}
role R
@ -39,9 +41,10 @@ protocol kaochow(I,R,S)
send_3 (R,I, T, {ni}kir, nr );
read_4 (I,R, {nr}kir );
claim_8 (R, Nisynch);
claim_9 (R, Niagree);
claim_10 (R, Secret, kir);
claim_R1 (R, Nisynch);
claim_R2 (R, Niagree);
claim_R3 (R, Secret, kir);
claim_R4 (R, Empty, (Fresh,kir));
}
role S

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

@ -16,6 +16,7 @@ secret k: Function;
const a, b, e: Agent;
const s: Server;
const Fresh: Function;
const ne: Nonce;
@ -43,6 +44,7 @@ protocol kslLowe(A,B,S)
claim_A1(A,Secret, Kab);
claim_A2(A,Niagree);
claim_A3(A,Nisynch);
claim_A4(A,Empty, (Fresh,Kab));
}
role B
@ -67,6 +69,7 @@ protocol kslLowe(A,B,S)
claim_B1(B,Secret, Kab);
claim_B2(B,Niagree);
claim_B3(B,Nisynch);
claim_B4(B,Empty, (Fresh,Kab));
}
role S

3
spdl/SPORE/ksl.spdl
View File

@ -14,6 +14,7 @@ secret k: Function;
const a, b, e: Agent;
const s: Server;
const Fresh: Function;
const ne: Nonce;
const kee: SessionKey;
@ -40,6 +41,7 @@ protocol ksl(A,B,S)
claim_A1(A,Secret, Kab);
claim_A2(A,Niagree);
claim_A3(A,Nisynch);
claim_A4(A,Empty, (Fresh, Kab));
}
role B
@ -64,6 +66,7 @@ protocol ksl(A,B,S)
claim_B1(B,Secret, Kab);
claim_B2(B,Niagree);
claim_B3(B,Nisynch);
claim_B4(B,Empty,(Fresh,Kab));
}
role S

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

@ -19,6 +19,7 @@ secret k: Function;
const dec,inc: Function;
inversekeys(dec,inc);
usertype SessionKey;
const Fresh: Function;
protocol needhamschroederskamend(I,R,S)
{
@ -39,6 +40,7 @@ protocol needhamschroederskamend(I,R,S)
claim_I2(I,Secret,Kir);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
@ -53,6 +55,7 @@ protocol needhamschroederskamend(I,R,S)
read_7(I,R,{{Nr}dec}Kir);
claim_R1(R,Secret,Nr);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S

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

@ -15,6 +15,7 @@ secret k: Function;
const dec,inc: Function;
inversekeys(dec,inc);
usertype SessionKey;
const Fresh: Function;
protocol needhamschroedersk(I,R,S)
{
@ -32,6 +33,7 @@ protocol needhamschroedersk(I,R,S)
send_5(I,R,{{Nr}dec}Kir);
claim_I2(I,Secret,Kir);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
@ -44,6 +46,7 @@ protocol needhamschroedersk(I,R,S)
read_5(I,R,{{Nr}dec}Kir);
claim_R1(R,Secret,Kir);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S

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

@ -17,6 +17,7 @@ secret k: Function;
const a, b, e: Agent;
const s: Server;
const Fresh: Function;
const ne: Nonce;
const kee: SessionKey;
@ -43,6 +44,7 @@ protocol neustubHwang(I,R,S)
claim_I1(I,Secret, Kir);
claim_I2(I,Niagree);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
@ -63,6 +65,7 @@ protocol neustubHwang(I,R,S)
claim_R1(R,Secret, Kir);
claim_R2(R,Niagree);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S

3
spdl/SPORE/neumannstub.spdl
View File

@ -14,6 +14,7 @@ secret k: Function;
const a, b, e: Agent;
const s: Server;
const Fresh: Function;
const ne: Nonce;
const kee: SessionKey;
@ -40,6 +41,7 @@ protocol neustub(I,R,S)
claim_I1(I,Secret, Kir);
claim_I2(I,Niagree);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
@ -60,6 +62,7 @@ protocol neustub(I,R,S)
claim_R1(R,Secret, Kir);
claim_R2(R,Niagree);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S

7
spdl/SPORE/otwayrees.spdl
View File

@ -11,6 +11,7 @@
secret const k : Function;
const Fresh: Function;
usertype String,SessionKey;
@ -26,7 +27,8 @@ protocol otwayrees(I,R,S)
read_4(R,I, M,{Ni,Kir}k(I,S) );
claim_I1(I, Secret,Kir);
#claim_I2(I, Nisynch);
claim_I2(I, Nisynch);
claim_I3(I, Empty, (Fresh,Kir));
}
role R
@ -42,7 +44,8 @@ protocol otwayrees(I,R,S)
send_4(R,I, M, T2 );
claim_R1(R, Secret,Kir);
#claim_R2(R, Nisynch);
claim_R2(R, Nisynch);
claim_R3(R, Empty, (Fresh,Kir));
}
role S

11
spdl/SPORE/tmn.spdl
View File

@ -3,12 +3,16 @@
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/tmn.html
#
# Note:
# According to Boyd and Mathuria Kb is the session key this is not clear
# from the description in SPORE
usertype Key;
const pk: Function;
secret sk: Function;
inversekeys(pk,sk);
const Fresh: Function;
protocol tmn(I,R,S)
{
@ -20,8 +24,9 @@ protocol tmn(I,R,S)
send_1(I,S, R,{Ki}pk(S) );
read_4(S,I, R,{Kr}Ki );
claim_I1(I,Secret,Ki);
claim_I2(I,Secret,Kr);
claim_I1(I,Secret,Kr);
claim_I2(I,Nisynch);
claim_I3(I,Empty,(Fresh,Kr));
}
role R
@ -32,6 +37,8 @@ protocol tmn(I,R,S)
send_3(R,S, I, { Kr }pk(S) );
claim_R1(R,Secret,Kr);
claim_R2(R,Nisynch);
claim_R3(R,Empty,(Fresh,Kr));
}
role S

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

@ -13,6 +13,7 @@ usertype Key;
usertype TimeStamp;
const succ,pred: Function;
inversekeys (succ,pred);
const Fresh: Function;
secret k: Function;
@ -31,6 +32,7 @@ protocol wmfLowe(I,R,S)
claim_I1(I,Secret,Kir);
claim_I2(I,Nisynch);
claim_I3(I,Empty,(Fresh,Kir));
}
role R
@ -45,6 +47,7 @@ protocol wmfLowe(I,R,S)
claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch);
claim_R3(R,Empty,(Fresh,Kir));
}
role S

3
spdl/SPORE/wmf.spdl
View File

@ -8,6 +8,7 @@ usertype Key;
usertype TimeStamp;
secret k: Function;
const Fresh: Function;
protocol wmf(I,R,S)
{
@ -20,6 +21,7 @@ protocol wmf(I,R,S)
send_1(I,S, I, {Ti, R, Kir}k(I,S));
claim_I1(I,Secret,Kir);
claim_I2(I,Empty,(Fresh,Kir));
}
role R
@ -31,6 +33,7 @@ protocol wmf(I,R,S)
claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch);
claim_R3(R,Empty,(Fresh,Kir));
}
role S

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

@ -12,6 +12,7 @@
usertype Key;
secret k: Function;
const Fresh: Function;
protocol woolam(I,R,S)
{
@ -30,6 +31,7 @@ protocol woolam(I,R,S)
claim_I1(I,Secret,Kir);
claim_I2(I,Nisynch);
claim_I3(I,Empty,(Fresh,Kir));
}
role R
@ -49,6 +51,7 @@ protocol woolam(I,R,S)
claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch);
claim_R3(R,Empty,(Fresh,Kir));
}
role S

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

@ -11,6 +11,7 @@
secret k : Function;
usertype Key;
const Fresh: Function;
protocol yahalomBAN(I,R,S)
@ -28,6 +29,7 @@ protocol yahalomBAN(I,R,S)
claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch);
claim_I3(I, Empty, (Fresh,Kir));
}
role R
@ -43,6 +45,7 @@ protocol yahalomBAN(I,R,S)
claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch);
claim_R3(R, Empty, (Fresh,Kir));
}
role S

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

@ -9,6 +9,7 @@
#
secret k : Function;
const Fresh: Function;
usertype Key;
@ -28,6 +29,7 @@ protocol yahalomPaulson(I,R,S)
claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch);
claim_I3(I, Empty, (Fresh,Kir));
}
role R
@ -43,6 +45,7 @@ protocol yahalomPaulson(I,R,S)
claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch);
claim_R3(R, Empty, (Fresh,Kir));
}
role S

3
spdl/SPORE/yahalom.spdl
View File

@ -11,6 +11,7 @@
secret k : Function;
usertype Key;
const Fresh: Function;
protocol yahalom(I,R,S)
@ -28,6 +29,7 @@ protocol yahalom(I,R,S)
claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch);
claim_I3(I, Empty, (Fresh,Kir));
}
role R
@ -43,6 +45,7 @@ protocol yahalom(I,R,S)
claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch);
claim_R3(R, Empty, (Fresh,Kir));
}
role S