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

- Fixed a modelling error in the key compromise part of WMF-Lowe

Browse Source 
- Included agent names in WMF-Lowe messages
This commit is contained in:
gijs 2005-07-04 13:40:09 +00:00
parent 92356a2d43
commit 53e7a7c55d
1 changed files with 12 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -29,10 +29,10 @@ protocol wmfLoweSessionKeyCompromise(C)
var I,R,S: Agent; var I,R,S: Agent;
read_C1(C,C, I,R,S); read_C1(C,C, I,R,S);
send_C2(C,C, I, {Ti,R,Kir}k(I,S), send_C2(C,C, I, {I,Ti,R,Kir}k(I,S),
{Ts,I,Kir}k(R,S), {S,Ts,I,Kir}k(R,S),
{Nr}k(I,S), {R,Nr}Kir,
{{Nr}succ}k(I,S), {I,{Nr}succ}Kir,
Kir Kir
); );
claim_C3(C,Empty, (Compromised,Kir)); claim_C3(C,Empty, (Compromised,Kir));
@ -48,9 +48,9 @@ protocol wmfLowe(I,R,S)
var Kr: SessionKey; 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, {I, Ti, R, Kir}k(I,S));
read_3(R,I,{Nr}Kir); read_3(R,I,{R,Nr}Kir);
send_4(I,R,{{Nr}succ}Kir); send_4(I,R,{I,{Nr}succ}Kir);
claim_I1(I,Secret,Kir); claim_I1(I,Secret,Kir);
claim_I2(I,Nisynch); claim_I2(I,Nisynch);
@ -63,9 +63,9 @@ protocol wmfLowe(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
const Nr: Nonce; const Nr: Nonce;
read_2(S,R, {Ts, I, Kir}k(R,S) ); read_2(S,R, {S, Ts, I, Kir}k(R,S) );
send_3(R,I, {Nr}Kir); send_3(R,I, {R, Nr}Kir);
read_4(I,R, {{Nr}succ}Kir); read_4(I,R, {I,{Nr}succ}Kir);
claim_R1(R,Secret,Kir); claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
@ -78,8 +78,8 @@ protocol wmfLowe(I,R,S)
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,{I,Ti, R, Kir}k(I,S) );
send_2(S,R, {Ts, I, Kir}k(R,S)); send_2(S,R, {R,Ts, I, Kir}k(R,S));
} }
} }