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

- Added SPORE protocols.

Browse Source
This commit is contained in:
ccremers 2006-11-21 13:42:06 +00:00
parent 567d629dd0
commit 45dbcfad21
44 changed files with 3593 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
spdl/SPORE/NotModelled.txt Normal file
View File

@ -0,0 +1,23 @@
The following protocols have not been modelled for use in Scyther:
- CAM http://www.lsv.ens-cachan.fr/spore/cam.html
This protocol only consists of one message and corresponding database actions.
The description given in SPORE is unsuitable for formalisation.
- Diffie Helman http://www.lsv.ens-cachan.fr/spore/diffieHelman.html
This protocol relies on algebraic properties that can not be modelled in
scyther.
- GJM http://www.lsv.ens-cachan.fr/spore/gjm.html
This protocol contains complicated if-then-else constructions that can
not be modelled in scyther.
- Gong http://www.lsv.ens-cachan.fr/spore/gong.html
This protocol relies on algebraic properties that can not be modelled in
scyther.
- SK3
This protocol relies on algebraic properties that can not be modelled in
scyther. It also has the notion of channels that can not be attacked,
which can not be modelled in scyther either.

96
spdl/SPORE/andrew-ban-concrete.spdl Normal file
View File

@ -0,0 +1,96 @@
# BAN concrete Andrew Secure RPC
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/andrewBAN2.html
#
# Note:
# The shared key between I and R is modelled as k(I,R) currently
# there is no way to express that this key is equal to k(R,I)
# In order to overcome this a 'dummy' role X has been hadded that recrypts
# a given term crypted with k(I,R) with k(R,I)
#
# Note:
# Read 4 by the Initatior has been placed after the synchronisation claim
# as it allows trivial synchronisation attacks otherwise (the message is
# completely fresh and can therefore always be replaced by an arbitrary value
# created by the intruder) which are not considered in SPORE
#
usertype SessionKey;
secret k: Function;
const Fresh: Function;
const Compromised: Function;
protocol @swapkey(X)
{
# Protocol added to work around the symmetry problems where k(I,R) != k(R,I)
role X
{
var I,R: Agent;
var T:Ticket;
read_X1(X,X,I,R,{T}k(I,R));
send_X2(X,X,{T}k(R,I));
}
}
protocol andrew-Concrete^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const ni,nr: Nonce;
const kir: SessionKey;
var I,R: Agent;
read_C1(C,C, I,R);
send_C2(C,C, (I,ni),
{ni,kir}k(I,R),
{ni}kir,
nr,
kir
);
claim_C3(C,Empty, (Compromised,kir));
}
}
protocol andrew-Concrete(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
var kir: SessionKey;
send_1(I,R, I,ni );
read_2(R,I, {ni,kir}k(I,R) );
send_3(I,R, {ni}kir);
claim_I1(I,Secret,kir);
claim_I2(I,Nisynch);
claim_I3(I,Empty,(Fresh,kir));
read_6(R,I, nr);
}
role R
{
var ni: Nonce;
const nr: Nonce;
const kir: SessionKey;
read_1(I,R, I,ni );
send_2(R,I, {ni,kir}k(I,R) );
read_3(I,R, {ni}kir);
send_6(R,I, nr);
claim_R1(R,Secret,kir);
claim_R2(R,Nisynch);
claim_R3(R,Empty,(Fresh,kir));
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;
const kee: SessionKey;

86
spdl/SPORE/andrew-ban.spdl Normal file
View File

@ -0,0 +1,86 @@
# BAN modified Andrew Secure RPC
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/andrewBAN.html
#
# Note:
# The shared key between I and R is modelled as k(I,R) currently
# there is no way to express that this key is equal to k(R,I)
# So it is possile that certain attacks that use this property are not found
#
# Note:
# According to SPORE there are no known attacks on this protocol
#
usertype SessionKey;
secret k: Function;
const Fresh: Function;
const Compromised: Function;
protocol andrew-Ban^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const ni,nr,nr2: Nonce;
const kir: SessionKey;
var I,R: Agent;
read_C1(C,C, I,R);
send_C2(C,C, (I,{ni}k(I,R)),
{ni,nr}k(I,R),
{nr}k(I,R),
{kir,nr2,ni}k(I,R),
kir
);
claim_C3(C,Empty, (Compromised,kir));
}
}
protocol andrew-Ban(I,R)
{
role I
{
const ni: Nonce;
var nr,nr2: Nonce;
var kir: SessionKey;
send_1(I,R, I,{ni}k(I,R) );
read_2(R,I, {ni,nr}k(I,R) );
send_3(I,R, {nr}k(I,R) );
read_4(R,I, {kir,nr2,ni}k(I,R) );
claim_I1(I,Nisynch);
claim_I2(I,Niagree);
claim_I3(I,Secret, kir);
claim_I4(I,Secret, k(I,R));
claim_I5(I,Empty, (Fresh,kir));
}
role R
{
var ni: Nonce;
const nr,nr2: Nonce;
const kir: SessionKey;
read_1(I,R, I,{ni}k(I,R) );
send_2(R,I, {ni,nr}k(I,R) );
read_3(I,R, {nr}k(I,R) );
send_4(R,I, {kir,nr2,ni}k(I,R) );
claim_R1(R,Nisynch);
claim_R2(R,Niagree);
claim_R3(R,Secret, kir);
claim_R4(R,Secret, k(I,R));
claim_R5(R,Empty, (Fresh,kir));
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;
const kee: SessionKey;
compromised k(Eve,Eve);
compromised k(Eve,Alice);
compromised k(Eve,Bob);
compromised k(Alice,Eve);
compromised k(Bob,Eve);

91
spdl/SPORE/andrew-lowe-ban.spdl Normal file
View File

@ -0,0 +1,91 @@
# Lowe modified BAN concrete Andrew Secure RPC
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/andrewLowe.html
#
# Note:
# The shared key between I and R is modelled as k(I,R) currently
# there is no way to express that this key is equal to k(R,I)
# So it is possile that certain attacks that use this property are not found
#
# Note:
# Read 4 by the Initatior has been placed after the synchronisation claim
# as it allows trivial synchronisation attacks otherwise (the message is
# completely fresh and can therefore always be replaced by an arbitrary value
# created by the intruder) which are not considered in SPORE
#
# Note:
# According to SPORE there are no known attacks on this protocol
#
usertype SessionKey;
secret k: Function;
const Fresh: Function;
const Compromised: Function;
protocol andrew-LoweBan^KeyCompromise(C)
{
// Read the names of 2 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const ni,nr: Nonce;
const kir: SessionKey;
var I,R: Agent;
read_C1(C,C, I,R);
send_C2(C,C, (I,ni),
{ni,kir,R}k(I,R),
{ni}kir,
nr,
kir
);
claim_C3(C,Empty, (Compromised,kir));
}
}
protocol andrew-LoweBan(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
var kir: SessionKey;
send_1(I,R, I,ni );
read_2(R,I, {ni,kir,R}k(I,R) );
send_3(I,R, {ni}kir );
claim_I1(I,Nisynch);
claim_I2(I,Secret, kir);
claim_I3(I,Empty, (Fresh,kir));
read_4(R,I, nr );
}
role R
{
var ni: Nonce;
const nr: Nonce;
const kir: SessionKey;
read_1(I,R, I,ni );
send_2(R,I, {ni,kir,R}k(I,R) );
read_3(I,R, {ni}kir );
send_4(R,I, nr );
claim_R1(R,Nisynch);
claim_R2(R,Secret, kir);
claim_R3(R,Empty, (Fresh,kir));
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;
const kee: SessionKey;
compromised k(Eve,Eve);
compromised k(Eve,Alice);
compromised k(Eve,Bob);
compromised k(Alice,Eve);
compromised k(Bob,Eve);

85
spdl/SPORE/andrew.spdl Normal file
View File

@ -0,0 +1,85 @@
# Andrew Secure RPC
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/andrew.html
#
# Note:
# The shared key between I and R is modelled as k(I,R) currently
# there is no way to express that this key is equal to k(R,I)
# So it is possile that certain attacks that use this property are not found
#
usertype SessionKey;
secret k: Function;
const succ: Function;
const Fresh: Function;
const Compromised: Function;
protocol andrew^KeyCompromise(C)
{
// Read the names of 2 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const ni,nr,nr2: Nonce;
const kir: SessionKey;
var I,R: Agent;
read_C1(C,C, I,R);
send_C2(C,C, (I,{ni}k(I,R)),
{succ(ni),nr}k(I,R),
{succ(nr)}k(I,R),
{kir,nr2}k(I,R),
kir
);
claim_C3(C,Empty, (Compromised,kir));
}
}
protocol andrew(I,R)
{
role I
{
const ni: Nonce;
var nr,nr2: Nonce;
var kir: SessionKey;
send_1(I,R, I,{ni}k(I,R) );
read_2(R,I, {succ(ni),nr}k(I,R) );
send_3(I,R, {succ(nr)}k(I,R) );
read_4(R,I, {kir,nr2}k(I,R) );
claim_I1(I,Secret,kir);
claim_I2(I,Nisynch);
claim_I3(I,Niagree);
claim_I4(I,Empty,(Fresh,kir));
}
role R
{
var ni: Nonce;
const nr,nr2: Nonce;
const kir: SessionKey;
read_1(I,R, I,{ni}k(I,R) );
send_2(R,I, {succ(ni),nr}k(I,R) );
read_3(I,R, {succ(nr)}k(I,R) );
send_4(R,I, {kir,nr2}k(I,R) );
claim_R1(R,Secret,kir);
claim_R2(R,Nisynch);
claim_R3(R,Niagree);
claim_R4(R,Empty,(Fresh,kir));
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;
const kee: SessionKey;
compromised k(Eve,Eve);
compromised k(Eve,Alice);
compromised k(Eve,Bob);
compromised k(Alice,Eve);
compromised k(Bob,Eve);

46
spdl/SPORE/ccitt509-1.spdl Normal file
View File

@ -0,0 +1,46 @@
# CCITT X.509 (1)
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/ccittx509_1.html
#
# Note:
# The attack in SPORE is not found as this is not an attack against
# synchronisation, but an attack against the freshness of Xa and Ya
# which can currently not be modelled in scyther
#
const pk: Function;
secret sk: Function;
inversekeys(pk,sk);
usertype Timestamp;
protocol ccitt509-1(I,R)
{
role I
{
const Ta: Timestamp;
const Na,Xa,Ya: Nonce;
send_1(I,R, I,{Ta, Na, R, Xa,{Ya}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_1(I,R, I,{Ta, Na, R, Xa,{Ya}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);

44
spdl/SPORE/ccitt509-1c.spdl Normal file
View File

@ -0,0 +1,44 @@
# 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 ccitt509-1c(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_1(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);

55
spdl/SPORE/ccitt509-3.spdl Normal file
View File

@ -0,0 +1,55 @@
# CCITT X.509 (3)
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/ccittx509_3.html
#
# Note:
# The protocol description also states that Xa and Ya should be fresh
# this can not be verified using scyther
#
const pk: Function;
secret sk: Function;
inversekeys(pk,sk);
usertype Timestamp;
protocol ccitt509-3(I,R)
{
role I
{
const Ta: Timestamp;
var Tb: Timestamp;
const Na,Xa,Ya: Nonce;
var Xb,Nb,Yb: Nonce;
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_I1(I,Nisynch);
claim_I2(I,Secret,Ya);
claim_I3(I,Secret,Yb);
}
role R
{
var Ta: Timestamp;
const Tb: Timestamp;
var Na,Xa,Ya: Nonce;
const Xb,Yb,Nb: Nonce;
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_R1(R,Nisynch);
claim_R2(R,Secret,Ya);
claim_R3(R,Secret,Yb);
# 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);

49
spdl/SPORE/ccitt509-ban3.spdl Normal file
View File

@ -0,0 +1,49 @@
# BAN modified version of CCITT X.509 (3)
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/ccittx509_3BAN.html
#
# Note:
# The protocol description also states that Xa and Ya should be fresh
# this can not be verified using scyther
#
# Note:
# According to SPORE there are no known attacks on this protocol
#
const pk: Function;
secret sk: Function;
inversekeys(pk,sk);
protocol ccitt509-ban3(I,R)
{
role I
{
const Na,Xa,Ya: Nonce;
var Xb,Nb,Yb: Nonce;
send_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I));
read_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
send_3(I,R, I,{R, Nb}sk(I));
claim_4(I,Nisynch);
}
role R
{
var Na,Xa,Ya: Nonce;
const Xb,Yb,Nb: Nonce;
read_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I));
send_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
read_3(I,R, I,{R, Nb}sk(I));
claim_5(R,Nisynch);
# There should also be Fresh Xa and Fresh Ya claims here
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);

100
spdl/SPORE/denning-sacco-lowe.spdl Normal file
View File

@ -0,0 +1,100 @@
# Lowe modified Denning-Sacco shared key
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/denningSaccoLowe.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
# Note:
# According to SPORE there are no attacks on this protocol, scyther
# finds one however. This has to be investigated further.
usertype Key;
usertype SessionKey;
usertype TimeStamp;
usertype ExpiredTimeStamp;
secret k: Function;
usertype PseudoFunction;
const dec: PseudoFunction;
const Fresh: Function;
const Compromised: Function;
protocol denningSacco-Lowe^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kir: SessionKey;
const T: ExpiredTimeStamp;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, (I,R),
{R,Kir,T,{Kir,I,T}k(R,S)}k(I,S),
{Kir,I,T}k(R,S),
{Nr}Kir,
{{Nr}dec}Kir,
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol denningSacco-Lowe(I,R,S)
{
role I
{
var W: Ticket;
var Kir: SessionKey;
var T: TimeStamp;
var Nr: Nonce;
send_1(I,S, I,R );
read_2(S,I, {R, Kir, T, W}k(I,S) );
send_3(I,R, W);
read_4(R,I, {Nr}Kir);
send_5(I,R, {{Nr}dec}Kir);
claim_I1(I,Niagree);
claim_I2(I,Nisynch);
claim_I3(I,Secret,Kir);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
{
var Kir: SessionKey;
var T: TimeStamp;
const Nr: Nonce;
read_3(I,R, {Kir,I,T}k(R,S));
send_4(R,I, {Nr}Kir);
read_5(I,R, {{Nr}dec}Kir);
claim_R1(R,Niagree);
claim_R2(R,Nisynch);
claim_R3(R,Secret,Kir);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
var W: Ticket;
const Kir: SessionKey;
const T: TimeStamp;
read_1(I,S, I,R );
send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const kee: SessionKey;
const tee: TimeStamp;
compromised k(Eve,Simon);

87
spdl/SPORE/denning-sacco.spdl Normal file
View File

@ -0,0 +1,87 @@
# Denning-Sacco shared key
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/denningSacco.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
usertype Key;
usertype SessionKey;
usertype TimeStamp;
usertype ExpiredTimeStamp;
secret k: Function;
const Fresh: Function;
const Compromised: Function;
protocol denningSacco^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kir: SessionKey;
const T: ExpiredTimeStamp;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, (I,R),
{R,Kir,T,{Kir,I,T}k(R,S)}k(I,S),
{Kir,I,T}k(R,S),
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol denningSacco(I,R,S)
{
role I
{
var W: Ticket;
var Kir: SessionKey;
var T: TimeStamp;
send_1(I,S, I,R );
read_2(S,I, {R, Kir, T, W}k(I,S) );
send_3(I,R, W);
claim_I1(I,Niagree);
claim_I2(I,Nisynch);
claim_I3(I,Secret,Kir);
claim_I4(I,Empty, (Fresh,Kir));
}
role R
{
var Kir: SessionKey;
var T: TimeStamp;
read_3(I,R, {Kir,I,T}k(R,S));
claim_R1(R,Niagree);
claim_R2(R,Nisynch);
claim_R3(R,Secret,Kir);
claim_R4(R,Empty, (Fresh,Kir));
}
role S
{
var W: Ticket;
const Kir: SessionKey;
const T: TimeStamp;
read_1(I,S, I,R );
send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const kee: SessionKey;
const tee: TimeStamp;
compromised k(Eve,Simon);

97
spdl/SPORE/kaochow-v2.spdl Normal file
View File

@ -0,0 +1,97 @@
# Kao Chow Authentication v.2
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/kaoChow2.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
usertype SessionKey;
secret k: Function;
const Fresh: Function;
const Compromised: Function;
protocol kaochow-2^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kir,Kt: SessionKey;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, (I,R,Ni),
{I,R,Ni,Kir,Kt}k(I,S),
{I,R,Ni,Kir,Kt}k(R,S),
R, Nr,
{Nr,Kir}Kt,
Kir
// Kt
);
claim_C3(C,Empty, (Compromised,Kir));
// claim_C4(C,Empty, (Compromised,Kt));
}
}
protocol kaochow-2(I,R,S)
{
role I
{
const ni: Nonce;
var nr: Nonce;
var kir,kt: SessionKey;
send_1 (I,S, I,R,ni);
read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr );
send_4 (I,R, {nr,kir}kt );
claim_I1 (I, Nisynch);
claim_I2 (I, Niagree);
claim_I3 (I, Secret, kir);
claim_I4 (I, Empty, (Fresh,kir));
}
role R
{
var ni: Nonce;
const nr: Nonce;
var kir,kt: SessionKey;
var T: Ticket;
read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) );
send_3 (R,I, R, T, {ni, kir}kt, nr );
read_4 (I,R, {nr,kir}kt );
claim_R1 (R, Nisynch);
claim_R2 (R, Niagree);
claim_R3 (R, Secret, kir);
claim_R4 (R, Empty, (Fresh,kir));
}
role S
{
var ni: Nonce;
const kir, kt: SessionKey;
read_1 (I,S, I,R,ni);
send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) );
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
const te: Ticket;
const ke: SessionKey;
compromised k(Eve,Eve);
compromised k(Eve,Alice);
compromised k(Eve,Bob);
compromised k(Eve,Simon);
compromised k(Alice,Eve);
compromised k(Bob,Eve);
compromised k(Simon,Eve);

104
spdl/SPORE/kaochow-v3.spdl Normal file
View File

@ -0,0 +1,104 @@
# Kao Chow Authentication v.3
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/kaoChow3.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
usertype SessionKey;
usertype ExpiredTimeStamp;
usertype TimeStamp;
secret k: Function;
const Fresh: Function;
const Compromised: Function;
protocol kaochow-3^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kir,Kt: SessionKey;
const T2: ExpiredTimeStamp;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, (I,R,Ni),
{I,R,Ni,Kir,Kt}k(I,S),
{I,R,Ni,Kir,Kt}k(R,S),
{Ni,Kir}Kt,
Nr,
{I,R,T2,Kir}k(R,S),
{Nr,Kir}Kt,
Kir
// Kt
);
claim_C3(C,Empty, (Compromised,Kir));
// claim_C4(C,Empty, (Compromised,Kt));
}
}
protocol kaochow-3(I,R,S)
{
role I
{
const ni: Nonce;
var nr: Nonce;
var kir,kt: SessionKey;
var T2: Ticket;
send_1 (I,S, I,R,ni);
read_3 (R,I, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 );
send_4 (I,R, {nr,kir}kt, T2 );
claim_I1 (I, Nisynch);
claim_I2 (I, Niagree);
claim_I3 (I, Secret, kir);
claim_I4 (I, Empty, (Fresh,kir));
}
role R
{
var ni: Nonce;
const nr: Nonce;
var kir,kt: SessionKey;
var T: Ticket;
const tr: TimeStamp;
read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) );
send_3 (R,I, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) );
read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) );
claim_R1 (R, Nisynch);
claim_R2 (R, Niagree);
claim_R3 (R, Secret, kir);
claim_R4 (R, Empty, (Fresh,kir));
}
role S
{
var ni: Nonce;
const kir, kt: SessionKey;
read_1 (I,S, I,R,ni);
send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) );
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
const te: Ticket;
const ke: SessionKey;
compromised k(Eve,Eve);
compromised k(Eve,Alice);
compromised k(Eve,Bob);
compromised k(Eve,Simon);
compromised k(Alice,Eve);
compromised k(Bob,Eve);
compromised k(Simon,Eve);

95
spdl/SPORE/kaochow.spdl Normal file
View File

@ -0,0 +1,95 @@
# Kao Chow Authentication v.1
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/kaoChow1.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
usertype SessionKey;
secret k: Function;
const Fresh: Function;
const Compromised: Function;
protocol kaochow^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kir: SessionKey;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, (I,R,Ni),
{I,R,Ni,Kir}k(I,S),
{I,R,Ni,Kir}k(R,S),
{Ni}Kir, Nr,
{Nr}Kir,
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol kaochow(I,R,S)
{
role I
{
const ni: Nonce;
var nr: Nonce;
var kir: SessionKey;
send_1 (I,S, I,R,ni);
read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr );
send_4 (I,R, {nr}kir );
claim_I1 (I, Nisynch);
claim_I2 (I, Niagree);
claim_I3 (I, Secret, kir);
claim_I4 (I, Empty, (Fresh,kir));
}
role R
{
var ni: Nonce;
const nr: Nonce;
var kir: SessionKey;
var T;
read_2 (S,R, T, { I,R,ni,kir }k(R,S) );
send_3 (R,I, T, {ni}kir, nr );
read_4 (I,R, {nr}kir );
claim_R1 (R, Nisynch);
claim_R2 (R, Niagree);
claim_R3 (R, Secret, kir);
claim_R4 (R, Empty, (Fresh,kir));
}
role S
{
var ni: Nonce;
const kir: SessionKey;
read_1 (I,S, I,R,ni);
send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) );
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
const te: Ticket;
const ke: SessionKey;
compromised k(Eve,Eve);
compromised k(Eve,Alice);
compromised k(Eve,Bob);
compromised k(Eve,Simon);
compromised k(Alice,Eve);
compromised k(Bob,Eve);
compromised k(Simon,Eve);

88
spdl/SPORE/key-compromise/needham-schroeder-sk.spdl Normal file
View File

@ -0,0 +1,88 @@
# Needham Schroeder Symmetric Key
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/nssk.html
#
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
secret k: Function;
# Model dec that is invertible by inc
const dec,inc: Function;
inversekeys(dec,inc);
usertype SessionKey;
const Fresh: Function;
const Compromised: Function;
protocol needhamschroederSessionKeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kir: SessionKey;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, (I,R,Ni),
{Ni,R,Kir,{Kir,I}k(R,S)}k(I,S),
{Kir,I}k(R,S),
{Nr}Kir,
{{Nr}dec}Kir,
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol needhamschroedersk(I,R,S)
{
role I
{
const Ni: Nonce;
var Nr: Nonce;
var Kir: SessionKey;
var T: Ticket;
send_1(I,S,(I,R,Ni));
read_2(S,I, {Ni,R,Kir,T}k(I,S));
send_3(I,R,T);
read_4(R,I,{Nr}Kir);
send_5(I,R,{{Nr}dec}Kir);
claim_I2(I,Secret,Kir);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
{
const Nr: Nonce;
var Kir: SessionKey;
read_3(I,R,{Kir,I}k(R,S));
send_4(R,I,{Nr}Kir);
read_5(I,R,{{Nr}dec}Kir);
claim_R1(R,Secret,Kir);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
var Ni: Nonce;
const Kir: SessionKey;
read_1(I,S,(I,R,Ni));
send_2(S,I,{Ni,R,Kir,{Kir,I}k(R,S)}k(I,S));
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised k(Eve,Simon);

115
spdl/SPORE/ksl-lowe.spdl Normal file
View File

@ -0,0 +1,115 @@
# Lowe modified KSL
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/kslLowe.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
# Note:
# According to SPORE there are no attacks on this protocol, scyther
# finds one however. This has to be investigated further.
usertype Server, SessionKey, TimeStamp, TicketKey;
usertype ExpiredTimeStamp;
secret k: Function;
const a, b, e: Agent;
const s: Server;
const Fresh: Function;
const Compromised: Function;
const ne: Nonce;
const kee: SessionKey;
untrusted e;
compromised k(e,s);
protocol ksl-Lowe^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr,Nc,Ma,Mb: Nonce;
const Kir: SessionKey;
const Kbb: TicketKey;
const Tr: ExpiredTimeStamp;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, (Ni,I),
(Ni,I,Nr,R),
{I,Nr,Kir}k(R,S),{Ni,R,Kir}k(I,S),
{Tr,I,Kir}Kbb,Nc,{R,Ni}k(I,R),
{Nc}Kir,
Ma,
Mb,{Ma,R}Kir,
{I,Mb}Kir,
Kir,
Kbb
);
claim_C3(C,Empty, (Compromised,Kir));
claim_C4(C,Empty, (Compromised,Kbb));
}
}
protocol ksl-Lowe(I,R,S)
{
role I
{
const Ni, Mi: Nonce;
var Nc, Mr: Nonce;
var T: Ticket;
var Kir: SessionKey;
send_1(I,R, Ni, I);
read_4(R,I, { Ni,R,Kir }k(I,S), T, Nc, {R,Ni}Kir );
send_5(I,R, { Nc }Kir );
send_6(I,R, Mi,T );
read_7(R,I, Mr,{Mi, R}Kir );
send_8(I,R, {I,Mr}Kir );
claim_I1(I,Secret, Kir);
claim_I2(I,Niagree);
claim_I3(I,Nisynch);
claim_I4(I,Empty, (Fresh,Kir));
}
role R
{
var Ni,Mi: Nonce;
const Nr,Nc,Mr: Nonce;
var Kir: SessionKey;
const Kbb: TicketKey;
const Tr: TimeStamp;
var T: Ticket;
read_1(I,R, Ni, I);
send_2(R,S, Ni, I, Nr, R );
read_3(S,R, { I, Nr, Kir }k(R,S), T );
send_4(R,I, T, { Tr, I, Kir }Kbb, Nc, {R, Ni}Kir );
read_5(I,R, { Nc }Kir );
read_6(I,R, Mi,{ Tr, I, Kir }Kbb );
send_7(R,I, Mr,{Mi,R}Kir );
read_8(I,R, {I,Mr}Kir );
claim_R1(R,Secret, Kir);
claim_R2(R,Niagree);
claim_R3(R,Nisynch);
claim_R4(R,Empty, (Fresh,Kir));
}
role S
{
var Ni, Nr: Nonce;
const Kir: SessionKey;
read_2(R,S, Ni, I, Nr, R );
send_3(S,R, { I, Nr, Kir }k(R,S), { Ni,R,Kir }k(I,S) );
}
}

86
spdl/SPORE/ksl.spdl Normal file
View File

@ -0,0 +1,86 @@
# KSL
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/ksl.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
usertype Server, SessionKey, TimeStamp, TicketKey;
usertype ExpiredTimeStamp;
secret k: Function;
const a, b, e: Agent;
const s: Server;
const Fresh: Function;
const Compromised: Function;
const ne: Nonce;
const kee: SessionKey;
untrusted e;
compromised k(e,s);
protocol ksl(I,R,S)
{
role I
{
const Ni, Mi: Nonce;
var Nc, Mr: Nonce;
var T: Ticket;
var Kir: SessionKey;
send_1(I,R, Ni, I);
read_4(R,I, { Ni,R,Kir }k(I,S), T, Nc, {Ni}Kir );
send_5(I,R, { Nc }Kir );
send_6(I,R, Mi,T );
read_7(R,I, Mr,{Mi}Kir );
send_8(I,R, {Mr}Kir );
claim_I1(I,Secret, Kir);
claim_I2(I,Niagree);
claim_I3(I,Nisynch);
claim_I4(I,Empty, (Fresh, Kir));
}
role R
{
var Ni,Mi: Nonce;
const Nr,Nc,Mr: Nonce;
var Kir: SessionKey;
const Kbb: TicketKey;
const Tr: TimeStamp;
var T: Ticket;
read_1(I,R, Ni, I);
send_2(R,S, Ni, I, Nr, R );
read_3(S,R, { Nr, I, Kir }k(R,S), T );
send_4(R,I, T, { Tr, I, Kir }Kbb, Nc, {Ni}Kir );
read_5(I,R, { Nc }Kir );
read_6(I,R, Mi,{ Tr, I, Kir }Kbb );
send_7(R,I, Mr,{Mi}Kir );
read_8(I,R, {Mr}Kir );
claim_R1(R,Secret, Kir);
claim_R2(R,Niagree);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
var Ni, Nr: Nonce;
const Kir: SessionKey;
read_2(R,S, Ni, I, Nr, R );
send_3(S,R, { Nr, I, Kir }k(R,S), { Ni,R,Kir }k(I,S) );
}
}

66
spdl/SPORE/needham-schroeder-lowe.spdl Normal file
View File

@ -0,0 +1,66 @@
# Lowe's fixed version of Needham Schroeder Public Key
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/nspkLowe.html
#
#
# Note:
# The modelling in SPORE includes a server to distribute the public keys
# of the agents, this is not necessary and it allows for attacks against
# synchronisation and agreement, because the keys that the server sends
# out can be replayed.
secret pk: Function; # For some reason SPORE models it such that the agents
# do not know the public keys of the other agents
secret sk: Function;
inversekeys(pk,sk);
protocol needhamschroederpk-Lowe(I,R,S)
{
role I
{
const Ni: Nonce;
var Nr: Nonce;
send_1(I,S, (I,R));
read_2(S,I, {pk(R), R}sk(S));
send_3(I,R,{Ni,I}pk(R));
read_6(R,I, {Ni,Nr,R}pk(I));
send_7(I,R, {Nr}pk(R));
claim_I1(I,Secret,Ni);
claim_I2(I,Secret,Nr);
claim_I3(I,Nisynch);
}
role R
{
const Nr: Nonce;
var Ni: Nonce;
read_3(I,R,{Ni,I}pk(R));
send_4(R,S,(R,I));
read_5(S,R,{pk(I),I}sk(S));
send_6(R,I,{Ni,Nr,R}pk(I));
read_7(I,R,{Nr}pk(R));
claim_R1(R,Secret,Nr);
claim_R2(R,Secret,Ni);
claim_R3(R,Nisynch);
}
role S
{
read_1(I,S,(I,R));
send_2(S,I,{pk(R),R}sk(S));
read_4(R,S,(R,I));
send_5(S,R,{pk(I),I}sk(S));
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);
compromised pk(Eve);
compromised pk(Simon); # Needed because of the way SPORE models nsl

101
spdl/SPORE/needham-schroeder-sk-amend.spdl Normal file
View File

@ -0,0 +1,101 @@
# Amended Needham Schroeder Symmetric Key
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/nssk_amended.html
#
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
# Note:
# According to SPORE there are no attacks on this protocol, scyther
# finds one however. This has to be investigated further.
secret k: Function;
# Model dec that is invertible by inc
const dec,inc: Function;
inversekeys(dec,inc);
usertype SessionKey;
const Fresh: Function;
const Compromised: Function;
protocol needhamschroedersk-amend^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kir: SessionKey;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, I,
{I,Nr}k(R,S),
I,R,Ni,{I,Nr}k(R,S),
{Ni,R,Kir,{Kir,Nr,I}k(R,S)}k(I,S),
{Kir,Nr,I}k(R,S),
{Nr}Kir,
{{Nr}dec}Kir,
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol needhamschroedersk-amend(I,R,S)
{
role I
{
const Ni: Nonce;
var Nr: Nonce;
var Kir: SessionKey;
var T,T2: Ticket;
send_1(I,R,I);
read_2(R,I,T);
send_3(I,S,(I,R,Ni,T));
read_4(S,I, {Ni,R,Kir,T2}k(I,S));
send_5(I,R,T2);
read_6(R,I,{Nr}Kir);
send_7(I,R,{{Nr}dec}Kir);
claim_I2(I,Secret,Kir);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
{
const Nr: Nonce;
var Kir: SessionKey;
read_1(I,R,I);
send_2(R,I,{I,Nr}k(R,S));
read_5(I,R,{Kir,Nr,I}k(R,S));
send_6(R,I,{Nr}Kir);
read_7(I,R,{{Nr}dec}Kir);
claim_R1(R,Secret,Nr);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
var Ni,Nr: Nonce;
const Kir: SessionKey;
read_3(I,S,(I,R,Ni,{I,Nr}k(R,S)));
send_4(S,I,{Ni,R,Kir,{Kir,Nr,I}k(R,S)}k(I,S));
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised k(Eve,Simon);

88
spdl/SPORE/needham-schroeder-sk.spdl Normal file
View File

@ -0,0 +1,88 @@
# Needham Schroeder Symmetric Key
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/nssk.html
#
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
secret k: Function;
# Model dec that is invertible by inc
const dec,inc: Function;
inversekeys(dec,inc);
usertype SessionKey;
const Fresh: Function;
const Compromised: Function;
protocol needhamschroedersk^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kir: SessionKey;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, (I,R,Ni),
{Ni,R,Kir,{Kir,I}k(R,S)}k(I,S),
{Kir,I}k(R,S),
{Nr}Kir,
{{Nr}dec}Kir,
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol needhamschroedersk(I,R,S)
{
role I
{
const Ni: Nonce;
var Nr: Nonce;
var Kir: SessionKey;
var T: Ticket;
send_1(I,S,(I,R,Ni));
read_2(S,I, {Ni,R,Kir,T}k(I,S));
send_3(I,R,T);
read_4(R,I,{Nr}Kir);
send_5(I,R,{{Nr}dec}Kir);
claim_I2(I,Secret,Kir);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
{
const Nr: Nonce;
var Kir: SessionKey;
read_3(I,R,{Kir,I}k(R,S));
send_4(R,I,{Nr}Kir);
read_5(I,R,{{Nr}dec}Kir);
claim_R1(R,Secret,Kir);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
var Ni: Nonce;
const Kir: SessionKey;
read_1(I,S,(I,R,Ni));
send_2(S,I,{Ni,R,Kir,{Kir,I}k(R,S)}k(I,S));
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised k(Eve,Simon);

67
spdl/SPORE/needham-schroeder.spdl Normal file
View File

@ -0,0 +1,67 @@
# Needham Schroeder Public Key
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/nspk.html
#
#
# Note:
# The modelling in SPORE includes a server to distribute the public keys
# of the agents, this is not necessary and it allows for attacks against
# synchronisation and agreement, because the keys that the server sends
# out can be replayed.
secret pk: Function; # For some reason SPORE models it such that the agents
# do not know the public keys of the other agents
secret sk: Function;
inversekeys(pk,sk);
protocol needhamschroederpk(I,R,S)
{
role I
{
const Ni: Nonce;
var Nr: Nonce;
send_1(I,S,(I,R));
read_2(S,I, {pk(R), R}sk(S));
send_3(I,R,{Ni,I}pk(R));
read_6(R,I, {Ni, Nr}pk(I));
send_7(I,R, {Nr}pk(R));
claim_I1(I,Secret,Ni);
claim_I2(I,Secret,Nr);
claim_I3(I,Nisynch);
}
role R
{
const Nr: Nonce;
var Ni: Nonce;
read_3(I,R,{Ni,I}pk(R));
send_4(R,S,(R,I));
read_5(S,R,{pk(I),I}sk(S));
send_6(R,I,{Ni,Nr}pk(I));
read_7(I,R,{Nr}pk(R));
claim_R1(R,Secret,Nr);
claim_R2(R,Secret,Ni);
claim_R3(R,Nisynch);
}
role S
{
read_1(I,S,(I,R));
send_2(S,I,{pk(R),R}sk(S));
read_4(R,S,(R,I));
send_5(S,R,{pk(I),I}sk(S));
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);
compromised pk(Eve);
compromised pk(Simon); # Needed because SPORE only assumes agents know their
# own public key and that of the server

116
spdl/SPORE/neumannstub-guttman-hwang.spdl Normal file
View File

@ -0,0 +1,116 @@
# Neumann Stubblebine
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
# Note:
# In SPORE this protocol is not described correctly, there are in fact 2
# different protocols (the key establishment protocol and the repeated
# authentication protocol)
usertype Server, SessionKey, TimeStamp, TicketKey;
usertype ExpiredTimeStamp;
secret k: Function;
const Alice, Bob, Simon, Eve: Agent;
const Fresh: Function;
const Compromised: Function;
const ne: Nonce;
const kee: SessionKey;
untrusted Eve;
compromised k(Eve,Simon);
protocol neustub-GuttmanHwang^Repeat(I,R,S)
{
const Kir: SessionKey;
role I
{
const Mi: Nonce;
var Mr: Nonce;
const Kir: SessionKey;
const Tr: TimeStamp;
send_5(I,R,Mi,{I,Kir,Tr}k(R,S));
read_6(R,I,{Mi,Mr}Kir);
send_7(I,R,{I,Mr}Kir);
claim_I1(I,Secret, Kir);
claim_I2(I,Niagree);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
{
const Mr: Nonce;
var Tr: TimeStamp;
var Kir: SessionKey;
var Mi: Nonce;
read_5(I,R,Mi,{I,Kir,Tr}k(R,S));
send_6(R,I,{Mi,Mr}Kir);
read_7(I,R,{I,Mr}Kir);
claim_R1(R,Secret, Kir);
claim_R2(R,Niagree);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
}
}
protocol neustub-GuttmanHwang(I,R,S)
{
role I
{
const Ni: Nonce;
var Nr: Nonce;
var T: Ticket;
var Tb: TimeStamp;
var Kir: SessionKey;
send_1(I,R, I, Ni);
read_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
send_!4(I,R,T,{Nr}Kir);
claim_I1(I,Secret, Kir);
claim_I2(I,Niagree);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
{
var Ni,Mi: Nonce;
const Nr,Mr: Nonce;
var Kir: SessionKey;
const Tb: TimeStamp;
var T: Ticket;
read_1(I,R, I, Ni);
send_!2(R,S, R, {I, Ni, Tb ,Nr}k(R,S));
read_!4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
claim_R1(R,Secret, Kir);
claim_R2(R,Niagree);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
var Ni, Nr: Nonce;
const Kir: SessionKey;
var Tb: TimeStamp;
read_!2(R,S, R, {I,Ni,Tb,Nr}k(R,S));
send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
}
}

116
spdl/SPORE/neumannstub-guttman.spdl Normal file
View File

@ -0,0 +1,116 @@
# Neumann Stubblebine
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
# Note:
# In SPORE this protocol is not described correctly, there are in fact 2
# different protocols (the key establishment protocol and the repeated
# authentication protocol)
usertype Server, SessionKey, TimeStamp, TicketKey;
usertype ExpiredTimeStamp;
secret k: Function;
const Alice, Bob, Simon, Eve: Agent;
const Fresh: Function;
const Compromised: Function;
const ne: Nonce;
const kee: SessionKey;
untrusted Eve;
compromised k(Eve,Simon);
protocol neustub^Repeat(I,R,S)
{
const Kir: SessionKey;
role I
{
const Mi: Nonce;
var Mr: Nonce;
const Kir: SessionKey;
const Tr: TimeStamp;
send_5(I,R,Mi,{I,Kir,Tr}k(R,S));
read_6(R,I,{Mi,Mr}Kir);
send_7(I,R,{I,Mr}Kir);
claim_I1(I,Secret, Kir);
claim_I2(I,Niagree);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
{
const Mr: Nonce;
var Tr: TimeStamp;
var Kir: SessionKey;
var Mi: Nonce;
read_5(I,R,Mi,{I,Kir,Tr}k(R,S));
send_6(R,I,{Mi,Mr}Kir);
read_7(I,R,{I,Mr}Kir);
claim_R1(R,Secret, Kir);
claim_R2(R,Niagree);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
}
}
protocol neustub(I,R,S)
{
role I
{
const Ni: Nonce;
var Nr: Nonce;
var T: Ticket;
var Tb: TimeStamp;
var Kir: SessionKey;
send_1(I,R, I, Ni);
read_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
send_4(I,R,T,{Nr}Kir);
claim_I1(I,Secret, Kir);
claim_I2(I,Niagree);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
{
var Ni,Mi: Nonce;
const Nr,Mr: Nonce;
var Kir: SessionKey;
const Tb: TimeStamp;
var T: Ticket;
read_1(I,R, I, Ni);
send_!2(R,S, R, {I, Ni, Tb}k(R,S),Nr);
read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
claim_R1(R,Secret, Kir);
claim_R2(R,Niagree);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
var Ni, Nr: Nonce;
const Kir: SessionKey;
var Tb: TimeStamp;
read_!2(R,S, R, {I,Ni,Tb}k(R,S), Nr);
send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
}
}

108
spdl/SPORE/neumannstub-hwang.spdl Normal file
View File

@ -0,0 +1,108 @@
# Hwang modified Neumann Stubblebine
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebineHwang.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
# Note:
# According to SPORE there are no attacks on this protocol, scyther
# finds one however. This has to be investigated further.
usertype Server, SessionKey, TimeStamp, TicketKey;
usertype ExpiredTimeStamp;
secret k: Function;
const a, b, e: Agent;
const s: Server;
const Fresh: Function;
const Compromised: Function;
const ne: Nonce;
const kee: SessionKey;
untrusted e;
compromised k(e,s);
protocol neustub-Hwang^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr,Mi,Mr: Nonce;
const Kir: SessionKey;
const Tr: ExpiredTimeStamp;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, I,Ni,
R,{I,Ni,Tr,Nr}k(R,S),
{R,Ni,Kir,Tr}k(I,S),
{I,Kir,Tr}k(R,S), Nr,
{Nr}Kir,
Mi,{I,Kir,Tr}k(R,S),
Mr,{Mi}Kir,
{Mr}Kir,
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol neustub-Hwang(I,R,S)
{
role I
{
const Ni,Mi: Nonce;
var Nr,Mr: Nonce;
var T: Ticket;
var Tb: TimeStamp;
var Kir: SessionKey;
send_1(I,R, I, Ni);
read_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
send_4(I,R,T,{Nr}Kir);
send_5(I,R,Mi,T);
read_6(R,I,Mr,{Mi}Kir);
send_7(I,R,{Mr}Kir);
claim_I1(I,Secret, Kir);
claim_I2(I,Niagree);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
{
var Ni,Mi: Nonce;
const Nr,Mr: Nonce;
var Kir: SessionKey;
const Tb: TimeStamp;
var T: Ticket;
read_1(I,R, I, Ni);
send_!2(R,S, R, {I, Ni, Tb, Nr}k(R,S));
read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
read_5(I,R,Mi,T);
send_6(R,I,Mr,{Mi}Kir);
read_7(I,R,{Mr}Kir);
claim_R1(R,Secret, Kir);
claim_R2(R,Niagree);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
var Ni, Nr: Nonce;
const Kir: SessionKey;
var Tb: TimeStamp;
read_!2(R,S, R, {I,Ni,Tb,Nr}k(R,S));
send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
}
}

141
spdl/SPORE/neumannstub-keycompromise.spdl Normal file
View File

@ -0,0 +1,141 @@
# Neumann Stubblebine
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
# Note:
# In SPORE this protocol is not described correctly, there are in fact 2
# different protocols (the key establishment protocol and the repeated
# authentication protocol)
usertype Server, SessionKey, TimeStamp, TicketKey;
usertype ExpiredTimeStamp;
secret k: Function;
const Alice, Bob, Simon, Eve: Agent;
const Fresh: Function;
const Compromised: Function;
const ne: Nonce;
const kee: SessionKey;
untrusted Eve;
compromised k(Eve,Simon);
protocol neustub^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr,Mi,Mr: Nonce;
const Kir: SessionKey;
const Tr: ExpiredTimeStamp;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, I,Ni,
R,{I,Ni,Tr}k(R,S),Nr,
{R,Ni,Kir,Tr}k(I,S),
{I,Kir,Tr}k(R,S), Nr,
{Nr}Kir,
Mi,{I,Kir,Tr}k(R,S),
Mr,{Mi}Kir,
{Mr}Kir,
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol neustub^Repeat(I,R,S)
{
const Kir: SessionKey;
role I
{
const Mi: Nonce;
var Mr: Nonce;
const Kir: SessionKey;
const Tr: TimeStamp;
send_5(I,R,Mi,{I,Kir,Tr}k(R,S));
read_6(R,I,Mr,{Mi}Kir);
send_7(I,R,{Mr}Kir);
claim_I1(I,Secret, Kir);
claim_I2(I,Niagree);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
{
const Mr: Nonce;
var Tr: TimeStamp;
var Kir: SessionKey;
var Mi: Nonce;
read_5(I,R,Mi,{I,Kir,Tr}k(R,S));
send_6(R,I,Mr,{Mi}Kir);
read_7(I,R,{Mr}Kir);
claim_R1(R,Secret, Kir);
claim_R2(R,Niagree);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
}
}
protocol neustub(I,R,S)
{
role I
{
const Ni: Nonce;
var Nr: Nonce;
var T: Ticket;
var Tb: TimeStamp;
var Kir: SessionKey;
send_1(I,R, I, Ni);
read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
send_4(I,R,T,{Nr}Kir);
claim_I1(I,Secret, Kir);
claim_I2(I,Niagree);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
{
var Ni,Mi: Nonce;
const Nr,Mr: Nonce;
var Kir: SessionKey;
const Tb: TimeStamp;
var T: Ticket;
read_1(I,R, I, Ni);
send_2(R,S, R, {I, Ni, Tb}k(R,S),Nr);
read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
claim_R1(R,Secret, Kir);
claim_R2(R,Niagree);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
var Ni, Nr: Nonce;
const Kir: SessionKey;
var Tb: TimeStamp;
read_2(R,S, R, {I,Ni,Tb}k(R,S), Nr);
send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
}
}

116
spdl/SPORE/neumannstub.spdl Normal file
View File

@ -0,0 +1,116 @@
# Neumann Stubblebine
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
# Note:
# In SPORE this protocol is not described correctly, there are in fact 2
# different protocols (the key establishment protocol and the repeated
# authentication protocol)
usertype Server, SessionKey, TimeStamp, TicketKey;
usertype ExpiredTimeStamp;
secret k: Function;
const Alice, Bob, Simon, Eve: Agent;
const Fresh: Function;
const Compromised: Function;
const ne: Nonce;
const kee: SessionKey;
untrusted Eve;
compromised k(Eve,Simon);
protocol neustub^Repeat(I,R,S)
{
const Kir: SessionKey;
role I
{
const Mi: Nonce;
var Mr: Nonce;
const Kir: SessionKey;
const Tr: TimeStamp;
send_5(I,R,Mi,{I,Kir,Tr}k(R,S));
read_6(R,I,Mr,{Mi}Kir);
send_7(I,R,{Mr}Kir);
claim_I1(I,Secret, Kir);
claim_I2(I,Niagree);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
{
const Mr: Nonce;
var Tr: TimeStamp;
var Kir: SessionKey;
var Mi: Nonce;
read_5(I,R,Mi,{I,Kir,Tr}k(R,S));
send_6(R,I,Mr,{Mi}Kir);
read_7(I,R,{Mr}Kir);
claim_R1(R,Secret, Kir);
claim_R2(R,Niagree);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
}
}
protocol neustub(I,R,S)
{
role I
{
const Ni: Nonce;
var Nr: Nonce;
var T: Ticket;
var Tb: TimeStamp;
var Kir: SessionKey;
send_1(I,R, I, Ni);
read_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
send_4(I,R,T,{Nr}Kir);
claim_I1(I,Secret, Kir);
claim_I2(I,Niagree);
claim_I3(I,Nisynch);
claim_I4(I,Empty,(Fresh,Kir));
}
role R
{
var Ni,Mi: Nonce;
const Nr,Mr: Nonce;
var Kir: SessionKey;
const Tb: TimeStamp;
var T: Ticket;
read_1(I,R, I, Ni);
send_!2(R,S, R, {I, Ni, Tb}k(R,S),Nr);
read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
claim_R1(R,Secret, Kir);
claim_R2(R,Niagree);
claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir));
}
role S
{
var Ni, Nr: Nonce;
const Kir: SessionKey;
var Tb: TimeStamp;
read_!2(R,S, R, {I,Ni,Tb}k(R,S), Nr);
send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
}
}

87
spdl/SPORE/otwayrees.spdl Normal file
View File

@ -0,0 +1,87 @@
# Otway Rees
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/otwayRees.html
#
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
secret const k : Function;
const Fresh: Function;
const Compromised: Function;
usertype String,SessionKey;
protocol otwayRees^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const M: String;
const Kir: SessionKey;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, M,I,R,{Ni,M,I,R}k(I,S),
{Nr,M,I,R}k(R,S),
{Ni,Kir}k(I,S), {Nr,Kir}k(R,S),
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol otwayrees(I,R,S)
{
role I
{
const Ni : Nonce;
const M : String;
var Kir : SessionKey;
send_1(I,R, M,I,R,{Ni,M,I,R}k(I,S) );
read_4(R,I, M,{Ni,Kir}k(I,S) );
claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch);
claim_I3(I, Empty, (Fresh,Kir));
}
role R
{
var M : String;
const Nr : Nonce;
var Kir : SessionKey;
var T1,T2: Ticket;
read_1(I,R, M,I,R, T1 );
send_2(R,S, M,I,R, T1, { Nr,M,I,R }k(R,S) );
read_3(S,R, M, T2, { Nr,Kir }k(R,S) );
send_4(R,I, M, T2 );
claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch);
claim_R3(R, Empty, (Fresh,Kir));
}
role S
{
var Ni,Nr : Nonce;
var M : String;
const Kir : SessionKey;
read_2(R,S, M,I,R, { Ni,M,I,R}k(I,S), { Nr,M,I,R }k(R,S) );
send_3(S,R, M, { Ni,Kir }k(I,S) , { Nr,Kir }k(R,S) );
}
}
const Alice, Bob, Eve, Simon: Agent;
untrusted Eve;
compromised k(Eve,Simon);

58
spdl/SPORE/smartright.spdl Normal file
View File

@ -0,0 +1,58 @@
# SmartRight view-only
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/smartright_viewonly.html
#
# Note:
# According to SPORE there are no known attacks on this protocol
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
# Note:
# Scyther finds an attack because the value of VoR in te last message can
# be replaced with an arbitrary value
const hash: Function;
secret unhash: Function;
secret k: Function;
inversekeys (hash,unhash);
usertype SessionKey;
usertype XorKey;
const Vor: XorKey;
protocol smartright(I,R)
{
role I
{
const VoKey: SessionKey;
const VoR: XorKey;
const CW;
var VoRi: Nonce;
send_1(I,R, {VoKey,{CW}VoR}k(I,R));
read_2(R,I, VoRi);
send_3(I,R, VoR, {{VoRi}hash}VoKey);
}
role R
{
var T: Ticket;
var VoR: XorKey;
var VoKey: SessionKey;
const VoRi: Nonce;
read_1(I,R, {VoKey,T}k(I,R));
send_2(R,I, VoRi);
read_3(I,R, VoR,{{VoRi}hash}VoKey);
claim_R1(R,Nisynch);
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;

75
spdl/SPORE/splice-as-cj.spdl Normal file
View File

@ -0,0 +1,75 @@
# Clark and Jacob modified Hwang and Chen modified SPLICE/AS
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/spliceas3.html
#
# Note:
# The assumptions made here do not comply with those in SPORE
# SPORE assumes that the agents do not know the pk function, but only
# their own public key values.
# This can currently not be modelled.
usertype TimeStamp, LifeTime;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
const inc,dec: Function;
inversekeys (inc,dec);
protocol spliceAS-CJ(I,R,S)
{
role I
{
const N1,N2: Nonce;
const T: TimeStamp;
const L: LifeTime;
send_1(I,S, I, R, N1 );
read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
send_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) );
read_6(R,I, R, I, {{N2}inc}pk(I) );
claim_7(I, Secret, N2);
claim_9(I, Niagree);
claim_10(I, Nisynch);
}
role S
{
var N1,N3: Nonce;
read_1(I,S, I, R, N1 );
send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
read_4(R,S, R, I, N3 );
send_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
}
role R
{
const N3: Nonce;
var N2: Nonce;
var T: TimeStamp;
var L: LifeTime;
var ni: Nonce;
const nr: Nonce;
read_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) );
send_4(R,S, R, I, N3 );
read_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
send_6(R,I, R, I, {{N2}inc}pk(I) );
claim_8(R, Secret, N2);
claim_11(R, Niagree);
claim_12(R, Nisynch);
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);

72
spdl/SPORE/splice-as-hc.spdl Normal file
View File

@ -0,0 +1,72 @@
# Hwang and Chen Modified SPLICE/AS
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/spliceas2.html
#
usertype TimeStamp, LifeTime;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
const inc,dec: Function;
inversekeys (inc,dec);
protocol spliceAS-HC(I,R,S)
{
role I
{
const N1,N2: Nonce;
const T: TimeStamp;
const L: LifeTime;
send_1(I,S, I, R, N1 );
read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
read_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_7(I, Secret, N2);
claim_9(I, Niagree);
claim_10(I, Nisynch);
}
role S
{
var N1,N3: Nonce;
read_1(I,S, I, R, N1 );
send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
read_4(R,S, R, I, N3 );
send_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) );
}
role R
{
const N3: Nonce;
var N2: Nonce;
var T: TimeStamp;
var L: LifeTime;
var ni: Nonce;
const nr: Nonce;
read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
send_4(R,S, R, I, N3 );
read_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) );
send_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_8(R, Secret, N2);
claim_11(R, Niagree);
claim_12(R, Nisynch);
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);

75
spdl/SPORE/splice-as.spdl Normal file
View File

@ -0,0 +1,75 @@
# SPLICE/AS
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/spliceas.html
#
# Note:
# The assumptions made here do not comply with those in SPORE
# SPORE assumes that the agents do not know the pk function, but only
# their own public key values.
# This can currently not be modelled.
usertype TimeStamp, LifeTime;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
const inc,dec: Function;
inversekeys (inc,dec);
protocol spliceAS(I,R,S)
{
role I
{
const N1,N2: Nonce;
const T: TimeStamp;
const L: LifeTime;
send_1(I,S, I, R, N1 );
read_2(S,I, S, {S, I, N1, pk(R)}sk(S) );
send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
read_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_7(I, Secret, N2);
claim_9(I, Niagree);
claim_10(I, Nisynch);
}
role S
{
var N1,N3: Nonce;
read_1(I,S, I, R, N1 );
send_2(S,I, S, {S, I, N1, pk(R)}sk(S) );
read_4(R,S, R, I, N3 );
send_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
}
role R
{
const N3: Nonce;
var N2: Nonce;
var T: TimeStamp;
var L: LifeTime;
var ni: Nonce;
const nr: Nonce;
read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
send_4(R,S, R, I, N3 );
read_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
send_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_8(R, Secret, N2);
claim_11(R, Niagree);
claim_12(R, Nisynch);
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);

82
spdl/SPORE/tmn.spdl Normal file
View File

@ -0,0 +1,82 @@
# TMN
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/tmn.html
#
# Note:
# According to Boyd and Mathuria Kb is the session key this is not clear
# from the description in SPORE
usertype SessionKey;
const pk: Function;
secret sk: Function;
inversekeys(pk,sk);
const Fresh: Function;
const Compromised: Function;
protocol tmn^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kr,Ki: SessionKey;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, R,{Ki}pk(S),
I, {Kr}pk(S),
{Kr}Ki,
Kr
);
claim_C3(C,Empty, (Compromised,Kr));
}
}
protocol tmn(I,R,S)
{
role I
{
const Ki: SessionKey;
var Kr: SessionKey;
send_1(I,S, R,{Ki}pk(S) );
read_4(S,I, R,{Kr}Ki );
claim_I1(I,Secret,Kr);
claim_I2(I,Nisynch);
claim_I3(I,Empty,(Fresh,Kr));
}
role R
{
const Kr: SessionKey;
read_2(S,R, I );
send_3(R,S, I, { Kr }pk(S) );
claim_R1(R,Secret,Kr);
claim_R2(R,Nisynch);
claim_R3(R,Empty,(Fresh,Kr));
}
role S
{
var Ki,Kr: SessionKey;
read_1(I,S, R,{Ki}pk(S) );
send_2(S,R, I );
read_3(R,S, I, { Kr }pk(S) );
send_4(S,I, R,{Kr}Ki );
}
}
const Alice,Bob,Eve,Simon: Agent;
const Ke: SessionKey;
untrusted Eve;
compromised sk(Eve);

96
spdl/SPORE/wmf-lowe.spdl Normal file
View File

@ -0,0 +1,96 @@
# Lowe modified Wide Mouthed Frog
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/wideMouthedFrogLowe.html
#
# Note:
# According to SPORE there are no known attacks on this protocol, scyther
# finds one however this has to do with the unusual assumption that every
# agent can recognise and will reject to read messages that it has created
# itself.
usertype SessionKey;
usertype TimeStamp;
usertype ExpiredTimeStamp;
const succ,pred: Function;
inversekeys (succ,pred);
const Fresh: Function;
const Compromised: Function;
secret k: Function;
protocol wmf-Lowe^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kir: SessionKey;
const Ti,Ts: ExpiredTimeStamp;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, I, {I,Ti,R,Kir}k(I,S),
{S,Ts,I,Kir}k(R,S),
{R,Nr}Kir,
{I,{Nr}succ}Kir,
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol wmf-Lowe(I,R,S)
{
role I
{
const Kir: SessionKey;
const Ti: TimeStamp;
var Kr: SessionKey;
var Nr: Nonce;
send_1(I,S, I, {Ti, R, Kir}k(I,S));
read_3(R,I,{Nr}Kir);
send_4(I,R,{{Nr}succ}Kir);
claim_I1(I,Secret,Kir);
claim_I2(I,Nisynch);
claim_I3(I,Empty,(Fresh,Kir));
}
role R
{
var Ts: TimeStamp;
var Kir: SessionKey;
const Nr: Nonce;
read_2(S,R, {Ts, I, Kir}k(R,S) );
send_3(R,I, {Nr}Kir);
read_4(I,R, {{Nr}succ}Kir);
claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch);
claim_R3(R,Empty,(Fresh,Kir));
}
role S
{
var Kir: SessionKey;
const Ts: TimeStamp;
var Ti: TimeStamp;
read_1(I,S, I,{Ti, R, Kir}k(I,S) );
send_2(S,R, {Ts, I, Kir}k(R,S));
}
}
const Alice,Bob,Eve,Simon: Agent;
const Ke: SessionKey;
const Te: TimeStamp;
untrusted Eve;
compromised k(Eve,Simon);

84
spdl/SPORE/wmf.spdl Normal file
View File

@ -0,0 +1,84 @@
# Wide Mouthed Frog
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/wideMouthedFrog.html
#
# Note
# The name of the party that has generated a message was added in order
# to model the property described in SPORE that an agent can identify
# its own messages and will reject them.
usertype SessionKey;
usertype TimeStamp;
usertype ExpiredTimeStamp;
secret k: Function;
const Fresh: Function;
const Compromised: Function;
protocol wmf^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kir: SessionKey;
const Ti,Ts: ExpiredTimeStamp;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, I, {I,Ti,R,Kir}k(I,S),
{S,Ts,I,Kir}k(R,S),
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol wmf(I,R,S)
{
role I
{
const Kir: SessionKey;
const Ti: TimeStamp;
var Kr: SessionKey;
send_1(I,S, I, {I, Ti, R, Kir}k(I,S));
claim_I1(I,Secret,Kir);
claim_I2(I,Empty,(Fresh,Kir));
}
role R
{
var Ts: TimeStamp;
var Kir: SessionKey;
read_2(S,R, {S, Ts, I, Kir}k(R,S) );
claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch);
claim_R3(R,Empty,(Fresh,Kir));
}
role S
{
var Kir: SessionKey;
const Ts: TimeStamp;
var Ti: TimeStamp;
read_1(I,S, I,{I, Ti, R, Kir}k(I,S) );
send_2(S,R, {S, Ts, I, Kir}k(R,S));
}
}
const Alice,Bob,Eve,Simon: Agent;
const Ke: SessionKey;
const Te: TimeStamp;
untrusted Eve;
compromised k(Eve,Simon);

57
spdl/SPORE/woo-lam-pi-1.spdl Normal file
View File

@ -0,0 +1,57 @@
# Woo and Lam Pi 1
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/wooLamPi1.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
secret k: Function;
protocol woolamPi-1(I,R,S)
{
role I
{
var Nr: Nonce;
send_1(I,R, I);
read_2(R,I, Nr);
send_3(I,R, {I,R,Nr}k(I,S));
}
role R
{
const Nr: Nonce;
var T: Ticket;
read_1(I,R, I);
send_2(R,I, Nr);
read_3(I,R, T);
send_4(R,S, {I,R, T}k(R,S));
read_5(S,R, {I,R, Nr}k(R,S));
claim_R1(R,Nisynch);
}
role S
{
var Nr: Nonce;
read_4(R,S, {I,R, {I,R,Nr}k(I,S)}k(R,S));
send_5(S,R, {I,R,Nr}k(R,S));
}
}
const Alice,Bob,Eve,Simon: Agent;
const Te: Ticket;
const Ne: Nonce;
untrusted Eve;
compromised k(Eve,Simon);

57
spdl/SPORE/woo-lam-pi-2.spdl Normal file
View File

@ -0,0 +1,57 @@
# Woo and Lam Pi 2
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/wooLamPi2.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
secret k: Function;
protocol woolamPi-2(I,R,S)
{
role I
{
var Nr: Nonce;
send_1(I,R, I);
read_2(R,I, Nr);
send_3(I,R, {I,Nr}k(I,S));
}
role R
{
const Nr: Nonce;
var T: Ticket;
read_1(I,R, I);
send_2(R,I, Nr);
read_3(I,R, T);
send_4(R,S, {I, T}k(R,S));
read_5(S,R, {I, Nr}k(R,S));
claim_R1(R,Nisynch);
}
role S
{
var Nr: Nonce;
read_4(R,S, {I, {I,Nr}k(I,S)}k(R,S));
send_5(S,R, {I,Nr}k(R,S));
}
}
const Alice,Bob,Eve,Simon: Agent;
const Te: Ticket;
const Ne: Nonce;
untrusted Eve;
compromised k(Eve,Simon);

57
spdl/SPORE/woo-lam-pi-3.spdl Normal file
View File

@ -0,0 +1,57 @@
# Woo and Lam Pi 2
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/wooLamPi3.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
secret k: Function;
protocol woolamPi-3(I,R,S)
{
role I
{
var Nr: Nonce;
send_1(I,R, I);
read_2(R,I, Nr);
send_3(I,R, {Nr}k(I,S));
}
role R
{
const Nr: Nonce;
var T: Ticket;
read_1(I,R, I);
send_2(R,I, Nr);
read_3(I,R, T);
send_4(R,S, {I, T}k(R,S));
read_5(S,R, {I, Nr}k(R,S));
claim_R1(R,Nisynch);
}
role S
{
var Nr: Nonce;
read_4(R,S, {I, {Nr}k(I,S)}k(R,S));
send_5(S,R, {I,Nr}k(R,S));
}
}
const Alice,Bob,Eve,Simon: Agent;
const Te: Ticket;
const Ne: Nonce;
untrusted Eve;
compromised k(Eve,Simon);

55
spdl/SPORE/woo-lam-pi-f.spdl Normal file
View File

@ -0,0 +1,55 @@
# Woo and Lam Pi f
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/wooLamPif.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
secret k: Function;
protocol woolamPi-f(I,R,S)
{
role I
{
var Nr: Nonce;
send_1(I,R, I);
read_2(R,I, Nr);
send_3(I,R, {I,R,Nr}k(I,S));
}
role R
{
const Nr: Nonce;
var T: Ticket;
read_1(I,R, I);
send_2(R,I, Nr);
read_3(I,R, T);
send_4(R,S, {I, R, Nr, T}k(R,S));
read_5(S,R, {I, R, Nr}k(R,S));
claim_R1(R,Nisynch);
}
role S
{
var Nr: Nonce;
read_4(R,S, {I, R, Nr,{I,R,Nr}k(I,S)}k(R,S));
send_5(S,R, {I, R, Nr}k(R,S));
}
}
const Alice,Bob,Eve,Simon: Agent;
const Te: Ticket;
const Ne: Nonce;
untrusted Eve;
compromised k(Eve,Simon);

61
spdl/SPORE/woo-lam-pi.spdl Normal file
View File

@ -0,0 +1,61 @@
# Woo and Lam Pi
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/wooLamPi.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
# Note:
# Scyther finds an attack that appears to be legit, but is not present in
# SPORE.
#
secret k: Function;
protocol woolamPi(I,R,S)
{
role I
{
var Nr: Nonce;
send_1(I,R, I);
read_2(R,I, Nr);
send_3(I,R, {Nr}k(I,S));
}
role R
{
const Nr: Nonce;
var T: Ticket;
read_1(I,R, I);
send_2(R,I, Nr);
read_3(I,R, T);
send_4(R,S, {I, T}k(R,S));
read_5(S,R, {Nr}k(R,S));
claim_R1(R,Nisynch);
}
role S
{
var Nr: Nonce;
read_4(R,S, {I,{Nr}k(I,S)}k(R,S));
send_5(S,R, {Nr}k(R,S));
}
}
const Alice,Bob,Eve,Simon: Agent;
const Te: Ticket;
const Ne: Nonce;
untrusted Eve;
compromised k(Eve,Simon);

102
spdl/SPORE/woo-lam.spdl Normal file
View File

@ -0,0 +1,102 @@
# Woo and Lam Mutual Authentication
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/wooLamMutual.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
usertype SessionKey;
secret k: Function;
const Fresh: Function;
const Compromised: Function;
protocol woolam^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const N1,N2: Nonce;
const Kir: SessionKey;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, I,N1,
R,N2,
{I,R,N1,N2}k(I,S),
{I,R,N1,N2}k(R,S),
{R,N1,N2,Kir}k(I,S),
{I,N1,N2,Kir}k(R,S),
{N1,N2}Kir,
{N2}Kir,
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol woolam(I,R,S)
{
role I
{
const N1: Nonce;
var Kir: SessionKey;
var N2: Nonce;
send_1(I,R, I, N1);
read_2(R,I, R, N2);
send_3(I,R, {I, R, N1, N2}k(I,S));
read_6(R,I, {R, N1, N2, Kir}k(I,S), {N1,N2}Kir);
send_7(I,R, {N2}Kir);
claim_I1(I,Secret,Kir);
claim_I2(I,Nisynch);
claim_I3(I,Empty,(Fresh,Kir));
}
role R
{
const N2: Nonce;
var N1: Nonce;
var Kir: SessionKey;
var T1,T2: Ticket;
read_1(I,R, I, N1);
send_2(R,I, R, N2);
read_3(I,R, T1);
send_4(R,S, T1, {I, R, N1, N2}k(R,S));
read_5(S,R, T2, {I, N1, N2, Kir}k(R,S));
send_6(R,I, T2, {N1,N2}Kir);
read_7(I,R, {N2}Kir);
claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch);
claim_R3(R,Empty,(Fresh,Kir));
}
role S
{
const Kir: SessionKey;
var N1,N2: Nonce;
read_4(R,S, {I, R, N1, N2}k(I,S), {I, R, N1, N2}k(R,S));
send_5(S,R, {R, N1, N2, Kir}k(I,S), {I, N1, N2, Kir}k(R,S));
}
}
const Alice,Bob,Eve,Simon: Agent;
const Ke: SessionKey;
const Te: Ticket;
const Ne: Nonce;
untrusted Eve;
compromised k(Eve,Simon);

85
spdl/SPORE/yahalom-ban.spdl Normal file
View File

@ -0,0 +1,85 @@
# BAN simplified version of Yahalom
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/yahalomBAN.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
secret k : Function;
usertype SessionKey;
const Fresh: Function;
const Compromised: Function;
protocol yahalom-BAN^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kir: SessionKey;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, I,Ni,
R,Nr,{I,Ni}k(R,S),
Nr,{R,Kir,Ni}k(I,S),
{I,Kir,Nr}k(R,S),
{Nr}Kir,
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol yahalom-BAN(I,R,S)
{
role I
{
const Ni: Nonce;
var Nr: Nonce;
var T: Ticket;
var Kir: SessionKey;
send_1(I,R, I,Ni);
read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T );
send_4(I,R, T, {Nr}Kir );
claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch);
claim_I3(I, Empty, (Fresh,Kir));
}
role R
{
const Nr: Nonce;
var Ni: Nonce;
var T: Ticket;
var Kir: SessionKey;
read_1(I,R, I,Ni);
send_2(R,S, R, Nr, {I,Ni}k(R,S) );
read_4(I,R, {I,Kir,Nr}k(R,S) , {Nr}Kir );
claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch);
claim_R3(R, Empty, (Fresh,Kir));
}
role S
{
const Kir: SessionKey;
var Ni,Nr: Nonce;
read_2(R,S, R, Nr, {I,Ni}k(R,S) );
send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,Kir,Nr}k(R,S) );
}
}
const Alice,Bob,Charlie,David: Agent;

56
spdl/SPORE/yahalom-lowe.spdl Normal file
View File

@ -0,0 +1,56 @@
# Lowe's modified version of Yahalom
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/yahalomLowe.html
#
#
secret k : Function;
usertype SessionKey;
protocol yahalom-Lowe(I,R,S)
{
role I
{
const Ni: Nonce;
var Nr: Nonce;
var Kir: SessionKey;
send_1(I,R, I,Ni);
read_3(S,I, {R,Kir,Ni,Nr}k(I,S) );
send_5(I,R, {I, R, S, Nr}Kir );
claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch);
}
role R
{
const Nr: Nonce;
var Ni: Nonce;
var Kir: SessionKey;
read_1(I,R, I,Ni);
send_2(R,S, {I,Ni,Nr}k(R,S) );
read_4(S,R, {I,Kir}k(R,S));
read_5(I,R, {I, R, S, Nr}Kir);
claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch);
}
role S
{
const Kir: SessionKey;
var Ni,Nr: Nonce;
read_2(R,S, {I,Ni,Nr}k(R,S) );
send_3(S,I, {R,Kir,Ni,Nr}k(I,S));
send_4(S,R, {I,Kir}k(R,S));
}
}
const Alice,Bob,Simon : Agent;

84
spdl/SPORE/yahalom-paulson.spdl Normal file
View File

@ -0,0 +1,84 @@
# Paulson's strengthened version of Yahalom
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/yahalomPaulson.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
secret k : Function;
const Fresh: Function;
const Compromised: Function;
usertype SessionKey;
protocol yahalom-Paulson^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kir: SessionKey;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, I,Ni,
R,Nr,{I,Ni}k(R,S),
Nr,{R,Kir,Ni}k(I,S),
{I,R,Kir,Nr}k(R,S),
{Nr}Kir,
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol yahalom-Paulson(I,R,S)
{
role I
{
const Ni: Nonce;
var Nr: Nonce;
var T: Ticket;
var Kir: SessionKey;
send_1(I,R, I,Ni);
read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T );
send_4(I,R, T, {Nr}Kir );
claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch);
claim_I3(I, Empty, (Fresh,Kir));
}
role R
{
const Nr: Nonce;
var Ni: Nonce;
var T: Ticket;
var Kir: SessionKey;
read_1(I,R, I,Ni);
send_2(R,S, R, Nr, {I,Ni}k(R,S) );
read_4(I,R, {I,R, Kir, Nr}k(R,S) , {Nr}Kir );
claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch);
claim_R3(R, Empty, (Fresh,Kir));
}
role S
{
const Kir: SessionKey;
var Ni,Nr: Nonce;
read_2(R,S, R, Nr, {I,Ni}k(R,S) );
send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,R,Kir,Nr}k(R,S) );
}
}
const Alice,Bob,Simon : Agent;

84
spdl/SPORE/yahalom.spdl Normal file
View File

@ -0,0 +1,84 @@
# Yahalom
#
# Modelled after the description in the SPORE library
# http://www.lsv.ens-cachan.fr/spore/yahalom.html
#
# Note:
# This protocol uses a ticket so scyther will only be able to verify
# the protocol using the ARACHNE engine (-a)
#
secret k : Function;
usertype SessionKey;
const Fresh: Function;
const Compromised: Function;
protocol yahalom^KeyCompromise(C)
{
// Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise
role C {
const Ni,Nr: Nonce;
const Kir: SessionKey;
var I,R,S: Agent;
read_C1(C,C, I,R,S);
send_C2(C,C, I,Ni,
R,{I,Ni,Nr}k(R,S),
{R,Kir,Ni,Nr}k(I,S),
{I,Kir}k(R,S),
{Nr}Kir,
Kir
);
claim_C3(C,Empty, (Compromised,Kir));
}
}
protocol yahalom(I,R,S)
{
role I
{
const Ni: Nonce;
var Nr: Nonce;
var T: Ticket;
var Kir: SessionKey;
send_1(I,R, I,Ni);
read_3(S,I, {R,Kir,Ni,Nr}k(I,S), T );
send_4(I,R, T, {Nr}Kir );
claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch);
claim_I3(I, Empty, (Fresh,Kir));
}
role R
{
const Nr: Nonce;
var Ni: Nonce;
var T: Ticket;
var Kir: SessionKey;
read_1(I,R, I,Ni);
send_2(R,S, R, {I,Ni,Nr}k(R,S) );
read_4(I,R, {I,Kir}k(R,S) , {Nr}Kir );
claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch);
claim_R3(R, Empty, (Fresh,Kir));
}
role S
{
const Kir: SessionKey;
var Ni,Nr: Nonce;
read_2(R,S, R, {I,Ni,Nr}k(R,S) );
send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) );
}
}
const Alice,Bob,Simon : Agent;