6f6cb322dc
however, later this was changed, and now the tool assumes that events have labels. This should be explicitly checked of course.
51 lines
1.1 KiB
Plaintext
51 lines
1.1 KiB
Plaintext
# CCITT X.509 (1c)
|
|
#
|
|
# Modelled after the description in the SPORE library
|
|
# http://www.lsv.ens-cachan.fr/spore/ccittx509_1c.html
|
|
#
|
|
# Note:
|
|
# According to SPORE there are no known attacks on this protocol
|
|
#
|
|
|
|
const pk,hash: Function;
|
|
secret sk,unhash: Function;
|
|
inversekeys (hash,unhash);
|
|
inversekeys(pk,sk);
|
|
usertype Timestamp;
|
|
|
|
protocol ccitt5091c(I,R)
|
|
{
|
|
role I
|
|
{
|
|
const Ta: Timestamp;
|
|
const Na,Xa,Ya: Nonce;
|
|
send_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I));
|
|
# claim_2(I,Nisynch);
|
|
# This claim is useless as there are no preceding read events
|
|
}
|
|
|
|
role R
|
|
{
|
|
var Ta: Timestamp;
|
|
var Na,Xa,Ya: Nonce;
|
|
|
|
read_2(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I));
|
|
claim_3(R,Nisynch);
|
|
# There should also be Fresh Xa and Fresh Ya claims here
|
|
}
|
|
}
|
|
|
|
const Alice,Bob,Eve: Agent;
|
|
|
|
untrusted Eve;
|
|
const ne: Nonce;
|
|
const te: Timestamp;
|
|
compromised sk(Eve);
|
|
|
|
# General scenario, 2 parallel runs of the protocol
|
|
|
|
run ccitt5091c.I(Agent,Agent);
|
|
run ccitt5091c.R(Agent,Agent);
|
|
run ccitt5091c.I(Agent,Agent);
|
|
run ccitt5091c.R(Agent,Agent);
|