- Fixed a protocol. The BNF of Scyther allows for non-labeled events;
however, later this was changed, and now the tool assumes that events have labels. This should be explicitly checked of course.
This commit is contained in:
parent
113a3c5dfc
commit
6f6cb322dc
@ -29,7 +29,7 @@ protocol ccitt5091c(I,R)
|
|||||||
var Ta: Timestamp;
|
var Ta: Timestamp;
|
||||||
var Na,Xa,Ya: Nonce;
|
var Na,Xa,Ya: Nonce;
|
||||||
|
|
||||||
read(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I));
|
read_2(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I));
|
||||||
claim_3(R,Nisynch);
|
claim_3(R,Nisynch);
|
||||||
# There should also be Fresh Xa and Fresh Ya claims here
|
# There should also be Fresh Xa and Fresh Ya claims here
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user