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

- Fix 2 incomplete/incorrect modellings

Browse Source
This commit is contained in:
gijs 2005-08-22 13:52:29 +00:00
parent e104dddbfb
commit 40f881b125
2 changed files with 7 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -24,7 +24,9 @@ protocol ccitt509-3(I,R)
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));
send_3(I,R, I, {Nb}sk(I));
claim_4(I,Nisynch);
claim_I1(I,Nisynch);
claim_I2(I,Secret,Ya);
claim_I3(I,Secret,Yb);
}
role R
@ -37,7 +39,9 @@ protocol ccitt509-3(I,R)
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));
read_3(I,R, I, {Nb}sk(I));
claim_5(R,Nisynch);
claim_R1(R,Nisynch);
claim_R2(R,Secret,Ya);
claim_R3(R,Secret,Yb);
# There should also be Fresh Xa and Fresh Ya claims here
}
}

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

@ -28,7 +28,7 @@ protocol denningSacco-Lowe^KeyCompromise(C)
role C {
const Ni,Nr: Nonce;
const Kir: SessionKey;
const T: TimeStamp;
const T: ExpiredTimeStamp;
var I,R,S: Agent;
read_C1(C,C, I,R,S);