- Using the scyther.py -e command, I found and fixed some errors.
This commit is contained in:
parent
531f0aa469
commit
533cf46080
@ -14,9 +14,9 @@ protocol kaochow(I,R,S)
|
|||||||
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 (R, Nisynch);
|
claim_5 (I, Nisynch);
|
||||||
claim_6 (R, Niagree);
|
claim_6 (I, Niagree);
|
||||||
claim_7 (R, Secret, kir);
|
claim_7 (I, Secret, kir);
|
||||||
}
|
}
|
||||||
|
|
||||||
role R
|
role R
|
||||||
|
@ -12,8 +12,8 @@ protocol nsl7(I,R)
|
|||||||
read_1(I,R, {I,ni}pk(R) );
|
read_1(I,R, {I,ni}pk(R) );
|
||||||
send_2(R,I, {ni,nr,R}pk(I) );
|
send_2(R,I, {ni,nr,R}pk(I) );
|
||||||
read_3(I,R, {nr}pk(R) );
|
read_3(I,R, {nr}pk(R) );
|
||||||
claim_4(I,Secret,ni);
|
claim_4(R,Secret,ni);
|
||||||
claim_5(I,Secret,nr);
|
claim_5(R,Secret,nr);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -9,7 +9,7 @@ secret sk: Function;
|
|||||||
|
|
||||||
inversekeys (pk,sk);
|
inversekeys (pk,sk);
|
||||||
|
|
||||||
protocol samasc-broken(I,R)
|
protocol samascbroken(I,R)
|
||||||
{
|
{
|
||||||
role R
|
role R
|
||||||
{
|
{
|
||||||
|
@ -23,7 +23,7 @@ protocol ns3speedtest(I,R)
|
|||||||
read_1(I,R, {I,ni}pk(R) );
|
read_1(I,R, {I,ni}pk(R) );
|
||||||
send_2(R,I, {ni,nr}pk(I) );
|
send_2(R,I, {ni,nr}pk(I) );
|
||||||
read_3(I,R, {nr}pk(R) );
|
read_3(I,R, {nr}pk(R) );
|
||||||
claim_5(I,Secret,ni);
|
claim_5(R,Secret,ni);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -66,7 +66,7 @@ protocol woolamcmv(A,B,S)
|
|||||||
read_4(B,S, { A,B, Na,Nb }k(A,S), { A,B,Na,Nb }k(B,S) );
|
read_4(B,S, { A,B, Na,Nb }k(A,S), { A,B,Na,Nb }k(B,S) );
|
||||||
send_5(S,B, { B,Na,Nb,Kab }k(A,S), { A,Na,Nb,Kab }k(B,S) );
|
send_5(S,B, { B,Na,Nb,Kab }k(A,S), { A,Na,Nb,Kab }k(B,S) );
|
||||||
|
|
||||||
claim_10(S,Secret, Kab);
|
claim_14(S,Secret, Kab);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user