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

- Use variable type SessionKey every where instead of a combination

Browse Source 
between Key and SessionKey
- Make KSL working again
This commit is contained in:
gijs 2005-06-29 12:42:25 +00:00
parent eef9072324
commit 49cd9b1271
9 changed files with 71 additions and 71 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

49
spdl/SPORE/ksl.spdl
View File

@ -12,14 +12,15 @@
usertype Server, SessionKey, GeneralizedTimestamp, TicketKey; usertype Server, SessionKey, GeneralizedTimestamp, TicketKey;
secret k: Function; secret k: Function;
const Alice, Bob, Simon, Eve: Agent; const a, b, e: Agent;
const s: Server;
const Fresh: Function; const Fresh: Function;
const Compromised: Function; const Compromised: Function;
const ne: Nonce; const ne: Nonce;
const kee: SessionKey; const kee: SessionKey;
untrusted Eve; untrusted e;
compromised k(Eve,Simon); compromised k(e,s);
protocol kslSessionKeyCompromise(C) protocol kslSessionKeyCompromise(C)
{ {
@ -36,7 +37,7 @@ protocol kslSessionKeyCompromise(C)
send_C2(C,C, (Ni,I), send_C2(C,C, (Ni,I),
(Ni,I,Nr,R), (Ni,I,Nr,R),
{Nr,I,Kir}k(R,S),{Ni,R,Kir}k(I,S), {Nr,I,Kir}k(R,S),{Ni,R,Kir}k(I,S),
{Tr,I,Kir}Kbb,Nc,{Ni}Kir, {Tr,I,Kir}Kbb,Nc,{Ni}k(I,R),
{Nc}Kir, {Nc}Kir,
Ma, Ma,
Mb,{Ma}Kir, Mb,{Ma}Kir,
@ -50,34 +51,34 @@ protocol kslSessionKeyCompromise(C)
} }
protocol ksl(I,R,S) protocol ksl(A,B,S)
{ {
role I role A
{ {
const Ni, Mi: Nonce; const Na, Ma: Nonce;
var Nr2, Mr: Nonce; var Nc, Mb: Nonce;
var T: Ticket; var T: Ticket;
var Kir: SessionKey; var Kab: SessionKey;
send_1(I,R, Ni, I); send_1(A,B, Na, A);
read_4(R,I, {Ni,R,Kir}k(I,S), T, Nr2, {Ni}Kir); read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab );
send_5(I,R, {Nr2}Kir ); send_5(A,B, { Nc }Kab );
send_6(I,R, Mi,T ); send_6(A,B, Ma,T );
read_7(R,I, Mr,{Mi}Kir ); read_7(B,A, Mb,{Ma}Kab );
send_8(I,R, {Mr}Kir ); send_8(A,B, {Mb}Kab );
claim_A1(A,Secret, Kab); claim_I1(A,Secret, Kab);
claim_A2(A,Niagree); claim_I2(A,Niagree);
claim_A3(A,Nisynch); claim_I3(A,Nisynch);
claim_A4(A,Empty, (Fresh, Kab)); claim_I4(A,Empty, (Fresh, Kab));
} }
role B role B
{ {
var Na,Ma: Nonce; var Na,Ma: Nonce;
const Nr,Nr2,Mr: Nonce; const Nb,Nc,Mb: Nonce;
var Kir: SessionKey; var Kab: SessionKey;
const Kbb: TicketKey; const Kbb: TicketKey;
const Tb: GeneralizedTimestamp; const Tb: GeneralizedTimestamp;
var T: Ticket; var T: Ticket;
@ -108,7 +109,7 @@ protocol ksl(I,R,S)
} }
} }
run ksl.A(Alice,Bob,Simon); run ksl.A(a,b,s);
run ksl.B(Alice,Bob,Simon); run ksl.B(a,b,s);
run ksl.S(Alice,Bob,Simon); run ksl.S(a,b,s);

15
spdl/SPORE/tmn.spdl
View File

@ -6,8 +6,7 @@
# Note: # Note:
# According to Boyd and Mathuria Kb is the session key this is not clear # According to Boyd and Mathuria Kb is the session key this is not clear
# from the description in SPORE # from the description in SPORE
usertype SessionKey;
usertype Key;
const pk: Function; const pk: Function;
secret sk: Function; secret sk: Function;
@ -21,7 +20,7 @@ protocol tmnSessionKeyCompromise(C)
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise
role C { role C {
const Ni,Nr: Nonce; const Ni,Nr: Nonce;
const Kr,Ki: Key; const Kr,Ki: SessionKey;
var I,R,S: Agent; var I,R,S: Agent;
read_C1(C,C, I,R,S); read_C1(C,C, I,R,S);
@ -38,8 +37,8 @@ protocol tmn(I,R,S)
{ {
role I role I
{ {
const Ki: Key; const Ki: SessionKey;
var Kr: Key; var Kr: SessionKey;
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 );
@ -51,7 +50,7 @@ protocol tmn(I,R,S)
role R role R
{ {
const Kr: Key; const Kr: SessionKey;
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) );
@ -63,7 +62,7 @@ protocol tmn(I,R,S)
role S role S
{ {
var Ki,Kr: Key; var Ki,Kr: SessionKey;
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 );
@ -73,7 +72,7 @@ protocol tmn(I,R,S)
} }
const Alice,Bob,Eve,Simon: Agent; const Alice,Bob,Eve,Simon: Agent;
const Ke: Key; const Ke: SessionKey;
untrusted Eve; untrusted Eve;

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

@ -9,7 +9,7 @@
# agent can recognise and will reject to read messages that it has created # agent can recognise and will reject to read messages that it has created
# itself. # itself.
usertype Key; usertype SessionKey;
usertype TimeStamp; usertype TimeStamp;
const succ,pred: Function; const succ,pred: Function;
inversekeys (succ,pred); inversekeys (succ,pred);
@ -24,7 +24,7 @@ protocol wmfLoweSessionKeyCompromise(C)
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise
role C { role C {
const Ni,Nr: Nonce; const Ni,Nr: Nonce;
const Kir: Key; const Kir: SessionKey;
const Ti,Ts: TimeStamp; const Ti,Ts: TimeStamp;
var I,R,S: Agent; var I,R,S: Agent;
@ -43,9 +43,9 @@ protocol wmfLowe(I,R,S)
{ {
role I role I
{ {
const Kir: Key; const Kir: SessionKey;
const Ti: TimeStamp; const Ti: TimeStamp;
var Kr: Key; var Kr: SessionKey;
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));
@ -60,7 +60,7 @@ protocol wmfLowe(I,R,S)
role R role R
{ {
var Ts: TimeStamp; var Ts: TimeStamp;
var Kir: Key; var Kir: SessionKey;
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) );
@ -74,7 +74,7 @@ protocol wmfLowe(I,R,S)
role S role S
{ {
var Kir: Key; var Kir: SessionKey;
const Ts: TimeStamp; const Ts: TimeStamp;
var Ti: TimeStamp; var Ti: TimeStamp;
@ -84,7 +84,7 @@ protocol wmfLowe(I,R,S)
} }
const Alice,Bob,Eve,Simon: Agent; const Alice,Bob,Eve,Simon: Agent;
const Ke: Key; const Ke: SessionKey;
const Te: TimeStamp; const Te: TimeStamp;

14
spdl/SPORE/wmf.spdl
View File

@ -4,7 +4,7 @@
# http://www.lsv.ens-cachan.fr/spore/wideMouthedFrog.html # http://www.lsv.ens-cachan.fr/spore/wideMouthedFrog.html
# #
usertype Key; usertype SessionKey;
usertype TimeStamp; usertype TimeStamp;
secret k: Function; secret k: Function;
@ -17,7 +17,7 @@ protocol wmfSessionKeyCompromise(C)
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise
role C { role C {
const Ni,Nr: Nonce; const Ni,Nr: Nonce;
const Kir: Key; const Kir: SessionKey;
const Ti,Ts: TimeStamp; const Ti,Ts: TimeStamp;
var I,R,S: Agent; var I,R,S: Agent;
@ -34,9 +34,9 @@ protocol wmf(I,R,S)
{ {
role I role I
{ {
const Kir: Key; const Kir: SessionKey;
const Ti: TimeStamp; const Ti: TimeStamp;
var Kr: Key; var Kr: SessionKey;
send_1(I,S, I, {Ti, R, Kir}k(I,S)); send_1(I,S, I, {Ti, R, Kir}k(I,S));
@ -47,7 +47,7 @@ protocol wmf(I,R,S)
role R role R
{ {
var Ts: TimeStamp; var Ts: TimeStamp;
var Kir: Key; var Kir: SessionKey;
read_2(S,R, {Ts, I, Kir}k(R,S) ); read_2(S,R, {Ts, I, Kir}k(R,S) );
@ -58,7 +58,7 @@ protocol wmf(I,R,S)
role S role S
{ {
var Kir: Key; var Kir: SessionKey;
const Ts: TimeStamp; const Ts: TimeStamp;
var Ti: TimeStamp; var Ti: TimeStamp;
@ -68,7 +68,7 @@ protocol wmf(I,R,S)
} }
const Alice,Bob,Eve,Simon: Agent; const Alice,Bob,Eve,Simon: Agent;
const Ke: Key; const Ke: SessionKey;
const Te: TimeStamp; const Te: TimeStamp;

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

@ -9,7 +9,7 @@
# #
usertype Key; usertype SessionKey;
secret k: Function; secret k: Function;
const Fresh: Function; const Fresh: Function;
@ -21,7 +21,7 @@ protocol woolamSessionKeyCompromise(C)
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise
role C { role C {
const N1,N2: Nonce; const N1,N2: Nonce;
const Kir: Key; const Kir: SessionKey;
var I,R,S: Agent; var I,R,S: Agent;
read_C1(C,C, I,R,S); read_C1(C,C, I,R,S);
@ -44,7 +44,7 @@ protocol woolam(I,R,S)
role I role I
{ {
const N1: Nonce; const N1: Nonce;
var Kir: Key; var Kir: SessionKey;
var N2: Nonce; var N2: Nonce;
send_1(I,R, I, N1); send_1(I,R, I, N1);
@ -63,7 +63,7 @@ protocol woolam(I,R,S)
{ {
const N2: Nonce; const N2: Nonce;
var N1: Nonce; var N1: Nonce;
var Kir: Key; var Kir: SessionKey;
var T1,T2: Ticket; var T1,T2: Ticket;
read_1(I,R, I, N1); read_1(I,R, I, N1);
@ -81,7 +81,7 @@ protocol woolam(I,R,S)
role S role S
{ {
const Kir: Key; const Kir: SessionKey;
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));
@ -90,7 +90,7 @@ protocol woolam(I,R,S)
} }
const Alice,Bob,Eve,Simon: Agent; const Alice,Bob,Eve,Simon: Agent;
const Ke: Key; const Ke: SessionKey;
const Te: Ticket; const Te: Ticket;
const Ne: Nonce; const Ne: Nonce;

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

@ -10,7 +10,7 @@
secret k : Function; secret k : Function;
usertype Key; usertype SessionKey;
const Fresh: Function; const Fresh: Function;
const Compromised: Function; const Compromised: Function;
@ -20,7 +20,7 @@ protocol yahalomBANSessionKeyCompromise(C)
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise
role C { role C {
const Ni,Nr: Nonce; const Ni,Nr: Nonce;
const Kir: Key; const Kir: SessionKey;
var I,R,S: Agent; var I,R,S: Agent;
read_C1(C,C, I,R,S); read_C1(C,C, I,R,S);
@ -44,7 +44,7 @@ protocol yahalomBAN(I,R,S)
const Ni: Nonce; const Ni: Nonce;
var Nr: Nonce; var Nr: Nonce;
var T: Ticket; var T: Ticket;
var Kir: Key; var Kir: SessionKey;
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 );
@ -60,7 +60,7 @@ protocol yahalomBAN(I,R,S)
const Nr: Nonce; const Nr: Nonce;
var Ni: Nonce; var Ni: Nonce;
var T: Ticket; var T: Ticket;
var Kir: Key; var Kir: SessionKey;
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) );
@ -73,7 +73,7 @@ protocol yahalomBAN(I,R,S)
role S role S
{ {
const Kir: Key; const Kir: SessionKey;
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) );

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

@ -7,7 +7,7 @@
secret k : Function; secret k : Function;
usertype Key; usertype SessionKey;
protocol yahalomLowe(I,R,S) protocol yahalomLowe(I,R,S)
@ -16,7 +16,7 @@ protocol yahalomLowe(I,R,S)
{ {
const Ni: Nonce; const Ni: Nonce;
var Nr: Nonce; var Nr: Nonce;
var Kir: Key; var Kir: SessionKey;
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) );
@ -30,7 +30,7 @@ protocol yahalomLowe(I,R,S)
{ {
const Nr: Nonce; const Nr: Nonce;
var Ni: Nonce; var Ni: Nonce;
var Kir: Key; var Kir: SessionKey;
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) );
@ -43,7 +43,7 @@ protocol yahalomLowe(I,R,S)
role S role S
{ {
const Kir: Key; const Kir: SessionKey;
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) );

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

@ -12,7 +12,7 @@ secret k : Function;
const Fresh: Function; const Fresh: Function;
const Compromised: Function; const Compromised: Function;
usertype Key; usertype SessionKey;
protocol yahalomPaulsonSessionKeyCompromise(C) protocol yahalomPaulsonSessionKeyCompromise(C)
{ {
@ -20,7 +20,7 @@ protocol yahalomPaulsonSessionKeyCompromise(C)
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise
role C { role C {
const Ni,Nr: Nonce; const Ni,Nr: Nonce;
const Kir: Key; const Kir: SessionKey;
var I,R,S: Agent; var I,R,S: Agent;
read_C1(C,C, I,R,S); read_C1(C,C, I,R,S);
@ -43,7 +43,7 @@ protocol yahalomPaulson(I,R,S)
const Ni: Nonce; const Ni: Nonce;
var Nr: Nonce; var Nr: Nonce;
var T: Ticket; var T: Ticket;
var Kir: Key; var Kir: SessionKey;
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 );
@ -59,7 +59,7 @@ protocol yahalomPaulson(I,R,S)
const Nr: Nonce; const Nr: Nonce;
var Ni: Nonce; var Ni: Nonce;
var T: Ticket; var T: Ticket;
var Kir: Key; var Kir: SessionKey;
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) );
@ -72,7 +72,7 @@ protocol yahalomPaulson(I,R,S)
role S role S
{ {
const Kir: Key; const Kir: SessionKey;
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) );

10
spdl/SPORE/yahalom.spdl
View File

@ -10,7 +10,7 @@
secret k : Function; secret k : Function;
usertype Key; usertype SessionKey;
const Fresh: Function; const Fresh: Function;
const Compromised: Function; const Compromised: Function;
@ -20,7 +20,7 @@ protocol yahalomSessionKeyCompromise(C)
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise
role C { role C {
const Ni,Nr: Nonce; const Ni,Nr: Nonce;
const Kir: Key; const Kir: SessionKey;
var I,R,S: Agent; var I,R,S: Agent;
read_C1(C,C, I,R,S); read_C1(C,C, I,R,S);
@ -43,7 +43,7 @@ protocol yahalom(I,R,S)
const Ni: Nonce; const Ni: Nonce;
var Nr: Nonce; var Nr: Nonce;
var T: Ticket; var T: Ticket;
var Kir: Key; var Kir: SessionKey;
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 );
@ -59,7 +59,7 @@ protocol yahalom(I,R,S)
const Nr: Nonce; const Nr: Nonce;
var Ni: Nonce; var Ni: Nonce;
var T: Ticket; var T: Ticket;
var Kir: Key; var Kir: SessionKey;
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) );
@ -72,7 +72,7 @@ protocol yahalom(I,R,S)
role S role S
{ {
const Kir: Key; const Kir: SessionKey;
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) );