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

- Remove spdl subdirectory: it is now part of the ecss repository.

Browse Source
This commit is contained in:
ccremers 2005-12-22 10:52:11 +00:00
parent 34484a28f9
commit 44e8771de8
113 changed files with 0 additions and 8712 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
spdl/SPORE/NotModelled.txt
View File

@ -1,23 +0,0 @@
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.

105
spdl/SPORE/andrew-ban-concrete.spdl
View File

@ -1,105 +0,0 @@
# 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;
# This scenario should find the attack in SPORE
# run andrewConcrete.I(Alice,Bob);
# run andrewConcrete.R(Bob,Alice);
# This is the original scenario
run andrew-Concrete.I(Agent,Agent);
run andrew-Concrete.R(Agent,Agent);
run andrew-Concrete.I(Agent,Agent);
run andrew-Concrete.R(Agent,Agent);

90
spdl/SPORE/andrew-ban.spdl
View File

@ -1,90 +0,0 @@
# 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);
run andrew-Ban.I(Agent,Agent);
run andrew-Ban.R(Agent,Agent);
run andrew-Ban.I(Agent,Agent);
run andrew-Ban.R(Agent,Agent);

95
spdl/SPORE/andrew-lowe-ban.spdl
View File

@ -1,95 +0,0 @@
# 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);
run andrew-LoweBan.I(Agent,Agent);
run andrew-LoweBan.R(Agent,Agent);
run andrew-LoweBan.I(Agent,Agent);
run andrew-LoweBan.R(Agent,Agent);

98
spdl/SPORE/andrew.spdl
View File

@ -1,98 +0,0 @@
# 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);
# This scenario should recreate the first attack in SPORE when running
# scyther in model checker mode
#run andrew.I(Alice,Bob);
#run andrew.R(Alice,Bob);
#run andrew.I(Alice,Bob);
#run andrew.R(Alice,Bob);
# General scenario, 2 parallel runs of the protocol
run andrew.I(Agent,Agent);
run andrew.R(Agent,Agent);
run andrew.I(Agent,Agent);
run andrew.R(Agent,Agent);

51
spdl/SPORE/ccitt509-1.spdl
View File

@ -1,51 +0,0 @@
# 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);
# General scenario, 2 parallel runs of the protocol
run ccitt509-1.I(Agent,Agent);
run ccitt509-1.R(Agent,Agent);
run ccitt509-1.I(Agent,Agent);
run ccitt509-1.R(Agent,Agent);

50
spdl/SPORE/ccitt509-1c.spdl
View File

@ -1,50 +0,0 @@
# 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);
# General scenario, 2 parallel runs of the protocol
run ccitt509-1c.I(Agent,Agent);
run ccitt509-1c.R(Agent,Agent);
run ccitt509-1c.I(Agent,Agent);
run ccitt509-1c.R(Agent,Agent);

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

@ -1,66 +0,0 @@
# 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);
# This scenario should find the attack described in SPORE
# run ccitt5093.I(Alice,Bob);
# run ccitt5093.I(Alice,Eve);
# run ccitt5093.R(Alice,Bob);
# General scenario, 2 parallel runs of the protocol
run ccitt509-3.I(Agent,Agent);
run ccitt509-3.R(Agent,Agent);
run ccitt509-3.I(Agent,Agent);
run ccitt509-3.R(Agent,Agent);

55
spdl/SPORE/ccitt509-ban3.spdl
View File

@ -1,55 +0,0 @@
# 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);
# General scenario, 2 parallel runs of the protocol
run ccitt509-ban3.I(Agent,Agent);
run ccitt509-ban3.R(Agent,Agent);
run ccitt509-ban3.I(Agent,Agent);
run ccitt509-ban3.R(Agent,Agent);

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

@ -1,110 +0,0 @@
# 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);
# General scenario, 2 parallel runs of the protocol
# Note because the modelchecker does not support tickets this might not
# be very useful
run denningSacco-Lowe.I(Agent,Agent,Simon);
run denningSacco-Lowe.R(Agent,Agent,Simon);
run denningSacco-Lowe.S(Agent,Agent,Simon);
run denningSacco-Lowe.I(Agent,Agent,Simon);
run denningSacco-Lowe.R(Agent,Agent,Simon);
run denningSacco-Lowe.S(Agent,Agent,Simon);

97
spdl/SPORE/denning-sacco.spdl
View File

@ -1,97 +0,0 @@
# 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);
# General scenario, 2 parallel runs of the protocol
# Note because the modelchecker does not support tickets this might not
# be very useful
run denningSacco.I(Agent,Agent,Simon);
run denningSacco.R(Agent,Agent,Simon);
run denningSacco.S(Agent,Agent,Simon);
run denningSacco.I(Agent,Agent,Simon);
run denningSacco.R(Agent,Agent,Simon);
run denningSacco.S(Agent,Agent,Simon);

103
spdl/SPORE/kaochow-v2.spdl
View File

@ -1,103 +0,0 @@
# 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);
run kaochow-2.I(Agent,Agent,Simon);
run kaochow-2.R(Agent,Agent,Simon);
run kaochow-2.S(Agent,Agent,Simon);
run kaochow-2.I(Agent,Agent,Simon);
run kaochow-2.R(Agent,Agent,Simon);
run kaochow-2.S(Agent,Agent,Simon);

110
spdl/SPORE/kaochow-v3.spdl
View File

@ -1,110 +0,0 @@
# 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);
run kaochow-3.I(Agent,Agent,Simon);
run kaochow-3.R(Agent,Agent,Simon);
run kaochow-3.S(Agent,Agent,Simon);
run kaochow-3.I(Agent,Agent,Simon);
run kaochow-3.R(Agent,Agent,Simon);
run kaochow-3.S(Agent,Agent,Simon);

101
spdl/SPORE/kaochow.spdl
View File

@ -1,101 +0,0 @@
# 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);
run kaochow.I(Agent,Agent,Simon);
run kaochow.R(Agent,Agent,Simon);
run kaochow.S(Agent,Agent,Simon);
run kaochow.I(Agent,Agent,Simon);
run kaochow.R(Agent,Agent,Simon);
run kaochow.S(Agent,Agent,Simon);

96
spdl/SPORE/key-compromise/needham-schroeder-sk.spdl
View File

@ -1,96 +0,0 @@
# 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);
# General scenario, 2 parallel runs of the protocol
run needhamschroedersk.I(Agent,Agent,Simon);
run needhamschroedersk.R(Agent,Agent,Simon);
run needhamschroedersk.S(Agent,Agent,Simon);
run needhamschroedersk.I(Agent,Agent,Simon);
run needhamschroedersk.R(Agent,Agent,Simon);
run needhamschroedersk.S(Agent,Agent,Simon);

118
spdl/SPORE/ksl-lowe.spdl
View File

@ -1,118 +0,0 @@
# 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) );
}
}
run ksl-Lowe.I(a,b,s);
run ksl-Lowe.R(a,b,s);
run ksl-Lowe.S(a,b,s);

116
spdl/SPORE/ksl.spdl
View File

@ -1,116 +0,0 @@
# 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^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),
{Nr,I,Kir}k(R,S),{Ni,R,Kir}k(I,S),
{Tr,I,Kir}Kbb,Nc,{Ni}k(I,R),
{Nc}Kir,
Ma,
Mb,{Ma}Kir,
{Mb}Kir,
Kir,
Kbb
);
claim_C3(C,Empty, (Compromised,Kir));
claim_C4(C,Empty, (Compromised,Kbb));
}
}
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) );
}
}
run ksl.I(a,b,s);
run ksl.R(a,b,s);
run ksl.S(a,b,s);

74
spdl/SPORE/needham-schroeder-lowe.spdl
View File

@ -1,74 +0,0 @@
# 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
# General scenario, 2 parallel runs of the protocol
run needhamschroederpk-Lowe.I(Agent,Agent,Simon);
run needhamschroederpk-Lowe.S(Agent,Agent,Simon);
run needhamschroederpk-Lowe.R(Agent,Agent,Simon);
run needhamschroederpk-Lowe.I(Agent,Agent,Simon);
run needhamschroederpk-Lowe.R(Agent,Agent,Simon);
run needhamschroederpk-Lowe.S(Agent,Agent,Simon);

108
spdl/SPORE/needham-schroeder-sk-amend.spdl
View File

@ -1,108 +0,0 @@
# 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);
# General scenario, 2 parallel runs of the protocol
run needhamschroedersk-amend.I(Agent,Agent,Simon);
run needhamschroedersk-amend.R(Agent,Agent,Simon);
run needhamschroedersk-amend.S(Agent,Agent,Simon);
run needhamschroedersk-amend.I(Agent,Agent,Simon);
run needhamschroedersk-amend.R(Agent,Agent,Simon);
run needhamschroedersk-amend.S(Agent,Agent,Simon);

96
spdl/SPORE/needham-schroeder-sk.spdl
View File

@ -1,96 +0,0 @@
# 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);
# General scenario, 2 parallel runs of the protocol
run needhamschroedersk.I(Agent,Agent,Simon);
run needhamschroedersk.R(Agent,Agent,Simon);
run needhamschroedersk.S(Agent,Agent,Simon);
run needhamschroedersk.I(Agent,Agent,Simon);
run needhamschroedersk.R(Agent,Agent,Simon);
run needhamschroedersk.S(Agent,Agent,Simon);

75
spdl/SPORE/needham-schroeder.spdl
View File

@ -1,75 +0,0 @@
# 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
# General scenario, 2 parallel runs of the protocol
run needhamschroederpk.I(Agent,Agent,Simon);
run needhamschroederpk.R(Agent,Agent,Simon);
run needhamschroederpk.S(Agent,Agent,Simon);
run needhamschroederpk.I(Agent,Agent,Simon);
run needhamschroederpk.R(Agent,Agent,Simon);
run needhamschroederpk.S(Agent,Agent,Simon);

112
spdl/SPORE/neumannstub-hwang.spdl
View File

@ -1,112 +0,0 @@
# 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,{Mr}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,{Mr}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,{Mr}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 );
}
}
run neustub-Hwang.A(a,b,s);
run neustub-Hwang.B(a,b,s);
run neustub-Hwang.S(a,b,s);

145
spdl/SPORE/neumannstub.spdl
View File

@ -1,145 +0,0 @@
# 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 );
}
}
run neustub.I(Alice,Bob,Simon);
run neustub.R(Alice,Bob,Simon);
run neustub.S(Alice,Bob,Simon);

95
spdl/SPORE/otwayrees.spdl
View File

@ -1,95 +0,0 @@
# 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);
run otwayrees.A(Alice, Agent, Simon);
run otwayrees.B(Agent, Bob, Simon);
run otwayrees.S(Agent, Agent, Simon);
run otwayrees.A(Agent, Agent, Simon);
run otwayrees.B(Agent, Agent, Simon);
run otwayrees.S(Agent, Agent, Simon);

64
spdl/SPORE/smartright.spdl
View File

@ -1,64 +0,0 @@
# 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;
# General scenario, 2 parallel runs of the protocol
run smartright.I(Agent,Agent);
run smartright.R(Agent,Agent);
run smartright.I(Agent,Agent);
run smartright.R(Agent,Agent);

83
spdl/SPORE/splice-as-cj.spdl
View File

@ -1,83 +0,0 @@
# 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);
run spliceAS-CJ.I(Agent,Agent,Agent);
run spliceAS-CJ.R(Agent,Agent,Agent);
run spliceAS-CJ.S(Agent,Agent,Agent);
#run spliceASCJ.I(Alice,Bob,Simon);
#run spliceASCJ.R(Alice,Bob,Simon);
#run spliceASCJ.S(Alice,Bob,Simon);

79
spdl/SPORE/splice-as-hc.spdl
View File

@ -1,79 +0,0 @@
# 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);
#run spliceASHC.I(Alice,Bob,Simon);
#run spliceASHC.R(Alice,Bob,Simon);
#run spliceASHC.S(Alice,Bob,Simon);
run spliceAS-HC.I(Agent,Agent,Agent);
run spliceAS-HC.R(Agent,Agent,Agent);
run spliceAS-HC.S(Agent,Agent,Agent);

83
spdl/SPORE/splice-as.spdl
View File

@ -1,83 +0,0 @@
# 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);
run spliceAS.I(Agent,Agent,Agent);
run spliceAS.R(Agent,Agent,Agent);
run spliceAS.S(Agent,Agent,Agent);
#run spliceAS.I(Alice,Bob,Simon);
#run spliceAS.R(Alice,Bob,Simon);
#run spliceAS.S(Alice,Bob,Simon);

91
spdl/SPORE/tmn.spdl
View File

@ -1,91 +0,0 @@
# 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);
# Scenario to recreate an attack in SPORE
#run tmn.I (Alice,Bob,Simon);
#run tmn.R (Alice,Bob,Simon);
#run tmn.S (Alice,Bob,Simon);
run tmn.I (Agent,Agent,Simon);
run tmn.R (Agent,Agent,Simon);
run tmn.S (Agent,Agent,Simon);

100
spdl/SPORE/wmf-lowe.spdl
View File

@ -1,100 +0,0 @@
# 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);
run wmf-Lowe.I (Agent,Agent,Simon);
run wmf-Lowe.R (Agent,Agent,Simon);
run wmf-Lowe.S (Agent,Agent,Simon);

88
spdl/SPORE/wmf.spdl
View File

@ -1,88 +0,0 @@
# 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);
run wmf.I (Agent,Agent,Simon);
run wmf.R (Agent,Agent,Simon);
run wmf.S (Agent,Agent,Simon);

61
spdl/SPORE/woo-lam-pi-1.spdl
View File

@ -1,61 +0,0 @@
# 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);
run woolamPi-1.I (Agent,Agent,Simon);
run woolamPi-1.R (Agent,Agent,Simon);
run woolamPi-1.S (Agent,Agent,Simon);

61
spdl/SPORE/woo-lam-pi-2.spdl
View File

@ -1,61 +0,0 @@
# 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);
run woolamPi-2.I (Agent,Agent,Simon);
run woolamPi-2.R (Agent,Agent,Simon);
run woolamPi-2.S (Agent,Agent,Simon);

61
spdl/SPORE/woo-lam-pi-3.spdl
View File

@ -1,61 +0,0 @@
# 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);
run woolamPi-3.I (Agent,Agent,Simon);
run woolamPi-3.R (Agent,Agent,Simon);
run woolamPi-3.S (Agent,Agent,Simon);

59
spdl/SPORE/woo-lam-pi-f.spdl
View File

@ -1,59 +0,0 @@
# 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);
run woolamPi-f.I (Agent,Agent,Simon);
run woolamPi-f.R (Agent,Agent,Simon);
run woolamPi-f.S (Agent,Agent,Simon);

65
spdl/SPORE/woo-lam-pi.spdl
View File

@ -1,65 +0,0 @@
# 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);
run woolamPi.I (Agent,Agent,Simon);
run woolamPi.R (Agent,Agent,Simon);
run woolamPi.S (Agent,Agent,Simon);

106
spdl/SPORE/woo-lam.spdl
View File

@ -1,106 +0,0 @@
# 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);
run woolam.I (Agent,Agent,Simon);
run woolam.R (Agent,Agent,Simon);
run woolam.S (Agent,Agent,Simon);

89
spdl/SPORE/yahalom-ban.spdl
View File

@ -1,89 +0,0 @@
# 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,Simon : Agent;
run yahalom-BAN.I(Agent,Agent,s);
run yahalom-BAN.I(Agent,Agent,s);
run yahalom-BAN.R(Agent,Agent,s);

60
spdl/SPORE/yahalom-lowe.spdl
View File

@ -1,60 +0,0 @@
# 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;
run yahalom-Lowe.I(Agent,Agent,s);
run yahalom-Lowe.I(Agent,Agent,s);
run yahalom-Lowe.R(Agent,Agent,s);

88
spdl/SPORE/yahalom-paulson.spdl
View File

@ -1,88 +0,0 @@
# 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;
run yahalom-Paulson.I(Agent,Agent,s);
run yahalom-Paulson.I(Agent,Agent,s);
run yahalom-Paulson.R(Agent,Agent,s);

88
spdl/SPORE/yahalom.spdl
View File

@ -1,88 +0,0 @@
# 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;
run yahalom.I(Agent,Agent,s);
run yahalom.I(Agent,Agent,s);
run yahalom.R(Agent,Agent,s);

52
spdl/demo/ns3.spdl
View File

@ -1,52 +0,0 @@
/*
* Needham-Schroeder protocol
*/
// PKI infrastructure
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
// The protocol description
protocol ns3(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
send_1(I,R, {I,ni}pk(R) );
read_2(R,I, {ni,nr}pk(I) );
send_3(I,R, {nr}pk(R) );
claim_i1(I,Secret,ni);
claim_i2(I,Secret,nr);
claim_i3(I,Niagree);
claim_i4(I,Nisynch);
}
role R
{
var ni: Nonce;
const nr: Nonce;
read_1(I,R, {I,ni}pk(R) );
send_2(R,I, {ni,nr}pk(I) );
read_3(I,R, {nr}pk(R) );
claim_r1(R,Secret,ni);
claim_r2(R,Secret,nr);
claim_r3(R,Niagree);
claim_r4(R,Nisynch);
}
}
// An untrusted agent, with leaked information
const Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);

52
spdl/demo/nsl3.spdl
View File

@ -1,52 +0,0 @@
/*
* Needham-Schroeder-Lowe protocol
*/
// PKI infrastructure
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
// The protocol description
protocol nsl3(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
send_1(I,R, {I,ni}pk(R) );
read_2(R,I, {ni,nr,R}pk(I) );
send_3(I,R, {nr}pk(R) );
claim_i1(I,Secret,ni);
claim_i2(I,Secret,nr);
claim_i3(I,Niagree);
claim_i4(I,Nisynch);
}
role R
{
var ni: Nonce;
const nr: Nonce;
read_1(I,R, {I,ni}pk(R) );
send_2(R,I, {ni,nr,R}pk(I) );
read_3(I,R, {nr}pk(R) );
claim_r1(R,Secret,ni);
claim_r2(R,Secret,nr);
claim_r3(R,Niagree);
claim_r4(R,Nisynch);
}
}
// An untrusted agent, with leaked information
const Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);

53
spdl/misc/andrew-ban.spdl
View File

@ -1,53 +0,0 @@
usertype SessionKey;
secret k: Function;
protocol andrewBan(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_5(I,Nisynch);
claim_5b(I,Niagree);
claim_6(I,Secret, kir);
claim_7(I,Secret, k(I,R));
}
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_8(R,Nisynch);
claim_8b(R,Niagree);
claim_9(R,Secret, kir);
claim_10(R,Secret, k(I,R));
}
}
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);
run andrewBan.I(Agent,Agent);
run andrewBan.R(Agent,Agent);
run andrewBan.I(Agent,Agent);
run andrewBan.R(Agent,Agent);

53
spdl/misc/andrew-lowe-ban.spdl
View File

@ -1,53 +0,0 @@
usertype SessionKey;
secret k: Function;
protocol andrewLoweBan(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,I}k(I,R) );
send_3(I,R, {ni}kir );
read_4(R,I, nr );
claim_5(I,Nisynch);
claim_5b(I,Niagree);
claim_6(I,Secret, kir);
claim_7(I,Secret, k(I,R));
}
role R
{
var ni: Nonce;
const nr: Nonce;
const kir: SessionKey;
read_1(I,R, I,ni );
send_2(R,I, {ni,kir,I}k(I,R) );
read_3(I,R, {ni}kir );
send_4(R,I, nr );
claim_8(R,Nisynch);
claim_8b(R,Niagree);
claim_9(R,Secret, kir);
claim_10(R,Secret, k(I,R));
}
}
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);
run andrewLoweBan.I(Agent,Agent);
run andrewLoweBan.R(Agent,Agent);
run andrewLoweBan.I(Agent,Agent);
run andrewLoweBan.R(Agent,Agent);

48
spdl/misc/bke-broken.spdl
View File

@ -1,48 +0,0 @@
/*
Bilateral Key Exchange with Public Key protocol (bkebroken)
Broken version with man in the middle attack.
*/
usertype Key;
const pk,h: Function;
secret sk,hinv: Function;
inversekeys (pk,sk);
inversekeys (h,hinv);
protocol bkebroken(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
var kir: Key;
send_1 (I,R, { ni,I }pk(R) );
read_2 (R,I, { h(ni),nr,kir }pk(I) );
send_3 (I,R, { h(nr),kir }pk(R) );
claim_4 (I, Secret, kir );
}
role R
{
var ni: Nonce;
const nr: Nonce;
const kir: Key;
read_1 (I,R, { ni,I }pk(R) );
send_2 (R,I, { h(ni),nr,kir }pk(I) );
read_3 (I,R, { h(nr),kir }pk(R) );
claim_5 (R, Secret, kir );
}
}
const a,b,e: Agent;
untrusted e;
compromised sk(e);
const ne: Nonce;
run bkebroken.I(a,Agent);
run bkebroken.R(Agent,b);

104
spdl/misc/bke-generalized-4.spdl
View File

@ -1,104 +0,0 @@
/*
* Generalized Bilateral Key Exchange protocol.
* Four-party version.
*
* Specific order of interleaving in message 1-4 is required to (a)
* avoid type flaws whilst (b) retaining BKE structure for the simple
* case.
*
* Cas Cremers
* Mon May 23 15:15:37 CEST 2005
*/
const zero;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol bkegen4(R1,R2,R3,R4)
{
role R1
{
const n1: Nonce;
var n2,n3,n4: Nonce;
send_1(R1,R2, {n1,R1,R3,R4}pk(R2) );
read_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) );
send_5(R1,R2, {n2,n3}n4 );
claim_r1a(R1,Secret,n1);
claim_r1b(R1,Secret,n2);
claim_r1c(R1,Secret,n3);
claim_r1d(R1,Secret,n4);
claim_r1A(R1,Niagree);
claim_r1S(R1,Nisynch);
}
role R2
{
const n2: Nonce;
var n1,n3,n4: Nonce;
read_1(R1,R2, {n1,R1,R3,R4}pk(R2) );
send_2(R2,R3, {n1,R1,n2,R2,R4}pk(R3) );
read_5(R1,R2, {n2,n3}n4 );
send_6(R2,R3, {n3}n4 );
claim_r2a(R2,Secret,n1);
claim_r2b(R2,Secret,n2);
claim_r2c(R2,Secret,n3);
claim_r2d(R2,Secret,n4);
claim_r2A(R2,Niagree);
claim_r2S(R2,Nisynch);
}
role R3
{
const n3: Nonce;
var n1,n2,n4: Nonce;
read_2(R2,R3, {n1,R1,n2,R2,R4}pk(R3) );
send_3(R3,R4, {n1,R1,n2,R2,n3,R3}pk(R4) );
read_6(R2,R3, {n3}n4 );
send_7(R3,R4, {zero}n4 );
claim_r3a(R3,Secret,n1);
claim_r3b(R3,Secret,n2);
claim_r3c(R3,Secret,n3);
claim_r3d(R3,Secret,n4);
claim_r3A(R3,Niagree);
claim_r3S(R3,Nisynch);
}
role R4
{
const n4: Nonce;
var n1,n2,n3: Nonce;
read_3(R3,R4, {n1,R1,n2,R2,n3,R3}pk(R4) );
send_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) );
read_7(R3,R4, {zero}n4 );
claim_r4a(R4,Secret,n1);
claim_r4b(R4,Secret,n2);
claim_r4c(R4,Secret,n3);
claim_r4d(R4,Secret,n4);
claim_r4A(R4,Niagree);
claim_r4S(R4,Nisynch);
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);
run bkegen4.R1(Agent,Agent,Agent,Agent);
run bkegen4.R2(Agent,Agent,Agent,Agent);
run bkegen4.R3(Agent,Agent,Agent,Agent);
run bkegen4.R4(Agent,Agent,Agent,Agent);

58
spdl/misc/bke-one.spdl
View File

@ -1,58 +0,0 @@
/*
Bilateral Key Exchange with Public Key protocol (bkeONE)
*/
usertype Key;
const pk,hash: Function;
secret sk,unhash: Function;
inversekeys (pk,sk);
inversekeys (hash,unhash);
protocol bkeONE(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
var kir: Key;
send_1 (I,R, { ni,I }pk(R) );
read_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
send_3 (I,R, { hash(nr) }kir );
claim_4 (I, Secret, kir );
}
role R
{
var ni: Nonce;
const nr: Nonce;
const kir: Key;
read_1 (I,R, { ni,I }pk(R) );
send_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
read_3 (I,R, { hash(nr) }kir );
claim_5 (R, Secret, kir );
}
}
const a,e: Agent;
untrusted e;
compromised sk(e);
const ne: Nonce;
run bkeONE.I(a,Agent);
run bkeONE.R(Agent,a);
run bkeONE.I(a,Agent);
run bkeONE.R(Agent,a);
run bkeONE.I(a,Agent);
run bkeONE.R(Agent,a);
run bkeONE.I(a,Agent);
run bkeONE.R(Agent,a);
run bkeONE.I(a,Agent);
run bkeONE.R(Agent,a);

55
spdl/misc/bke-variation.spdl
View File

@ -1,55 +0,0 @@
/*
Bilateral Key Exchange with Public Key protocol (BKEPK)
Variation for exercise 2r890
*/
usertype Key;
const pk,hash: Function;
secret sk,unhash: Function;
inversekeys (pk,sk);
inversekeys (hash,unhash);
protocol bkevariation(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
var kir: Key;
send_1 (I,R, { ni,I }pk(R) );
read_2 (R,I, { hash(ni),nr,kir }pk(I) );
send_3 (I,R, { hash(nr) }kir );
claim_4 (I, Secret, kir );
claim_5 (I, Niagree );
claim_6 (I, Nisynch );
}
role R
{
var ni: Nonce;
const nr: Nonce;
const kir: Key;
read_1 (I,R, { ni,I }pk(R) );
send_2 (R,I, { hash(ni),nr,kir }pk(I) );
read_3 (I,R, { hash(nr) }kir );
claim_7 (R, Secret, kir );
claim_8 (R, Niagree );
claim_9 (R, Nisynch );
}
}
const a,b,e: Agent;
untrusted e;
compromised sk(e);
const ne: Nonce;
run bkevariation.I(a,Agent);
run bkevariation.R(Agent,b);
run bkevariation.I(a,Agent);
run bkevariation.R(Agent,b);

62
spdl/misc/bke.spdl
View File

@ -1,62 +0,0 @@
/*
Bilateral Key Exchange with Public Key protocol (BKEPK)
*/
usertype Key;
const pk,hash: Function;
secret sk,unhash: Function;
inversekeys (pk,sk);
inversekeys (hash,unhash);
protocol bke(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
var kir: Key;
send_1 (I,R, { ni,I }pk(R) );
read_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
send_3 (I,R, { hash(nr) }kir );
claim_4 (I, Secret, kir );
claim_5 (I, Niagree );
claim_6 (I, Nisynch );
}
role R
{
var ni: Nonce;
const nr: Nonce;
const kir: Key;
read_1 (I,R, { ni,I }pk(R) );
send_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
read_3 (I,R, { hash(nr) }kir );
claim_7 (R, Secret, kir );
claim_8 (R, Niagree );
claim_9 (R, Nisynch );
}
}
const a,b,e: Agent;
untrusted e;
compromised sk(e);
const ne: Nonce;
run bke.I(a,Agent);
run bke.R(Agent,b);
run bke.I(a,Agent);
run bke.R(Agent,b);
run bke.I(a,Agent);
run bke.R(Agent,b);
run bke.I(a,Agent);
run bke.R(Agent,b);
run bke.I(a,Agent);
run bke.R(Agent,b);

61
spdl/misc/bkepk-ce.spdl
View File

@ -1,61 +0,0 @@
/*
Bilateral Key Exchange with Public Key protocol (bkeCE)
Version from Corin/Etalle: An Improved Constraint-Based System for the Verification of Security Protocols.
Tried to stay as close as possible to compare timing results.
*/
usertype Key;
const pk,hash: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol bkeCE(A,B,testnonce)
{
role B
{
const nb: Nonce;
var na: Nonce;
var kab: Key;
send_1 (B,A, B,{ nb,B }pk(A) );
read_2 (A,B, { hash(nb),na,A,kab }pk(B) );
send_3 (B,A, { hash(na) }kab );
}
role A
{
var nb: Nonce;
const na: Nonce;
const kab: Key;
read_1 (B,A, B,{ nb,B }pk(A) );
send_2 (A,B, { hash(nb),na,A,kab }pk(B) );
read_3 (B,A, { hash(na) }kab );
}
role testnonce
{
var n: Nonce;
read_4 (testnonce,testnonce, n);
}
}
const Alice,Bob,Eve;
compromised sk(Eve);
untrusted Eve;
run bkeCE.A(Alice,Bob,Alice);
run bkeCE.A(Alice,Bob,Alice);
run bkeCE.B(Alice,Bob,Alice);
run bkeCE.B(Alice,Bob,Alice);
run bkeCE.testnonce(Alice,Bob,Alice);
run bkeCE.testnonce(Alice,Bob,Alice);
run bkeCE.A(Alice,Bob,Alice);
run bkeCE.testnonce(Alice,Bob,Alice);

62
spdl/misc/bkepk-ce2.spdl
View File

@ -1,62 +0,0 @@
/*
Bilateral Key Exchange with Public Key protocol (bkepkCE2)
Version from Corin/Etalle: An Improved Constraint-Based System for the Verification of Security Protocols.
Tried to stay as close as possible to compare timing results.
*/
usertype Key;
const pk,hash: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol bkepkCE2(A,B,testnonce)
{
role B
{
const nb: Nonce;
var na: Nonce;
var kab: Key;
send_1 (B,A, B,{ nb,B }pk(A) );
read_2 (A,B, { hash(nb),na,A,kab }pk(B) );
send_3 (B,A, { hash(na) }kab );
}
role A
{
var nb: Nonce;
const na: Nonce;
const kab: Key;
read_1 (B,A, B,{ nb,B }pk(A) );
send_2 (A,B, { hash(nb),na,A,kab }pk(B) );
read_3 (B,A, { hash(na) }kab );
}
role testnonce
{
var n: Nonce;
read_4 (testnonce,testnonce, n);
}
}
const Alice,Bob,Eve;
compromised sk(Eve);
untrusted Eve;
run bkepkCE2.A(Alice,Bob,Alice);
run bkepkCE2.A(Alice,Bob,Alice);
run bkepkCE2.A(Alice,Bob,Alice);
run bkepkCE2.B(Alice,Bob,Alice);
run bkepkCE2.B(Alice,Bob,Alice);
run bkepkCE2.B(Alice,Bob,Alice);
run bkepkCE2.testnonce(Alice,Bob,Alice);
run bkepkCE2.testnonce(Alice,Bob,Alice);
run bkepkCE2.testnonce(Alice,Bob,Alice);

55
spdl/misc/boyd-nsl-fix.spdl
View File

@ -1,55 +0,0 @@
/*
* Boyd fix for NS(L)
*
* From the paper "Towards Extensional Goals in Authentication
* Protocols"
*
* Broken. Best shown by attack id 4.
*/
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
const hash: Function;
secret unhash: Function;
inversekeys (hash,unhash);
protocol boydNS(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
send_1(I,R, {ni}pk(R),I );
read_2(R,I, {nr}pk(I),hash(ni,R) );
send_3(I,R, hash(nr, I,R) );
claim_i1(I,Secret,ni);
claim_i2(I,Secret,nr);
claim_i3(I,Niagree);
claim_i4(I,Nisynch);
}
role R
{
var ni: Nonce;
const nr: Nonce;
read_1(I,R, {ni}pk(R),I );
send_2(R,I, {nr}pk(I),hash(ni,R) );
read_3(I,R, hash(nr, I,R) );
claim_r1(R,Secret,ni);
claim_r2(R,Secret,nr);
claim_r3(R,Niagree);
claim_r4(R,Nisynch);
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);
run boydNS.I(Agent,Agent);
run boydNS.R(Agent,Agent);

81
spdl/misc/boyd.spdl
View File

@ -1,81 +0,0 @@
usertype Sessionkey;
usertype Macseed;
secret k: Function;
const m: Function;
secret unm: Function;
const f: Function;
inversekeys (m, unm);
/*
* Boyd key agreement
*
* Boyd & Mathuria: Protocols for authentication and key establishment
* (2003) p. 101
*
* Note that MAC_ks(x) has been interpreted as MAC(x,ks); this
* assumption causes some possible false attacks.
*/
protocol boyd(I,R,S)
{
role I
{
const ni: Nonce;
var nr: Nonce;
var ks: Macseed;
send_1 (I,S, I,R, ni );
read_3 (R,I, { I,R, ks }k(I,S), m(ni, m(ks,ni,nr)), nr );
send_4 (I,R, m(nr, m(ks,ni,nr)) );
claim_6 (I, Secret, m(ks,ni,nr) );
claim_7 (I, Niagree);
claim_8 (I, Nisynch);
}
role R
{
var ni: Nonce;
const nr: Nonce;
var ks: Macseed;
read_2 (S,R, { I,R, ks }k(I,S), { I,R, ks }k(R,S), ni );
send_3 (R,I, { I,R, ks }k(I,S), m(ni, m(ks,ni,nr)), nr );
read_4 (I,R, m(nr, m(ks,ni,nr)) );
claim_10 (R, Secret, m(ks,ni,nr));
claim_11 (R, Niagree);
claim_12 (R, Nisynch);
}
role S
{
var ni,nr: Nonce;
const ks: Macseed;
read_1 (I,S, I,R, ni );
send_2 (S,R, { I,R, ks }k(I,S), { I,R, ks }k(R,S), ni );
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
const mcsde: Macseed;
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);
run boyd.I(Agent,Agent,Simon);
run boyd.R(Agent,Agent,Simon);
run boyd.S(Agent,Agent,Simon);
run boyd.I(Agent,Agent,Simon);
run boyd.R(Agent,Agent,Simon);
run boyd.S(Agent,Agent,Simon);

39
spdl/misc/broken1.spdl
View File

@ -1,39 +0,0 @@
/*
* A broken protocol
*
* Cas Cremers
* Visualization challenge of the week.
* Can be checked withouth CL, please do so.
*/
usertype String, Key;
const PlainSight: String;
secret HelloWorld, HelloServer: String;
secret k: Key;
protocol broken1(I,R,S)
{
role I
{
send_1(I, R, PlainSight, {HelloWorld, I, R}k );
send_2(I, S, {HelloServer, I, S}k );
}
role R
{
read_3(S, R, {HelloWorld, S, I, R}k );
read_1(I, R, PlainSight, {HelloWorld, I, R}k );
claim_4(R, Secret, PlainSight);
}
role S
{
read_2(I, S, {HelloServer, I, S}k );
send_3(S, R, {HelloWorld, S, I, R}k );
}
}
const a, b, S: Agent;
run broken1.I(a, b, S);
run broken1.R(a, b, S);
run broken1.S(a, b, S);

89
spdl/misc/bunava-1-3.spdl
View File

@ -1,89 +0,0 @@
# Buttyan Nagy Vajda protocol 1 (3-party)
#
# Modelled after the description in the paper
# "Efficient multi-party challenge-response protocols for entity
# authentication"
#
# Attacks:
# Does not satisfy ni-agree, because when Alice in the A role terminates
# it cannot be sure that the agent in role B is aware of having sent a
# reply for Alice.
# A type flaw attack exists in which there are only two agents active.
#
secret k: Function;
protocol intruderhelp(Swap)
{
role Swap
{
var T: Ticket;
var A,B: Agent;
read_1(Swap,Swap, { T }k(A,B) );
send_2(Swap,Swap, { T }k(B,A) );
}
}
protocol bunava13(A,B,C)
{
role A
{
const ra: Nonce;
var rb,rc: Nonce;
send_1(A,B, ra);
read_3(C,A, rc,{C,rb,B,ra}k(A,C) );
send_4(A,B, {A,rc,C,rb}k(A,B) );
claim_A1(A, Niagree);
claim_A2(A, Nisynch);
}
role B
{
const rb: Nonce;
var ra,rc: Nonce;
read_1(A,B, ra);
send_2(B,C, rb,{B,ra}k(B,C) );
read_4(A,B, {A,rc,C,rb}k(A,B) );
send_5(B,C, {B,A,rc}k(B,C) );
claim_B1(B, Niagree);
claim_B2(B, Nisynch);
}
role C
{
const rc: Nonce;
var ra,rb: Nonce;
read_2(B,C, rb,{B,ra}k(B,C) );
send_3(C,A, rc,{C,rb,B,ra}k(A,C) );
read_5(B,C, {B,A,rc}k(B,C) );
claim_C1(C, Niagree);
claim_C2(C, Nisynch);
}
}
const Alice,Bob,Charlie,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised k(Alice,Eve);
compromised k(Bob,Eve);
compromised k(Charlie,Eve);
compromised k(Eve,Alice);
compromised k(Eve,Bob);
compromised k(Eve,Charlie);
# General scenario, 2 parallel runs of the protocol
run bunava13.A(Agent,Agent,Agent);
run bunava13.B(Agent,Agent,Agent);
run bunava13.C(Agent,Agent,Agent);
run bunava13.A(Agent,Agent,Agent);
run bunava13.B(Agent,Agent,Agent);
run bunava13.C(Agent,Agent,Agent);

106
spdl/misc/bunava-1-4.spdl
View File

@ -1,106 +0,0 @@
# Buttyan Nagy Vajda protocol 1 (4-party)
#
# Modelled after the description in the paper
# "Efficient multi-party challenge-response protocols for entity
# authentication"
#
# Attacks:
# Does not satisfy ni-agree, because when Alice in the A role terminates
# it cannot be sure that the agent in role B is aware of having sent a
# reply for Alice.
# A type flaw attack exists in which there are only three agents active.
# Especially -m2 attack 17 is nice, I think.
#
secret k: Function;
protocol intruderhelp(Swap)
{
role Swap
{
var T: Ticket;
var A,B: Agent;
read_1(Swap,Swap, { T }k(A,B) );
send_2(Swap,Swap, { T }k(B,A) );
}
}
protocol bunava14(A,B,C,D)
{
role A
{
const ra: Nonce;
var rb,rc,rd: Nonce;
send_1(A,B, ra);
read_4(D,A, rd,{D,rc,C,rb,B,ra}k(A,D) );
send_5(A,B, {A,rd,D,rc,C,rb}k(A,B) );
claim_A1(A, Niagree);
claim_A2(A, Nisynch);
}
role B
{
const rb: Nonce;
var ra,rc,rd: Nonce;
read_1(A,B, ra);
send_2(B,C, rb,{B,ra}k(B,C) );
read_5(A,B, {A,rd,D,rc,C,rb}k(A,B) );
send_6(B,C, {B,A,rd,D,rc}k(B,C) );
claim_B1(B, Niagree);
claim_B2(B, Nisynch);
}
role C
{
const rc: Nonce;
var ra,rb,rd: Nonce;
read_2(B,C, rb,{B,ra}k(B,C) );
send_3(C,D, rc,{C,rb,B,ra}k(C,D) );
read_6(B,C, {B,A,rd,D,rc}k(B,C) );
send_7(C,D, {C,B,A,rd}k(C,D) );
claim_C1(C, Niagree);
claim_C2(C, Nisynch);
}
role D
{
const rd: Nonce;
var ra,rb,rc: Nonce;
read_3(C,D, rc,{C,rb,B,ra}k(C,D) );
send_4(D,A, rd,{D,rc,C,rb,B,ra}k(A,D) );
read_7(C,D, {C,B,A,rd}k(C,D) );
claim_D1(D, Niagree);
claim_D2(D, Nisynch);
}
}
const Alice,Bob,Charlie,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised k(Alice,Eve);
compromised k(Bob,Eve);
compromised k(Charlie,Eve);
compromised k(Eve,Alice);
compromised k(Eve,Bob);
compromised k(Eve,Charlie);
# General scenario, 2 parallel runs of the protocol
run bunava14.A(Agent,Agent,Agent,Agent);
run bunava14.B(Agent,Agent,Agent,Agent);
run bunava14.C(Agent,Agent,Agent,Agent);
run bunava14.D(Agent,Agent,Agent,Agent);
run bunava14.A(Agent,Agent,Agent,Agent);
run bunava14.B(Agent,Agent,Agent,Agent);
run bunava14.C(Agent,Agent,Agent,Agent);
run bunava14.D(Agent,Agent,Agent,Agent);

88
spdl/misc/bunava-2-3.spdl
View File

@ -1,88 +0,0 @@
# Buttyan Nagy Vajda protocol 2 (3-party)
#
# Modelled after the description in the paper
# "Efficient multi-party challenge-response protocols for entity
# authentication"
#
# Attacks:
#
secret k: Function;
protocol intruderhelp(Swap)
{
role Swap
{
var T: Ticket;
var A,B: Agent;
read_1(Swap,Swap, { T }k(A,B) );
send_2(Swap,Swap, { T }k(B,A) );
}
}
protocol bunava23(A,B,C)
{
role A
{
const ra: Nonce;
var rb,rc: Nonce;
var Ta: Ticket;
send_1(A,B, ra);
read_3(C,A, rc, Ta, { C,{ B,ra }k(A,B) }k(A,C) );
send_4(A,B, { A,rc }k(A,C), { A, Ta }k(A,B) );
claim_A1(A, Niagree);
claim_A2(A, Nisynch);
}
role B
{
const rb: Nonce;
var ra,rc: Nonce;
var Tb: Ticket;
read_1(A,B, ra);
send_2(B,C, rb,{B,ra}k(B,C) );
read_4(A,B, Tb, { A, { C,rb }k(B,C) }k(A,B) );
send_5(B,C, { B, Tb }k(B,C) );
claim_B1(B, Niagree);
claim_B2(B, Nisynch);
}
role C
{
const rc: Nonce;
var ra,rb: Nonce;
var Tc: Ticket;
read_2(B,C, rb, Tc );
send_3(C,A, rc,{ C,rb }k(B,C), { C, Tc }k(A,C) );
read_5(B,C, { B, { A,rc }k(A,C) }k(B,C) );
claim_C1(C, Niagree);
claim_C2(C, Nisynch);
}
}
const Alice,Bob,Charlie,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised k(Alice,Eve);
compromised k(Bob,Eve);
compromised k(Charlie,Eve);
compromised k(Eve,Alice);
compromised k(Eve,Bob);
compromised k(Eve,Charlie);
# General scenario
run bunava23.A(Agent,Agent,Agent);
run bunava23.B(Agent,Agent,Agent);
run bunava23.C(Agent,Agent,Agent);
run bunava23.A(Agent,Agent,Agent);
run bunava23.B(Agent,Agent,Agent);
run bunava23.C(Agent,Agent,Agent);

138
spdl/misc/bunava-2-4.spdl
View File

@ -1,138 +0,0 @@
# Buttyan Nagy Vajda protocol 2 (4-party)
#
# Modelled after the description in the paper
# "Efficient multi-party challenge-response protocols for entity
# authentication"
#
# Note:
# Does not seem to reach the claim. I don't know why yet. TODO
# investigate.
#
secret k: Function;
# protocol intruderhelp(Swap)
# {
# role Swap
# {
# var T: Ticket;
# var A,B: Agent;
#
# read_1(Swap,Swap, { T }k(A,B) );
# send_2(Swap,Swap, { T }k(B,A) );
# }
# }
protocol bunava24(A,B,C,D)
{
role A
{
const ra: Nonce;
var rb,rc,rd: Nonce;
var Tacd, Tabd: Ticket;
send_1(A,B, ra);
read_4(D,A, rd,
Tacd,
Tabd,
{ D, { C, { B,ra }k(A,B) }k(A,C) }k(A,D)
);
# send_5(A,B,
# { A, rd }k(A,D),
# { A, Tacd }k(A,C),
# { A, Tabd }k(A,B)
# );
claim_A1(A, Niagree);
claim_A2(A, Nisynch);
}
role B
{
const rb: Nonce;
var ra,rc,rd: Nonce;
var Tbad, Tbac: Ticket;
read_1(A,B, ra);
send_2(B,C, rb,
{ B,ra }k(A,B)
);
# read_5(A,B,
# Tbad,
# Tbac,
# { A, { D, { C,rb }k(B,C) }k(B,D) }k(A,B)
# );
# send_6(B,C,
# { B, Tbad }k(B,D),
# { B, Tbac }k(B,C)
# );
#
# claim_B1(B, Niagree);
# claim_B2(B, Nisynch);
}
role C
{
const rc: Nonce;
var ra,rb,rd: Nonce;
var Tcab,Tcbd: Ticket;
read_2(B,C, rb, Tcab );
send_3(C,D, rc,
{ C, rb }k(B,C),
{ C, Tcab }k(A,C)
);
# read_6(B,C,
# Tcbd,
# { B, { A,{ D,rc }k(C,D) }k(A,C) }k(B,C)
# );
# send_7(C,D,
# { C, Tcbd }k(C,D)
# );
#
# claim_C1(C, Niagree);
# claim_C2(C, Nisynch);
}
role D
{
const rd: Nonce;
var ra,rb,rc: Nonce;
var Tdbc,Tdac: Ticket;
read_3(C,D, rc, Tdbc, Tdac );
send_4(D,A, rd,
{ D, rc }k(C,D),
{ D, Tdbc }k(B,D),
{ D, Tdac }k(A,D)
);
# read_7(C,D,
# { C, { B,{ A,rd }k(A,D) }k(B,D) }k(C,D)
# );
#
# claim_D1(D, Niagree);
# claim_D2(D, Nisynch);
}
}
const Alice,Bob,Charlie,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised k(Alice,Eve);
compromised k(Bob,Eve);
compromised k(Charlie,Eve);
compromised k(Eve,Alice);
compromised k(Eve,Bob);
compromised k(Eve,Charlie);
# General scenario
run bunava24.A(Agent,Agent,Agent,Agent);
run bunava24.B(Agent,Agent,Agent,Agent);
run bunava24.C(Agent,Agent,Agent,Agent);
run bunava24.D(Agent,Agent,Agent,Agent);
run bunava24.A(Agent,Agent,Agent,Agent);
run bunava24.B(Agent,Agent,Agent,Agent);
run bunava24.C(Agent,Agent,Agent,Agent);
run bunava24.D(Agent,Agent,Agent,Agent);

32
spdl/misc/carkey-broken-limited.spdl
View File

@ -1,32 +0,0 @@
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol carkeybrokenlim(I,R)
{
role I
{
const ni: Nonce;
send_1(I,R, I,R );
}
role R
{
var ni: Nonce;
read_1(I,R, I,R );
claim_2(R,Nisynch);
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const nc: Nonce;
compromised sk(Eve);
run carkeybrokenlim.I(Alice,Bob);
run carkeybrokenlim.R(Alice,Bob);
run carkeybrokenlim.I(Alice,Bob);
run carkeybrokenlim.R(Alice,Bob);

32
spdl/misc/carkey-broken.spdl
View File

@ -1,32 +0,0 @@
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol carkeybroken(I,R)
{
role I
{
const ni: Nonce;
send_1(I,R, {ni}sk(I) );
}
role R
{
var ni: Nonce;
read_1(I,R, {ni}sk(I) );
claim_2(R,Nisynch);
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const nc: Nonce;
compromised sk(Eve);
run carkeybroken.I(Agent,Agent);
run carkeybroken.R(Agent,Agent);
run carkeybroken.I(Agent,Agent);
run carkeybroken.R(Agent,Agent);

32
spdl/misc/carkey-ni.spdl
View File

@ -1,32 +0,0 @@
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol carkeyni(I,R)
{
role I
{
const ni: Nonce;
send_1(I,R, {R,ni}sk(I) );
}
role R
{
var ni: Nonce;
read_1(I,R, {R,ni}sk(I) );
claim_2(R,Nisynch);
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const nc: Nonce;
compromised sk(Eve);
run carkeyni.I(Agent,Agent);
run carkeyni.R(Agent,Agent);
run carkeyni.I(Agent,Agent);
run carkeyni.R(Agent,Agent);

34
spdl/misc/carkey-ni2.spdl
View File

@ -1,34 +0,0 @@
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol carkeyni2(I,R)
{
role I
{
const ni: Nonce;
send_1(I,R, {R,ni}sk(I) );
send_2(I,R, {R,ni}sk(I) );
}
role R
{
var ni: Nonce;
read_1(I,R, {R,ni}sk(I) );
read_2(I,R, {R,ni}sk(I) );
claim_4(R,Nisynch);
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const nc: Nonce;
compromised sk(Eve);
run carkeyni2.I(Agent,Agent);
run carkeyni2.R(Agent,Agent);
run carkeyni2.I(Agent,Agent);
run carkeyni2.R(Agent,Agent);

53
spdl/misc/ccitt509-ban.spdl
View File

@ -1,53 +0,0 @@
usertype Data;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol ccitt509(I,R)
{
role I
{
const xi,yi: Data;
const ni: Nonce;
var nr: Nonce;
var yr,xr: Data;
send_1(I,R, I,{ni, R, xi, {yi}pk(R) }sk(I) );
read_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) );
send_3(I,R, I,{R,nr}sk(I) );
claim_4(I,Secret,yi);
claim_5(I,Secret,yr);
claim_6(I,Nisynch);
claim_7(I,Niagree);
}
role R
{
var xi,yi: Data;
var ni: Nonce;
const nr: Nonce;
const yr,xr: Data;
read_1(I,R, I,{ni, R, xi, {yi}pk(R) }sk(I) );
send_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) );
read_3(I,R, I,{R,nr}sk(I) );
claim_8(R,Secret,yi);
claim_9(R,Secret,yr);
claim_10(R,Nisynch);
claim_11(R,Niagree);
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;
const de: Data;
compromised sk(Eve);
run ccitt509.I(Agent,Agent);
run ccitt509.R(Agent,Agent);
run ccitt509.I(Agent,Agent);
run ccitt509.R(Agent,Agent);

74
spdl/misc/denning-sacco-shared.spdl
View File

@ -1,74 +0,0 @@
/*
* Denning-Sacco shared key
* CJ, but modeled after Sjouke's protocol list
*/
/* default includes */
/* asymmetric */
const pk,hash: Function;
secret sk,unhash: Function;
/* symmetric */
usertype SessionKey, Time, Ticket;
secret k: Function;
/* agents */
const a,b,e: Agent;
/* untrusted e */
untrusted e;
const ne: Nonce;
const kee: SessionKey;
compromised k(e,e);
compromised k(e,a);
compromised k(e,b);
compromised k(a,e);
compromised k(b,e);
protocol denningsaccosh(A,S,B)
{
role A
{
var t: Time;
var T: Ticket;
var kab: SessionKey;
send_1 (A,S, A,S );
read_2 (S,A, {B, kab, t, T}k(A,S) );
send_3 (A,B, T);
claim_4 (A, Secret, kab);
claim_5 (A, Nisynch);
claim_6 (A, Niagree);
}
role S
{
const t: Time;
const kab: SessionKey;
read_1 (A,S, A,S );
send_2 (S,A, {B, kab, t, { kab, A,t }k(B,S) }k(A,S) );
}
role B
{
var t: Time;
var kab: SessionKey;
read_3 (A,B, { kab, A,t }k(B,S) );
claim_7 (B, Secret, kab);
claim_8 (B, Nisynch);
claim_9 (B, Niagree);
}
}

48
spdl/misc/f4.spdl
View File

@ -1,48 +0,0 @@
/*
* f4.spdl
*
* Tailored protocol to show that any number of runs can be required to
* find an attack.
*
* For this version, -m2 and -r4 are needed.
*
* April 2005, Cas Cremers
*/
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol f4(I,R)
{
role I
{
var nr: Nonce;
read_1(R,I, nr );
send_2(I,R, { nr }sk(I) );
read_3(R,I, {{{{ nr }sk(R)}sk(R)}sk(R)}sk(R) );
claim_i1(I,Niagree);
}
role R
{
const nr: Nonce;
send_1(R,I, nr );
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);

48
spdl/misc/f5.spdl
View File

@ -1,48 +0,0 @@
/*
* f5.spdl
*
* Tailored protocol to show that any number of runs can be required to
* find an attack.
*
* For this version, -m2 and -r5 are needed.
*
* April 2005, Cas Cremers
*/
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol f4(I,R)
{
role I
{
var nr: Nonce;
read_1(R,I, nr );
send_2(I,R, { nr }sk(I) );
read_3(R,I, {{{{{ nr }sk(R)}sk(R)}sk(R)}sk(R)}sk(R) );
claim_i1(I,Niagree);
}
role R
{
const nr: Nonce;
send_1(R,I, nr );
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);
run f4.I(Agent,Agent);

32
spdl/misc/five-run-bound.spdl
View File

@ -1,32 +0,0 @@
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol r5bound(I,R)
{
role R
{
var k1: Nonce;
var ni: Nonce;
const k2: Nonce;
read_1 (I,R, ni );
send_2 (R,I, { ni }sk(R) );
read_3 (I,R, {{{ {k1}pk(R) }sk(I)}sk(I)}sk(I) );
send_4 (R,I, {k2}k1 );
claim_6 (R, Secret, k2);
}
}
const Alice, Bob: Agent;
const ne: Nonce;
run r5bound.R(Agent);
run r5bound.R(Agent);
run r5bound.R(Agent);
run r5bound.R(Agent);
run r5bound.R(Agent);
run r5bound.R(Agent);

81
spdl/misc/gong-nonce-b.spdl
View File

@ -1,81 +0,0 @@
usertype Sessionkey;
usertype Keypart;
secret k: Function;
const f: Function;
/*
* Gong nonce based alternative
*
* Boyd & Mathuria: Protocols for authentication and key establishment
* (2003) p. 101
*/
protocol gongnonceb(I,R,S)
{
role I
{
const ni: Nonce;
var nr: Nonce;
const ki: Keypart;
var kr: Keypart;
send_1 (I,S, I,R, { I,S,I, ki, R }k(I,S), ni );
read_4 (S,I, { S,I,R,kr,I }k(I,S), { R,I,ni }f(ki,kr), nr );
send_5 (I,R, { I,R,nr }f(ki,kr) );
claim_6 (I, Secret, ki);
claim_7 (I, Secret, kr);
claim_8 (I, Nisynch);
claim_9 (I, Niagree);
}
role R
{
var ni: Nonce;
const nr: Nonce;
const kr: Keypart;
var ki: Keypart;
read_2 (S,R, I,R, { S,R,I, ki, R }k(R,S), ni );
send_3 (R,S, { R,S,R,kr,I }k(R,S), { R,I, ni }f(ki,kr), nr );
read_5 (I,R, { I,R,nr }f(ki,kr) );
claim_10 (R, Secret, ki);
claim_11 (R, Secret, kr);
claim_12 (R, Nisynch);
claim_13 (R, Niagree);
}
role S
{
var ni,nr: Nonce;
var ki,kr: Keypart;
var T;
read_1 (I,S, I,R, { I,S,I, ki, R }k(I,S), ni );
send_2 (S,R, I,R, { S,R,I, ki, R }k(R,S), ni );
read_3 (R,S, { R,S,R,kr,I }k(R,S), T, nr );
send_4 (S,I, { S,I,R,kr,I }k(I,S), T, nr );
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
const kpe: Keypart;
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);
run gongnonceb.I(Agent,Agent,Simon);
run gongnonceb.R(Agent,Agent,Simon);
run gongnonceb.S(Agent,Agent,Simon);
run gongnonceb.I(Agent,Agent,Simon);
run gongnonceb.R(Agent,Agent,Simon);
run gongnonceb.S(Agent,Agent,Simon);

72
spdl/misc/gong-nonce.spdl
View File

@ -1,72 +0,0 @@
usertype Sessionkey;
usertype Keypart;
secret k: Function;
protocol gongnonce(I,R,S)
{
role I
{
const ni: Nonce;
var nr: Nonce;
const ki: Keypart;
var kr: Keypart;
send_1 (I,R, I,R,ni );
read_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr);
send_4 (I,S, { I,S,I, ki, R, nr }k(I,S) );
claim_6 (I, Secret, ki);
claim_7 (I, Secret, kr);
claim_8 (I, Nisynch);
claim_9 (I, Niagree);
}
role R
{
var ni: Nonce;
const nr: Nonce;
const kr: Keypart;
var ki: Keypart;
read_1 (I,R, I,R,ni );
send_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S));
read_5 (S,R, { S,R,I, ki, R, nr }k(R,S) );
claim_10 (R, Secret, ki);
claim_11 (R, Secret, kr);
claim_12 (R, Nisynch);
claim_13 (R, Niagree);
}
role S
{
var ni,nr: Nonce;
var ki,kr: Keypart;
read_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S));
send_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr);
read_4 (I,S, { I,S,I, ki, R, nr }k(I,S) );
send_5 (S,R, { S,R,I, ki, R, nr }k(R,S) );
}
}
const Alice,Bob,Simon,Eve: Agent;
untrusted Eve;
const ne: Nonce;
const kpe: Keypart;
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);
run gongnonce.I(Agent,Agent,Simon);
run gongnonce.R(Agent,Agent,Simon);
run gongnonce.S(Agent,Agent,Simon);
run gongnonce.I(Agent,Agent,Simon);
run gongnonce.R(Agent,Agent,Simon);
run gongnonce.S(Agent,Agent,Simon);

17
spdl/misc/helloworld.spdl
View File

@ -1,17 +0,0 @@
usertype String, World;
secret HelloWorld, k: String;
protocol hw(initiator,world)
{
role initiator
{
send_1(initiator, world, HelloWorld);
/* claim_2(initiator, Secret, HelloWorld); */
}
}
const Alice, Bob: Agent;
const Earth, Mars: World;
run hw.initiator(Agent,World);

63
spdl/misc/isoiec11770-2-13.spdl
View File

@ -1,63 +0,0 @@
usertype Sessionkey;
usertype Ticket;
secret k: Function;
protocol isoiec11770213(I,R,S)
{
role I
{
const ni: Nonce;
var nr: Nonce;
var kir: Sessionkey;
send_1 (I,R, ni);
read_4 (R,I, { ni,kir,R }k(I,S) );
claim_5 (I, Secret, kir);
}
role R
{
var ni: Nonce;
const nr: Nonce;
const kir: Sessionkey;
var T;
read_1 (I,R, ni);
send_2 (R,S, { nr,ni,I,kir }k(R,S) );
read_3 (S,R, { nr, I }k(R,S), T );
send_4 (R,I, T );
claim_6 (R, Secret, kir);
}
role S
{
var ni,nr: Nonce;
var kir: Sessionkey;
read_2 (R,S, { nr,ni,I,kir }k(R,S) );
send_3 (S,R, { nr, I }k(R,S), { ni,kir,R }k(I,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);
run isoiec11770213.I(Agent,Agent,Simon);
run isoiec11770213.R(Agent,Agent,Simon);
run isoiec11770213.S(Agent,Agent,Simon);
run isoiec11770213.I(Agent,Agent,Simon);
run isoiec11770213.R(Agent,Agent,Simon);
run isoiec11770213.S(Agent,Agent,Simon);

67
spdl/misc/kaochow-palm.spdl
View File

@ -1,67 +0,0 @@
usertype Sessionkey;
usertype Ticket;
secret k: Function;
protocol kaochowPalm(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_5 (I, Nisynch);
claim_6 (I, Niagree);
claim_7 (I, Secret, 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) }k(R,S) );
send_3 (R,I, T, {ni}kir, nr );
read_4 (I,R, {nr}kir );
claim_8 (R, Nisynch);
claim_9 (R, Niagree);
claim_10 (R, Secret, 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) }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);
run kaochowPalm.I(Agent,Agent,Simon);
run kaochowPalm.R(Agent,Agent,Simon);
run kaochowPalm.S(Agent,Agent,Simon);
run kaochowPalm.I(Agent,Agent,Simon);
run kaochowPalm.R(Agent,Agent,Simon);
run kaochowPalm.S(Agent,Agent,Simon);

67
spdl/misc/kaochow-v2.spdl
View File

@ -1,67 +0,0 @@
usertype Sessionkey;
usertype Ticket;
secret k: Function;
protocol kaochow2(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_5 (I, Nisynch);
claim_6 (I, Niagree);
claim_7 (I, Secret, 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_8 (R, Nisynch);
claim_9 (R, Niagree);
claim_10 (R, Secret, 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);
run kaochow2.I(Agent,Agent,Simon);
run kaochow2.R(Agent,Agent,Simon);
run kaochow2.S(Agent,Agent,Simon);
run kaochow2.I(Agent,Agent,Simon);
run kaochow2.R(Agent,Agent,Simon);
run kaochow2.S(Agent,Agent,Simon);

70
spdl/misc/kaochow-v3.spdl
View File

@ -1,70 +0,0 @@
usertype Sessionkey;
usertype Ticket;
usertype Timestamp;
secret k: Function;
protocol kaochow3(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, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 );
send_4 (I,R, {nr,kir}kt, T2 );
claim_5 (I, Nisynch);
claim_6 (I, Niagree);
claim_7 (I, Secret, 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, R, 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_8 (R, Nisynch);
claim_9 (R, Niagree);
claim_10 (R, Secret, 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);
run kaochow3.I(Agent,Agent,Simon);
run kaochow3.R(Agent,Agent,Simon);
run kaochow3.S(Agent,Agent,Simon);
run kaochow3.I(Agent,Agent,Simon);
run kaochow3.R(Agent,Agent,Simon);
run kaochow3.S(Agent,Agent,Simon);

67
spdl/misc/kaochow.spdl
View File

@ -1,67 +0,0 @@
usertype Sessionkey;
usertype Ticket;
secret k: Function;
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_5 (I, Nisynch);
claim_6 (I, Niagree);
claim_7 (I, Secret, 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_8 (R, Nisynch);
claim_9 (R, Niagree);
claim_10 (R, Secret, 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);
run kaochow.I(Agent,Agent,Simon);
run kaochow.R(Agent,Agent,Simon);
run kaochow.S(Agent,Agent,Simon);
run kaochow.I(Agent,Agent,Simon);
run kaochow.R(Agent,Agent,Simon);
run kaochow.S(Agent,Agent,Simon);

83
spdl/misc/ksl.spdl
View File

@ -1,83 +0,0 @@
/*
* KSL from SPORE
*
* Messages 6-8 are intended for repeated authentication, and there are
* known attacks on this. However, we don't model that yet.
*
* Furthermore, it is interesting to experiment here with key
* compromise (of kab), when this is implemented in Scyther.
*/
usertype Server, SessionKey, GeneralizedTimestamp, Ticket, TicketKey;
secret k: Function;
const a, b, e: Agent;
const s: Server;
/* give the intruder something to work with */
const ne: Nonce;
const kee: SessionKey;
untrusted e;
compromised k(e,s);
protocol ksl(A,B,S)
{
role A
{
const Na, Ma: Nonce;
var Nc, Mb: Nonce;
var T: Ticket;
var Kab: SessionKey;
send_1(A,B, Na, A);
read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab );
send_5(A,B, { Nc }Kab );
send_6(A,B, Ma,T );
read_7(B,A, Mb,{Ma}Kab );
send_8(A,B, {Mb}Kab );
claim_A1(A,Secret, Kab);
claim_A2(A,Niagree);
claim_A3(A,Nisynch);
}
role B
{
var Na,Ma: Nonce;
const Nb,Nc,Mb: Nonce;
var Kab: SessionKey;
const Kbb: TicketKey;
const Tb: GeneralizedTimestamp;
var T: Ticket;
read_1(A,B, Na, A);
send_2(B,S, Na, A, Nb, B );
read_3(S,B, { Nb, A, Kab }k(B,S), T );
send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {Na}Kab );
read_5(A,B, { Nc }Kab );
read_6(A,B, Ma,{ Tb, A, Kab }Kbb );
send_7(B,A, Mb,{Ma}Kab );
read_8(A,B, {Mb}Kab );
claim_B1(B,Secret, Kab);
claim_B2(B,Niagree);
claim_B3(B,Nisynch);
}
role S
{
var Na, Nb: Nonce;
const Kab: SessionKey;
read_2(B,S, Na, A, Nb, B );
send_3(S,B, { Nb, A, Kab }k(B,S), { Na,B,Kab }k(A,S) );
}
}
run ksl.A(a,b,s);
run ksl.B(a,b,s);
run ksl.S(a,b,s);

83
spdl/misc/ns-symmetric-amended.spdl
View File

@ -1,83 +0,0 @@
/*
* Needham-Schroeder symmetric
* Amended version (from Sjouke's interpret.)
*/
/* symmetric */
usertype SessionKey;
secret k: Function;
/* agents */
const a,b,e: Agent;
/* untrusted e */
untrusted e;
const ne: Nonce;
const kee: SessionKey;
compromised k(e,e);
compromised k(e,a);
compromised k(e,b);
compromised k(a,e);
compromised k(b,e);
/* {}x used for public (invertible) function modeling */
usertype PseudoFunction;
const succ: PseudoFunction;
usertype Ticket;
protocol nssymmetricamended(A,S,B)
{
role A
{
const na: Nonce;
var T1: Ticket;
var T2: Ticket;
var kab: SessionKey;
var nb: Nonce;
send_1(A,B, A );
read_2(B,A, T1 );
send_3(A,S, A,B,na,T1 );
read_4(S,A, { na,B,kab,T2 }k(A,S) );
send_5(A,B, T2 );
read_6(B,A, { nb }kab );
send_7(A,B, { {nb}succ }kab );
claim_8(A, Secret, kab);
claim_8a(A, Niagree);
claim_8b(A, Nisynch);
}
role S
{
const kab: SessionKey;
var na: Nonce;
var nb: Nonce;
read_3(A,S, A,B,na, { A,nb }k(B,S) );
send_4(S,A, { na,B,kab, { kab,A }k(B,S) }k(A,S) );
}
role B
{
var kab: SessionKey;
const nb: Nonce;
read_1(A,B, A );
send_2(B,A, { A,nb }k(B,S) );
read_5(A,B, { kab,A }k(B,S) );
send_6(B,A, { nb }kab );
read_7(A,B, { {nb}succ }kab );
claim_9(B, Secret, kab);
claim_9a(B, Niagree);
claim_9b(B, Nisynch);
}
}

72
spdl/misc/ns-symmetric.spdl
View File

@ -1,72 +0,0 @@
/*
* Needham-Schroeder symmetric
*/
/* symmetric */
usertype SessionKey;
secret k: Function;
/* agents */
const a,b,e: Agent;
/* untrusted e */
untrusted e;
const ne: Nonce;
const kee: SessionKey;
compromised k(e,e);
compromised k(e,a);
compromised k(e,b);
compromised k(a,e);
compromised k(b,e);
/* {}x used for public (invertible) function modeling */
usertype PseudoFunction;
const succ: PseudoFunction;
usertype Ticket;
protocol nssymmetric(A,S,B)
{
role A
{
const na: Nonce;
var T: Ticket;
var kab: SessionKey;
var nb: Nonce;
send_1(A,S, A,B,na );
read_2(S,A, { na,B,kab,T }k(A,S) );
send_3(A,B, T );
read_4(B,A, { nb }kab );
send_5(A,B, { {nb}succ }kab );
claim_6(A, Secret, kab);
}
role S
{
const kab: SessionKey;
var na: Nonce;
read_1(A,S, A,B,na );
send_2(S,A, { na,B,kab, { kab,A }k(B,S) }k(A,S) );
}
role B
{
var kab: SessionKey;
const nb: Nonce;
read_3(A,B, { kab,A }k(B,S) );
send_4(B,A, { nb }kab );
read_5(A,B, { {nb}succ }kab );
claim_7(B, Secret, kab);
}
}

50
spdl/misc/ns3-brutus.spdl
View File

@ -1,50 +0,0 @@
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol ns3brutus(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
send_1(I,R, {I,ni}pk(R) );
read_2(R,I, {ni,nr}pk(I) );
send_3(I,R, {nr}pk(R) );
claim_4(I,Secret,nr);
}
role R
{
var ni: Nonce;
const nr: Nonce;
read_1(I,R, {I,ni}pk(R) );
send_2(R,I, {ni,nr}pk(I) );
read_3(I,R, {nr}pk(R) );
claim_5(R,Secret,ni);
}
}
const Alice,Bob,Eve : Agent;
/* something like this will later on all be implied by 'untrusted Eve' */
untrusted Eve;
/* const nc: Nonce; */
compromised sk(Eve);
/* pre-defined 10 runs, limit using --max-runs parameters */
/* to be nice to brutus, stupid scenario :( */
run ns3brutus.R(Agent,Bob);
run ns3brutus.I(Alice,Agent);
run ns3brutus.R(Agent,Bob);
run ns3brutus.I(Alice,Agent);
run ns3brutus.R(Agent,Bob);
run ns3brutus.I(Alice,Agent);
run ns3brutus.R(Agent,Bob);
run ns3brutus.I(Alice,Agent);
run ns3brutus.R(Agent,Bob);
run ns3brutus.I(Alice,Agent);

67
spdl/misc/ns3.spdl
View File

@ -1,67 +0,0 @@
/*
* Needham-Schroeder protocol
*/
// PKI infrastructure
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
// The protocol description
protocol ns3(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
send_1(I,R, {I,ni}pk(R) );
read_2(R,I, {ni,nr}pk(I) );
send_3(I,R, {nr}pk(R) );
claim_i1(I,Secret,ni);
claim_i2(I,Secret,nr);
claim_i3(I,Niagree);
claim_i4(I,Nisynch);
}
role R
{
var ni: Nonce;
const nr: Nonce;
read_1(I,R, {I,ni}pk(R) );
send_2(R,I, {ni,nr}pk(I) );
read_3(I,R, {nr}pk(R) );
claim_r1(R,Secret,ni);
claim_r2(R,Secret,nr);
claim_r3(R,Niagree);
claim_r4(R,Nisynch);
}
}
// The agents in the system
const Alice,Bob: Agent;
// An untrusted agent, with leaked information
const Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);
// The runs (only needed for the modelchecker algorithm)
run ns3.I(Agent,Agent);
run ns3.R(Agent,Agent);
run ns3.I(Agent,Agent);
run ns3.R(Agent,Agent);
run ns3.I(Agent,Agent);
run ns3.R(Agent,Agent);
run ns3.I(Agent,Agent);
run ns3.R(Agent,Agent);
run ns3.I(Agent,Agent);
run ns3.R(Agent,Agent);

102
spdl/misc/nsl-generalized-4.spdl
View File

@ -1,102 +0,0 @@
/*
* Generalized Needham-Schroeder-Lowe protocol.
* Four-party version.
*
* Specific order of interleaving in message 1-4 is required to (a)
* avoid type flaws whilst (b) retaining NSL structure for the simple
* case.
*
* Mon May 23 11:49:29 CEST 2005
*/
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol nslgen4(R1,R2,R3,R4)
{
role R1
{
const n1: Nonce;
var n2,n3,n4: Nonce;
send_1(R1,R2, {n1,R1,R3,R4}pk(R2) );
read_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) );
send_5(R1,R2, {n2,n3,n4}pk(R2) );
claim_r1a(R1,Secret,n1);
claim_r1b(R1,Secret,n2);
claim_r1c(R1,Secret,n3);
claim_r1d(R1,Secret,n4);
claim_r1A(R1,Niagree);
claim_r1S(R1,Nisynch);
}
role R2
{
const n2: Nonce;
var n1,n3,n4: Nonce;
read_1(R1,R2, {n1,R1,R3,R4}pk(R2) );
send_2(R2,R3, {n1,R1,n2,R2,R4}pk(R3) );
read_5(R1,R2, {n2,n3,n4}pk(R2) );
send_6(R2,R3, {n3,n4}pk(R3) );
claim_r2a(R2,Secret,n1);
claim_r2b(R2,Secret,n2);
claim_r2c(R2,Secret,n3);
claim_r2d(R2,Secret,n4);
claim_r2A(R2,Niagree);
claim_r2S(R2,Nisynch);
}
role R3
{
const n3: Nonce;
var n1,n2,n4: Nonce;
read_2(R2,R3, {n1,R1,n2,R2,R4}pk(R3) );
send_3(R3,R4, {n1,R1,n2,R2,n3,R3}pk(R4) );
read_6(R2,R3, {n3,n4}pk(R3) );
send_7(R3,R4, {n4}pk(R4) );
claim_r3a(R3,Secret,n1);
claim_r3b(R3,Secret,n2);
claim_r3c(R3,Secret,n3);
claim_r3d(R3,Secret,n4);
claim_r3A(R3,Niagree);
claim_r3S(R3,Nisynch);
}
role R4
{
const n4: Nonce;
var n1,n2,n3: Nonce;
read_3(R3,R4, {n1,R1,n2,R2,n3,R3}pk(R4) );
send_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) );
read_7(R3,R4, {n4}pk(R4) );
claim_r4a(R4,Secret,n1);
claim_r4b(R4,Secret,n2);
claim_r4c(R4,Secret,n3);
claim_r4d(R4,Secret,n4);
claim_r4A(R4,Niagree);
claim_r4S(R4,Nisynch);
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);
run nslgen4.R1(Agent,Agent,Agent,Agent);
run nslgen4.R2(Agent,Agent,Agent,Agent);
run nslgen4.R3(Agent,Agent,Agent,Agent);
run nslgen4.R4(Agent,Agent,Agent,Agent);

43
spdl/misc/nsl3-nisynch-rep.spdl
View File

@ -1,43 +0,0 @@
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol nsl3rep(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
send_1(I,R, {I,ni}pk(R) );
send_6(I,R, {I,ni}pk(R) );
read_2(R,I, {ni,nr,R}pk(I) );
send_3(I,R, {nr}pk(R) );
claim_4(I,Niagree);
claim_7(I,Nisynch);
}
role R
{
var ni: Nonce;
const nr: Nonce;
read_1(I,R, {I,ni}pk(R) );
read_6(I,R, {I,ni}pk(R) );
send_2(R,I, {ni,nr,R}pk(I) );
read_3(I,R, {nr}pk(R) );
claim_5(R,Niagree);
claim_8(R,Nisynch);
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const nc: Nonce;
compromised sk(Eve);
run nsl3rep.I(Agent,Agent);
run nsl3rep.R(Agent,Agent);
run nsl3rep.I(Agent,Agent);
run nsl3rep.R(Agent,Agent);

43
spdl/misc/nsl3.spdl
View File

@ -1,43 +0,0 @@
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol nsl3(I,R)
{
role I
{
const ni: Nonce;
var nr: Nonce;
send_1(I,R, {I,ni}pk(R) );
read_2(R,I, {ni,nr,R}pk(I) );
send_3(I,R, {nr}pk(R) );
claim_i1(I,Secret,ni);
claim_i2(I,Secret,nr);
claim_i3(I,Niagree);
claim_i4(I,Nisynch);
}
role R
{
var ni: Nonce;
const nr: Nonce;
read_1(I,R, {I,ni}pk(R) );
send_2(R,I, {ni,nr,R}pk(I) );
read_3(I,R, {nr}pk(R) );
claim_r1(R,Secret,ni);
claim_r2(R,Secret,nr);
claim_r3(R,Niagree);
claim_r4(R,Nisynch);
}
}
const Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);

26
spdl/misc/nsl7.spdl
View File

@ -1,26 +0,0 @@
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol nsl7(I,R)
{
role R
{
var ni;
const nr;
read_1(I,R, {I,ni}pk(R) );
send_2(R,I, {ni,nr,R}pk(I) );
read_3(I,R, {nr}pk(R) );
claim_4(R,Secret,ni);
claim_5(R,Secret,nr);
}
}
const Alice,Bob,Eve;
const ne;
untrusted Eve;
compromised sk(Eve);
run nsl7.R(Agent,Agent);
run nsl7.R(Agent,Agent);

30
spdl/misc/onetrace.spdl
View File

@ -1,30 +0,0 @@
usertype String;
const Alice,Bob,Charlie: Agent;
const Hallo: String;
protocol onetrace(I)
{
role I
{
var input: String;
read_1(I,I, input);
send_2(I,I, Hallo);
read_3(I,I, input);
claim_4(I, Secret, input);
}
}
run onetrace.I(Alice);
run onetrace.I(Alice);
run onetrace.I(Alice);
run onetrace.I(Alice);
run onetrace.I(Alice);
run onetrace.I(Alice);
run onetrace.I(Alice);
run onetrace.I(Alice);
run onetrace.I(Alice);
run onetrace.I(Alice);

66
spdl/misc/otwayrees.spdl
View File

@ -1,66 +0,0 @@
secret const k : Function;
/* Version from the Spore Librairy
http://www.lsv.ens-cachan.fr/spore/otwayRees.html
*/
usertype String, SesKey, Ticket, Server;
protocol otwayrees(A,B,S)
{
role A
{
const na : Nonce;
const M : String;
var kab : SesKey;
send_1(A,B, M,A,B, { na,M,A,B }k(A,S) );
read_4(B,A, M, { na,kab }k(A,S) );
claim_5(A, Secret,kab);
claim_5b(A, Niagree);
claim_5c(A, Nisynch);
}
role B
{
var M : String;
const nb : Nonce;
var kab : SesKey;
var t1,t2;
read_1(A,B, M,A,B, t1 );
send_2(B,S, M,A,B, t1, { nb,M,A,B }k(B,S) );
read_3(S,B, M, t2, { nb,kab }k(B,S) );
send_4(B,A, M, t2 );
claim_6(B, Secret,kab);
claim_6a(B, Niagree);
claim_6b(B, Nisynch);
}
role S
{
var na,nb : Nonce;
var M : String;
const kab : SesKey;
read_2(B,S, M,A,B, { na,M,A,B }k(A,S), { nb,M,A,B }k(B,S) );
send_3(S,B, M, { na,kab }k(A,S) , { nb,kab }k(B,S) );
}
}
const Alice, Bob, Eve: Agent;
const Simon: Server;
untrusted Eve;
compromised k(Eve,Simon);
run otwayrees.A(Alice, Agent, Simon);
run otwayrees.B(Agent, Bob, Simon);
run otwayrees.S(Agent, Agent, Simon);
run otwayrees.A(Agent, Agent, Simon);
run otwayrees.B(Agent, Agent, Simon);
run otwayrees.S(Agent, Agent, Simon);

52
spdl/misc/protocol-list.txt
View File

@ -1,52 +0,0 @@
# List of protocols to test
#
andrew-ban.spdl
andrew-lowe-ban.spdl
#bke-broken.spdl
#bke-one.spdl
#bkepk-ce2.spdl
#bkepk-ce.spdl
#bkepk.spdl
bke.spdl
#boyd.spdl
broken1.spdl
#carkey-broken-limited.spdl
#carkey-broken.spdl
carkey-ni2.spdl
carkey-ni.spdl
ccitt509-ban.spdl
denning-sacco-shared.spdl
five-run-bound.spdl
#gong-nonce-b.spdl
#gong-nonce.spdl
helloworld.spdl
isoiec11770-2-13.spdl
#kaochow-palm.spdl
kaochow.spdl
ns-symmetric.spdl
ns-symmetric-amended.spdl
ns3-brutus.spdl
ns3.spdl
nsl3-nisynch-rep.spdl
nsl3.spdl
nsl7.spdl
#onetrace.spdl
otwayrees.spdl
#samasc-broken.spdl
#simplest.spdl
#soph-keyexch.spdl
#soph.spdl
#speedtest.spdl
splice-as-hc-cj.spdl
#splice-as-hc.spdl
splice-as.spdl
#tls-paulson.spdl
tmn.spdl
#unknown2.spdl
wmf-brutus.spdl
woolam-ce.spdl
woolam-cmv.spdl
yahalom-ban.spdl
yahalom-lowe.spdl
yahalom-paulson.spdl
yahalom.spdl

36
spdl/misc/samasc-broken.spdl
View File

@ -1,36 +0,0 @@
/*
Samasc broken
*/
usertype Key;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol samascbroken(I,R)
{
role R
{
const nr: Nonce;
var kir: Key;
read_1a (I,R, { kir,I }pk(R) );
send_1b (R,I, {nr,R}pk(I) );
/* Commenting out these two lines yields an attack: */
read_2a (I,R, { nr }kir );
send_2b (R,I, { I,R,nr }kir );
read_3 (I,R, { I,R }kir );
claim_4 (R, Secret, kir );
}
}
const a,b,e: Agent;
untrusted e;
compromised sk(e);
const ne: Nonce;

20
spdl/misc/simplest.spdl
View File

@ -1,20 +0,0 @@
secret k: Nonce;
const Alice,Bob,Charlie: Agent;
const ne: Nonce;
protocol simplest(I)
{
role I
{
var x: Nonce;
const n: Nonce;
read_1(I,I, x);
send_2(I,I, n, {n, x}k );
claim_3(I, Secret, n);
}
}
run simplest.I(Alice);
run simplest.I(Alice);

39
spdl/misc/soph-keyexch.spdl
View File

@ -1,39 +0,0 @@
usertype Sessionkey;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol sophkx(I,R)
{
role I
{
const ni: Nonce;
const kir: Sessionkey;
var nr: Nonce;
send_1(I,R, ni, {I,kir}pk(R) );
read_2(R,I, {ni}kir );
claim_4(I,Secret,kir);
}
role R
{
var ni: Nonce;
var kir: Sessionkey;
const nr: Nonce;
read_1(I,R, ni, {I,kir}pk(R) );
send_2(R,I, {ni}kir );
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const nc: Nonce;
const ke: Sessionkey;
compromised sk(Eve);
run sophkx.I(Agent,Agent);
run sophkx.R(Agent,Agent);
run sophkx.I(Agent,Agent);

34
spdl/misc/soph.spdl
View File

@ -1,34 +0,0 @@
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol soph(I,R)
{
role I
{
const ni: Nonce;
send_1(I,R, {I,ni}pk(R) );
read_2(R,I, ni );
claim_3(I,Niagree);
}
role R
{
var ni: Nonce;
read_1(I,R, {I,ni}pk(R) );
send_2(R,I, ni );
}
}
const Alice,Bob,Eve: Agent;
untrusted Eve;
const nc: Nonce;
compromised sk(Eve);
run soph.I(Agent,Agent);
run soph.R(Agent,Agent);
run soph.I(Agent,Agent);
run soph.R(Agent,Agent);

66
spdl/misc/splice-as-hc-cj.spdl
View File

@ -1,66 +0,0 @@
usertype TimeStamp, LifeTime;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol spliceAShcCJ(C,AS,S)
{
role C
{
const N1,N2: Nonce;
const T: TimeStamp;
const L: LifeTime;
send_1(C,AS, C, S, N1 );
read_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) );
send_3(C,S, C, S, {T, L, {C, N2}pk(S)}sk(C) );
read_6(S,C, S, C, {N2}pk(C) );
claim_7(C, Secret, N2);
claim_9(C, Niagree);
claim_10(C, Nisynch);
}
role AS
{
var N1,N3: Nonce;
read_1(C,AS, C, S, N1 );
send_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) );
read_4(S,AS, S, C, N3 );
send_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) );
}
role S
{
const N3: Nonce;
var N2: Nonce;
var T: TimeStamp;
var L: LifeTime;
var ni: Nonce;
const nr: Nonce;
read_3(C,S, C, S, {T, L, {C, N2}pk(S)}sk(C) );
send_4(S,AS, S, C, N3 );
read_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) );
send_6(S,C, S, C, {N2}pk(C) );
claim_8(S, Secret, N2);
claim_11(S, Niagree);
claim_12(S, Nisynch);
}
}
const Al,Bo,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);
run spliceAShcCJ.C(Agent,Agent,Agent);
run spliceAShcCJ.AS(Agent,Agent,Agent);
run spliceAShcCJ.S(Agent,Agent,Agent);

66
spdl/misc/splice-as-hc.spdl
View File

@ -1,66 +0,0 @@
usertype TimeStamp, LifeTime;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol spliceAShc(C,AS,S)
{
role C
{
const N1,N2: Nonce;
const T: TimeStamp;
const L: LifeTime;
send_1(C,AS, C, S, N1 );
read_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) );
send_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) );
read_6(S,C, S, C, {S, N2}pk(C) );
claim_7(C, Secret, N2);
claim_9(C, Niagree);
claim_10(C, Nisynch);
}
role AS
{
var N1,N3: Nonce;
read_1(C,AS, C, S, N1 );
send_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) );
read_4(S,AS, S, C, N3 );
send_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) );
}
role S
{
const N3: Nonce;
var N2: Nonce;
var T: TimeStamp;
var L: LifeTime;
var ni: Nonce;
const nr: Nonce;
read_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) );
send_4(S,AS, S, C, N3 );
read_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) );
send_6(S,C, S, C, {S, N2}pk(C) );
claim_8(S, Secret, N2);
claim_11(S, Niagree);
claim_12(S, Nisynch);
}
}
const Al,Bo,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);
run spliceAShc.C(Agent,Agent,Agent);
run spliceAShc.AS(Agent,Agent,Agent);
run spliceAShc.S(Agent,Agent,Agent);

66
spdl/misc/splice-as.spdl
View File

@ -1,66 +0,0 @@
usertype TimeStamp, LifeTime;
const pk: Function;
secret sk: Function;
inversekeys (pk,sk);
protocol spliceAS(C,AS,S)
{
role C
{
const N1,N2: Nonce;
const T: TimeStamp;
const L: LifeTime;
send_1(C,AS, C, S, N1 );
read_2(AS,C, AS, {AS, C, N1, pk(S)}sk(AS) );
send_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) );
read_6(S,C, S, C, {S, N2}pk(C) );
claim_7(C, Secret, N2);
claim_9(C, Niagree);
claim_10(C, Nisynch);
}
role AS
{
var N1,N3: Nonce;
read_1(C,AS, C, S, N1 );
send_2(AS,C, AS, {AS, C, N1, pk(S)}sk(AS) );
read_4(S,AS, S, C, N3 );
send_5(AS,S, AS, {AS, S, N3, pk(C)}sk(AS) );
}
role S
{
const N3: Nonce;
var N2: Nonce;
var T: TimeStamp;
var L: LifeTime;
var ni: Nonce;
const nr: Nonce;
read_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) );
send_4(S,AS, S, C, N3 );
read_5(AS,S, AS, {AS, S, N3, pk(C)}sk(AS) );
send_6(S,C, S, C, {S, N2}pk(C) );
claim_8(S, Secret, N2);
claim_11(S, Niagree);
claim_12(S, Nisynch);
}
}
const Al,Bo,Eve: Agent;
untrusted Eve;
const ne: Nonce;
compromised sk(Eve);
run spliceAS.C(Agent,Agent,Agent);
run spliceAS.AS(Agent,Agent,Agent);
run spliceAS.S(Agent,Agent,Agent);

95
spdl/misc/tls-paulson.cpp
View File

@ -1,95 +0,0 @@
/*
* This is a model of the TLS version as modeled by Paulson
*
* The .cpp file cannot be fed into scyther directly; rather, one needs
* to type:
*
* cpp tls-paulson.cpp >tls-paulson.spdl
*
* in order to generate a valid spdl file for scyther.
*
* This allows for macro expansion, as seen in the next part.
*
*/
#define CERT(a) { a,pk(a) }sk(Terence)
#define MSG a,na,sid,pa,pb,nb,sid,pb,CERT(a),CERT(b),{pms}pk(b)
#define M hash(pms,na,nb)
#define F hash(M,MSG)
#define CLIENTK hash(sid,M,na,pa,a,nb,pb,b,false)
#define SERVERK hash(sid,M,na,pa,a,nb,pb,b,true)
usertype Params, Bool, SessionID;
const pk,hash: Function;
secret sk,unhash: Function;
inversekeys(pk,sk);
inversekeys(hash,unhash);
const pa,pb: Params;
const Terence: Agent;
const false,true: Bool;
protocol tlspaulson(a,b)
{
role a
{
const na: Nonce;
const sid: SessionID;
const pms: Nonce;
var nb: Nonce;
var pb: Params;
send_1( a,b, a,na,sid,pa );
read_2( b,a, nb,sid,pb );
read_3( b,a, CERT(b) );
send_4( a,b, CERT(a) );
send_5( a,b, { pms }pk(b) );
send_6( a,b, { hash(nb,b,pms) }sk(a) );
send_7( a,b, { F }CLIENTK );
read_8( b,a, { F }SERVERK );
claim_9a(a, Secret, SERVERK);
claim_9b(a, Secret, CLIENTK);
}
role b
{
var na: Nonce;
var sid: SessionID;
var pms: Nonce;
const nb: Nonce;
const pb: Params;
read_1( a,b, a,na,sid,pa );
send_2( b,a, nb,sid,pb );
send_3( b,a, CERT(b) );
read_4( a,b, CERT(a) );
read_5( a,b, { pms }pk(b) );
read_6( a,b, { hash(nb,b,pms) }sk(a) );
read_7( a,b, { F }CLIENTK );
send_8( b,a, { F }SERVERK );
claim_10a(b, Secret, SERVERK);
claim_10b(b, Secret, CLIENTK);
}
}
const Alice, Bob, Eve: Agent;
untrusted Eve;
compromised sk(Eve);
const ne: Nonce;
const side: SessionID;
const pe: Params;
run tlspaulson.a(Agent,Agent);
run tlspaulson.b(Agent,Agent);
run tlspaulson.a(Agent,Agent);
run tlspaulson.b(Agent,Agent);
run tlspaulson.a(Agent,Agent);
run tlspaulson.b(Agent,Agent);
run tlspaulson.a(Agent,Agent);
run tlspaulson.b(Agent,Agent);

56
spdl/misc/tmn-Gijs.spdl
View File

@ -1,56 +0,0 @@
usertype Key;
const pk: Function;
secret sk: Function;
inversekeys(pk,sk);
protocol tmn(A,B,S)
{
role A
{
const Ka: Key;
var Kb: Key;
send_1(A,S, B,{Ka}pk(S) );
read_4(S,A, B,{Kb}Ka );
#claim_5(A,Secret,Ka);
#claim_8(A,Secret,Kb);
}
role B
{
const Kb: Key;
read_2(S,B, A );
send_3(B,S, A, { Kb }pk(S) );
claim_6(B,Secret,Kb);
}
role S
{
var Ka,Kb: Key;
read_1(A,S, B,{Ka}pk(S) );
send_2(S,B, A );
read_3(B,S, A, { Kb }pk(S) );
send_4(S,A, B,{Kb}Ka );
#claim_7(S,Secret,Ka);
}
}
const Alice,Bob,Eve,Simon: Agent;
const Ke: Key;
untrusted Eve;
compromised sk(Eve);
# Scenario to recreate an attack in SPORE
run tmn.B (Alice,Bob,Simon);
run tmn.S (Alice,Bob,Simon);

56
spdl/misc/tmn.spdl
View File

@ -1,56 +0,0 @@
usertype Key;
const pk: Function;
secret sk: Function;
inversekeys(pk,sk);
protocol tmn(A,B,S)
{
role A
{
const Ka: Key;
var Kb: Key;
send_1(A,S, B,{Ka}pk(S) );
read_4(S,A, B,{Kb}Ka );
claim_5(A,Secret,Ka);
claim_8(A,Secret,Kb);
}
role B
{
const Kb: Key;
read_2(S,B, A );
send_3(B,S, A, { Kb }pk(S) );
claim_6(B,Secret,Kb);
}
role S
{
var Ka,Kb: Key;
read_1(A,S, B,{Ka}pk(S) );
send_2(S,B, A );
read_3(B,S, A, { Kb }pk(S) );
send_4(S,A, B,{Kb}Ka );
claim_7(S,Secret,Ka);
}
}
const Alice,Bob,Eve,Simon: Agent;
untrusted Eve;
compromised sk(Eve);
run tmn.A (Agent,Agent,Simon);
run tmn.A (Agent,Agent,Simon);
run tmn.B (Agent,Agent,Simon);
run tmn.B (Agent,Agent,Simon);
run tmn.S (Agent,Agent,Simon);
run tmn.S (Agent,Agent,Simon);

69
spdl/misc/unknown2.spdl
View File

@ -1,69 +0,0 @@
usertype SessionKey;
secret k: Function;
protocol unknown2(I,R,S)
{
role I
{
const ni: Nonce;
var nr: Nonce;
var kir: SessionKey;
var T;
send_1(I,R, ni );
read_3(S,I, { I,R,kir,ni,nr }k(I,S), T );
send_4(I,R, T, {nr}kir );
claim_i1(I,Nisynch);
claim_i2(I,Niagree);
claim_i3(I,Secret, kir);
}
role R
{
const nr: Nonce;
var ni: Nonce;
var kir: SessionKey;
read_1(I,R, ni );
send_2(R,S, { I,R,ni,nr }k(R,S) );
read_4(I,R, { I,R,kir,ni,nr }k(R,S), {nr}kir );
claim_r1(R,Nisynch);
claim_r2(R,Niagree);
claim_r3(R,Secret, kir);
}
role S
{
const kir: SessionKey;
var ni,nr: Nonce;
read_2(R,S, { I,R,ni,nr }k(R,S) );
send_3(S,I, { I,R,kir,ni,nr }k(I,S), { I,R,kir,ni,nr }k(R,S) );
/*
claim_s1(S,Nisynch);
claim_s2(S,Niagree);
claim_s3(S,Secret, 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);
run unknown2.I(Agent,Agent,Agent);
run unknown2.R(Agent,Agent,Agent);
run unknown2.S(Agent,Agent,Agent);
run unknown2.R(Agent,Agent,Agent);
run unknown2.I(Agent,Agent,Agent);
run unknown2.S(Agent,Agent,Agent);

48
spdl/misc/wmf-brutus.spdl
View File

@ -1,48 +0,0 @@
usertype SesKey, Server;
secret const k : Function;
/* Version from the Brutus reports
*/
protocol wmfbrutus(A,B,S)
{
role A
{
const kab : SesKey;
send_1(A,S, A, { B,kab }k(A,S) );
}
role B
{
var kab : SesKey;
read_2(S,B, { A, kab }k(B,S) );
claim_3(B, Secret,kab);
}
role S
{
var kab : SesKey;
read_1(A,S, A, { B,kab }k(A,S) );
send_2(S,B, { A, kab }k(B,S) );
}
}
const Alice, Bob, Eve: Agent;
const Simon: Server;
untrusted Eve;
compromised k(Eve,Simon);
run wmfbrutus.A(Agent, Agent, Simon);
run wmfbrutus.B(Agent, Agent, Simon);
run wmfbrutus.A(Agent, Agent, Simon);
run wmfbrutus.B(Agent, Agent, Simon);
run wmfbrutus.A(Agent, Agent, Simon);
run wmfbrutus.B(Agent, Agent, Simon);
run wmfbrutus.S(Agent, Agent, Simon);

Some files were not shown because too many files have changed in this diff Show More