Added a new subdirectory with protocols for MPA experiments.
This commit is contained in:
Cas Cremers
parent
96e52a3724
commit
fac14fc950
39
gui/Protocols/MultiProtocolAttacks/BKE.spdl
Normal file
39
gui/Protocols/MultiProtocolAttacks/BKE.spdl
Normal file
@ -0,0 +1,39 @@
|
|||||||
|
/*
|
||||||
|
Bilateral Key Exchange with Public Key protocol (BKEPK)
|
||||||
|
*/
|
||||||
|
|
||||||
|
usertype SessionKey;
|
||||||
|
|
||||||
|
hashfunction hash;
|
||||||
|
|
||||||
|
protocol bke(I,R)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh ni: Nonce;
|
||||||
|
var nr: Nonce;
|
||||||
|
var kir: SessionKey;
|
||||||
|
|
||||||
|
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;
|
||||||
|
fresh nr: Nonce;
|
||||||
|
fresh kir: SessionKey;
|
||||||
|
|
||||||
|
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 );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
73
gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl
Normal file
73
gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl
Normal file
@ -0,0 +1,73 @@
|
|||||||
|
# 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;
|
||||||
|
const Fresh: 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(I,R)
|
||||||
|
{
|
||||||
|
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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;
|
||||||
|
fresh nr: Nonce;
|
||||||
|
fresh 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;
|
||||||
|
|
||||||
63
gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl
Normal file
63
gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl
Normal file
@ -0,0 +1,63 @@
|
|||||||
|
# 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;
|
||||||
|
const Fresh: Function;
|
||||||
|
const Compromised: Function;
|
||||||
|
|
||||||
|
protocol andrew-Ban(I,R)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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_I5(I,Empty, (Fresh,kir));
|
||||||
|
}
|
||||||
|
|
||||||
|
role R
|
||||||
|
{
|
||||||
|
var ni: Nonce;
|
||||||
|
fresh nr,nr2: Nonce;
|
||||||
|
fresh 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_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);
|
||||||
|
|
||||||
70
gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl
Normal file
70
gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl
Normal file
@ -0,0 +1,70 @@
|
|||||||
|
# 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;
|
||||||
|
const Fresh: Function;
|
||||||
|
const Compromised: Function;
|
||||||
|
|
||||||
|
protocol andrew-LoweBan(I,R)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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;
|
||||||
|
fresh nr: Nonce;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
70
gui/Protocols/MultiProtocolAttacks/boyd.spdl
Normal file
70
gui/Protocols/MultiProtocolAttacks/boyd.spdl
Normal file
@ -0,0 +1,70 @@
|
|||||||
|
usertype Sessionkey;
|
||||||
|
usertype Macseed;
|
||||||
|
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
|
||||||
|
{
|
||||||
|
fresh 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) );
|
||||||
|
}
|
||||||
|
|
||||||
|
role R
|
||||||
|
{
|
||||||
|
var ni: Nonce;
|
||||||
|
fresh 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));
|
||||||
|
}
|
||||||
|
|
||||||
|
role S
|
||||||
|
{
|
||||||
|
var ni,nr: Nonce;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
45
gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl
Normal file
45
gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl
Normal file
@ -0,0 +1,45 @@
|
|||||||
|
# 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
|
||||||
|
#
|
||||||
|
|
||||||
|
protocol ccitt509-ban3(I,R)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
74
gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl
Normal file
74
gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl
Normal file
@ -0,0 +1,74 @@
|
|||||||
|
# Lowe modified Denning-Sacco shared key
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/denningSaccoLowe.html
|
||||||
|
#
|
||||||
|
# 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;
|
||||||
|
usertype PseudoFunction;
|
||||||
|
const dec: PseudoFunction;
|
||||||
|
const Fresh: Function;
|
||||||
|
const Compromised: Function;
|
||||||
|
|
||||||
|
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;
|
||||||
|
fresh 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;
|
||||||
|
fresh Kir: SessionKey;
|
||||||
|
fresh T: TimeStamp;
|
||||||
|
|
||||||
|
read_1(I,S, I,R );
|
||||||
|
send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
|
||||||
|
claim_x(S, Secret, Kir);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
const Alice,Bob,Simon,Eve: Agent;
|
||||||
|
|
||||||
|
untrusted Eve;
|
||||||
|
const kee: SessionKey;
|
||||||
|
const tee: TimeStamp;
|
||||||
|
compromised k(Eve,Simon);
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
62
gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl
Normal file
62
gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl
Normal file
@ -0,0 +1,62 @@
|
|||||||
|
# Denning-Sacco shared key
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/denningSacco.html
|
||||||
|
#
|
||||||
|
|
||||||
|
usertype Key;
|
||||||
|
usertype SessionKey;
|
||||||
|
usertype TimeStamp;
|
||||||
|
usertype ExpiredTimeStamp;
|
||||||
|
const Fresh: Function;
|
||||||
|
const Compromised: Function;
|
||||||
|
|
||||||
|
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;
|
||||||
|
fresh Kir: SessionKey;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
80
gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl
Normal file
80
gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl
Normal file
@ -0,0 +1,80 @@
|
|||||||
|
usertype Sessionkey;
|
||||||
|
usertype Keypart;
|
||||||
|
hashfunction f;
|
||||||
|
|
||||||
|
/*
|
||||||
|
* Gong nonce based alternative
|
||||||
|
*
|
||||||
|
* Boyd & Mathuria: Protocols for authentication and key establishment
|
||||||
|
* (2003) p. 101
|
||||||
|
*/
|
||||||
|
|
||||||
|
protocol gongnonceb(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh ni: Nonce;
|
||||||
|
var nr: Nonce;
|
||||||
|
fresh 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;
|
||||||
|
fresh nr: Nonce;
|
||||||
|
fresh 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);
|
||||||
71
gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl
Normal file
71
gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl
Normal file
@ -0,0 +1,71 @@
|
|||||||
|
usertype Sessionkey;
|
||||||
|
usertype Keypart;
|
||||||
|
|
||||||
|
protocol gongnonce(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh ni: Nonce;
|
||||||
|
var nr: Nonce;
|
||||||
|
fresh 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;
|
||||||
|
fresh nr: Nonce;
|
||||||
|
fresh 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);
|
||||||
62
gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl
Normal file
62
gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl
Normal file
@ -0,0 +1,62 @@
|
|||||||
|
usertype Sessionkey;
|
||||||
|
usertype Ticket;
|
||||||
|
|
||||||
|
protocol isoiec11770213(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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;
|
||||||
|
fresh nr: Nonce;
|
||||||
|
fresh 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);
|
||||||
69
gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl
Normal file
69
gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl
Normal file
@ -0,0 +1,69 @@
|
|||||||
|
# Kao Chow Authentication v.2
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/kaoChow2.html
|
||||||
|
#
|
||||||
|
|
||||||
|
usertype SessionKey;
|
||||||
|
const Fresh: Function;
|
||||||
|
const Compromised: Function;
|
||||||
|
|
||||||
|
protocol kaochow-2(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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;
|
||||||
|
fresh 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;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
73
gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl
Normal file
73
gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl
Normal file
@ -0,0 +1,73 @@
|
|||||||
|
# Kao Chow Authentication v.3
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/kaoChow3.html
|
||||||
|
#
|
||||||
|
|
||||||
|
usertype SessionKey;
|
||||||
|
usertype ExpiredTimeStamp;
|
||||||
|
usertype TimeStamp;
|
||||||
|
const Fresh: Function;
|
||||||
|
const Compromised: Function;
|
||||||
|
|
||||||
|
protocol kaochow-3(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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;
|
||||||
|
fresh nr: Nonce;
|
||||||
|
var kir,kt: SessionKey;
|
||||||
|
var T: Ticket;
|
||||||
|
fresh 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;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
69
gui/Protocols/MultiProtocolAttacks/kaochow.spdl
Normal file
69
gui/Protocols/MultiProtocolAttacks/kaochow.spdl
Normal file
@ -0,0 +1,69 @@
|
|||||||
|
# Kao Chow Authentication v.1
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/kaoChow1.html
|
||||||
|
#
|
||||||
|
|
||||||
|
usertype SessionKey;
|
||||||
|
const Fresh: Function;
|
||||||
|
const Compromised: Function;
|
||||||
|
|
||||||
|
protocol kaochow(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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;
|
||||||
|
fresh 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;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
@ -0,0 +1,73 @@
|
|||||||
|
# Amended Needham Schroeder Symmetric Key
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/nssk_amended.html
|
||||||
|
#
|
||||||
|
#
|
||||||
|
# Note:
|
||||||
|
# According to SPORE there are no attacks on this protocol, scyther
|
||||||
|
# finds one however. This has to be investigated further.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
# 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(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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
|
||||||
|
{
|
||||||
|
fresh 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;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
|
|
||||||
62
gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl
Normal file
62
gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl
Normal file
@ -0,0 +1,62 @@
|
|||||||
|
# Needham Schroeder Symmetric Key
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/nssk.html
|
||||||
|
#
|
||||||
|
#
|
||||||
|
|
||||||
|
|
||||||
|
# Model dec that is invertible by inc
|
||||||
|
const dec,inc: Function;
|
||||||
|
inversekeys(dec,inc);
|
||||||
|
usertype SessionKey;
|
||||||
|
const Fresh: Function;
|
||||||
|
const Compromised: Function;
|
||||||
|
|
||||||
|
protocol needhamschroedersk(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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
|
||||||
|
{
|
||||||
|
fresh 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;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
5
gui/Protocols/MultiProtocolAttacks/new.txt
Normal file
5
gui/Protocols/MultiProtocolAttacks/new.txt
Normal file
@ -0,0 +1,5 @@
|
|||||||
|
denning-sacco-lowe.spdl
|
||||||
|
wmf.spdl
|
||||||
|
wmf-lowe.spdl
|
||||||
|
andrew-ban-concrete.spdl
|
||||||
|
yahalom-ban-paulson.spdl
|
||||||
41
gui/Protocols/MultiProtocolAttacks/ns3.spdl
Normal file
41
gui/Protocols/MultiProtocolAttacks/ns3.spdl
Normal file
@ -0,0 +1,41 @@
|
|||||||
|
/*
|
||||||
|
* Needham-Schroeder protocol
|
||||||
|
*/
|
||||||
|
|
||||||
|
// The protocol description
|
||||||
|
|
||||||
|
protocol ns3(I,R)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh ni: Nonce;
|
||||||
|
var nr: Nonce;
|
||||||
|
|
||||||
|
send_1(I,R, {ni,I}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,Alive);
|
||||||
|
claim_i4(I,Niagree);
|
||||||
|
claim_i5(I,Nisynch);
|
||||||
|
}
|
||||||
|
|
||||||
|
role R
|
||||||
|
{
|
||||||
|
var ni: Nonce;
|
||||||
|
fresh nr: Nonce;
|
||||||
|
|
||||||
|
read_1(I,R, {ni,I}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,Alive);
|
||||||
|
claim_r4(R,Niagree);
|
||||||
|
claim_r5(R,Nisynch);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
39
gui/Protocols/MultiProtocolAttacks/nsl3.spdl
Normal file
39
gui/Protocols/MultiProtocolAttacks/nsl3.spdl
Normal file
@ -0,0 +1,39 @@
|
|||||||
|
/*
|
||||||
|
* Needham-Schroeder-Lowe protocol
|
||||||
|
*/
|
||||||
|
|
||||||
|
// The protocol description
|
||||||
|
|
||||||
|
protocol nsl3(I,R)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh ni: Nonce;
|
||||||
|
var nr: Nonce;
|
||||||
|
|
||||||
|
send_1(I,R, {ni,I}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;
|
||||||
|
fresh nr: Nonce;
|
||||||
|
|
||||||
|
read_1(I,R, {ni,I}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);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
61
gui/Protocols/MultiProtocolAttacks/otwayrees.spdl
Normal file
61
gui/Protocols/MultiProtocolAttacks/otwayrees.spdl
Normal file
@ -0,0 +1,61 @@
|
|||||||
|
# Otway Rees
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/otwayRees.html
|
||||||
|
#
|
||||||
|
|
||||||
|
|
||||||
|
const Fresh: Function;
|
||||||
|
const Compromised: Function;
|
||||||
|
|
||||||
|
usertype String,SessionKey;
|
||||||
|
|
||||||
|
protocol otwayrees(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh Ni : Nonce;
|
||||||
|
fresh 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;
|
||||||
|
fresh 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;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
31
gui/Protocols/MultiProtocolAttacks/soph.spdl
Normal file
31
gui/Protocols/MultiProtocolAttacks/soph.spdl
Normal file
@ -0,0 +1,31 @@
|
|||||||
|
|
||||||
|
protocol soph(I,R)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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);
|
||||||
72
gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl
Normal file
72
gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl
Normal file
@ -0,0 +1,72 @@
|
|||||||
|
# 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 inc,dec: Function;
|
||||||
|
inversekeys (inc,dec);
|
||||||
|
|
||||||
|
protocol spliceAS-CJ(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh N1,N2: Nonce;
|
||||||
|
fresh T: TimeStamp;
|
||||||
|
fresh 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
|
||||||
|
{
|
||||||
|
fresh N3: Nonce;
|
||||||
|
var N2: Nonce;
|
||||||
|
var T: TimeStamp;
|
||||||
|
var L: LifeTime;
|
||||||
|
|
||||||
|
var ni: Nonce;
|
||||||
|
fresh nr: Nonce;
|
||||||
|
|
||||||
|
read_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) );
|
||||||
|
send_4(R,S, R, I, N3 );
|
||||||
|
read_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
|
||||||
|
send_6(R,I, R, I, {{N2}inc}pk(I) );
|
||||||
|
|
||||||
|
claim_8(R, Secret, N2);
|
||||||
|
claim_11(R, Niagree);
|
||||||
|
claim_12(R, Nisynch);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
const Alice,Bob,Simon,Eve: Agent;
|
||||||
|
|
||||||
|
untrusted Eve;
|
||||||
|
const ne: Nonce;
|
||||||
|
compromised sk(Eve);
|
||||||
|
|
||||||
72
gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl
Normal file
72
gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl
Normal file
@ -0,0 +1,72 @@
|
|||||||
|
# Hwang and Chen Modified SPLICE/AS
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/spliceas2.html
|
||||||
|
#
|
||||||
|
|
||||||
|
|
||||||
|
usertype TimeStamp, LifeTime;
|
||||||
|
|
||||||
|
const pk: Function;
|
||||||
|
secret sk: Function;
|
||||||
|
inversekeys (pk,sk);
|
||||||
|
const inc,dec: Function;
|
||||||
|
inversekeys (inc,dec);
|
||||||
|
|
||||||
|
protocol spliceAS-HC(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh N1,N2: Nonce;
|
||||||
|
fresh T: TimeStamp;
|
||||||
|
fresh 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
|
||||||
|
{
|
||||||
|
fresh N3: Nonce;
|
||||||
|
var N2: Nonce;
|
||||||
|
var T: TimeStamp;
|
||||||
|
var L: LifeTime;
|
||||||
|
|
||||||
|
var ni: Nonce;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
72
gui/Protocols/MultiProtocolAttacks/splice-as.spdl
Normal file
72
gui/Protocols/MultiProtocolAttacks/splice-as.spdl
Normal file
@ -0,0 +1,72 @@
|
|||||||
|
# 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 inc,dec: Function;
|
||||||
|
inversekeys (inc,dec);
|
||||||
|
|
||||||
|
protocol spliceAS(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh N1,N2: Nonce;
|
||||||
|
fresh T: TimeStamp;
|
||||||
|
fresh 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
|
||||||
|
{
|
||||||
|
fresh N3: Nonce;
|
||||||
|
var N2: Nonce;
|
||||||
|
var T: TimeStamp;
|
||||||
|
var L: LifeTime;
|
||||||
|
|
||||||
|
var ni: Nonce;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
60
gui/Protocols/MultiProtocolAttacks/tmn.spdl
Normal file
60
gui/Protocols/MultiProtocolAttacks/tmn.spdl
Normal file
@ -0,0 +1,60 @@
|
|||||||
|
# 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 Fresh: Function;
|
||||||
|
const Compromised: Function;
|
||||||
|
|
||||||
|
protocol tmn(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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
|
||||||
|
{
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
47
gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl
Normal file
47
gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl
Normal file
@ -0,0 +1,47 @@
|
|||||||
|
usertype SesKey, Server;
|
||||||
|
|
||||||
|
/* Version from the Brutus reports
|
||||||
|
*/
|
||||||
|
|
||||||
|
protocol wmfbrutus(A,B,S)
|
||||||
|
{
|
||||||
|
role A
|
||||||
|
{
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
73
gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl
Normal file
73
gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl
Normal file
@ -0,0 +1,73 @@
|
|||||||
|
# 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;
|
||||||
|
|
||||||
|
protocol wmf-Lowe(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh Kir: SessionKey;
|
||||||
|
fresh 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;
|
||||||
|
fresh 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;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
64
gui/Protocols/MultiProtocolAttacks/wmf.spdl
Normal file
64
gui/Protocols/MultiProtocolAttacks/wmf.spdl
Normal file
@ -0,0 +1,64 @@
|
|||||||
|
# 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;
|
||||||
|
|
||||||
|
const Fresh: Function;
|
||||||
|
const Compromised: Function;
|
||||||
|
|
||||||
|
protocol wmf(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh Kir: SessionKey;
|
||||||
|
fresh 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;
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
49
gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl
Normal file
49
gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl
Normal file
@ -0,0 +1,49 @@
|
|||||||
|
# Woo and Lam Pi f
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/wooLamPif.html
|
||||||
|
#
|
||||||
|
|
||||||
|
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
|
||||||
|
{
|
||||||
|
fresh 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);
|
||||||
|
|
||||||
64
gui/Protocols/MultiProtocolAttacks/woo-lam.spdl
Normal file
64
gui/Protocols/MultiProtocolAttacks/woo-lam.spdl
Normal file
@ -0,0 +1,64 @@
|
|||||||
|
# Woo and Lam Mutual Authentication
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/wooLamMutual.html
|
||||||
|
#
|
||||||
|
|
||||||
|
|
||||||
|
usertype SessionKey;
|
||||||
|
|
||||||
|
const Fresh: Function;
|
||||||
|
const Compromised: Function;
|
||||||
|
|
||||||
|
protocol woolam(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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
|
||||||
|
{
|
||||||
|
fresh 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
|
||||||
|
{
|
||||||
|
fresh 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));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
@ -0,0 +1,52 @@
|
|||||||
|
// BAN modified version of the yahalom protocol
|
||||||
|
//
|
||||||
|
// Modeled as version in Paulson's paper:
|
||||||
|
// "Relations Between Secrets: Two Formal Analyses of the Yahalom
|
||||||
|
// Protocol"
|
||||||
|
//
|
||||||
|
// Modified (improved) version from page 16.
|
||||||
|
|
||||||
|
usertype Server;
|
||||||
|
usertype SessionKey;
|
||||||
|
|
||||||
|
const a,b,c : Agent;
|
||||||
|
const s : Server;
|
||||||
|
|
||||||
|
protocol yahalom-BAN-Paulson-modified(A,B,S)
|
||||||
|
{
|
||||||
|
role A
|
||||||
|
{
|
||||||
|
fresh na: Nonce;
|
||||||
|
var nb: Nonce;
|
||||||
|
var ticket: Ticket;
|
||||||
|
var kab: SessionKey;
|
||||||
|
|
||||||
|
send_1(A,B, A,na);
|
||||||
|
read_3(S,A, nb, {B,kab,na}k(A,S), ticket );
|
||||||
|
send_4(A,B, ticket, {nb}kab );
|
||||||
|
claim_5(A, Secret,kab);
|
||||||
|
}
|
||||||
|
|
||||||
|
role B
|
||||||
|
{
|
||||||
|
fresh nb: Nonce;
|
||||||
|
var na: Nonce;
|
||||||
|
var ticket: Ticket;
|
||||||
|
var kab: SessionKey;
|
||||||
|
|
||||||
|
read_1(A,B, A,na);
|
||||||
|
send_2(B,S, B, nb, {A,na}k(B,S) );
|
||||||
|
read_4(A,B, {A,B,kab,nb}k(B,S) , {nb}kab );
|
||||||
|
claim_6(B, Secret,kab);
|
||||||
|
}
|
||||||
|
|
||||||
|
role S
|
||||||
|
{
|
||||||
|
fresh kab: SessionKey;
|
||||||
|
var na,nb: Nonce;
|
||||||
|
|
||||||
|
read_2(B,S, B, nb, {A,na}k(B,S) );
|
||||||
|
send_3(S,A, nb, {B,kab,na}k(A,S), {A,B,kab,nb}k(B,S) );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
50
gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl
Normal file
50
gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl
Normal file
@ -0,0 +1,50 @@
|
|||||||
|
// BAN modified version of the yahalom protocol
|
||||||
|
//
|
||||||
|
// Modeled as version in Paulson's paper:
|
||||||
|
// "Relations Between Secrets: Two Formal Analyses of the Yahalom
|
||||||
|
// Protocol"
|
||||||
|
|
||||||
|
usertype Server;
|
||||||
|
usertype SessionKey;
|
||||||
|
|
||||||
|
const a,b,c : Agent;
|
||||||
|
const s : Server;
|
||||||
|
|
||||||
|
protocol yahalom-BAN-Paulson(A,B,S)
|
||||||
|
{
|
||||||
|
role A
|
||||||
|
{
|
||||||
|
fresh na: Nonce;
|
||||||
|
var nb: Nonce;
|
||||||
|
var ticket: Ticket;
|
||||||
|
var kab: SessionKey;
|
||||||
|
|
||||||
|
send_1(A,B, A,na);
|
||||||
|
read_3(S,A, {B,kab,na,nb}k(A,S), ticket );
|
||||||
|
send_4(A,B, ticket, {nb}kab );
|
||||||
|
claim_5(A, Secret,kab);
|
||||||
|
}
|
||||||
|
|
||||||
|
role B
|
||||||
|
{
|
||||||
|
fresh nb: Nonce;
|
||||||
|
var na: Nonce;
|
||||||
|
var ticket: Ticket;
|
||||||
|
var kab: SessionKey;
|
||||||
|
|
||||||
|
read_1(A,B, A,na);
|
||||||
|
send_2(B,S, B, {A,na,nb}k(B,S) );
|
||||||
|
read_4(A,B, {A,kab}k(B,S) , {nb}kab );
|
||||||
|
claim_6(B, Secret,kab);
|
||||||
|
}
|
||||||
|
|
||||||
|
role S
|
||||||
|
{
|
||||||
|
fresh kab: SessionKey;
|
||||||
|
var na,nb: Nonce;
|
||||||
|
|
||||||
|
read_2(B,S, B, {A,na,nb}k(B,S) );
|
||||||
|
send_3(S,A, {B,kab,na,nb}k(A,S), {A,kab}k(B,S) );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
56
gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl
Normal file
56
gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl
Normal file
@ -0,0 +1,56 @@
|
|||||||
|
# BAN simplified version of Yahalom
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/yahalomBAN.html
|
||||||
|
#
|
||||||
|
|
||||||
|
usertype SessionKey;
|
||||||
|
const Fresh: Function;
|
||||||
|
const Compromised: Function;
|
||||||
|
|
||||||
|
protocol yahalom-BAN(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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
|
||||||
|
{
|
||||||
|
fresh 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
|
||||||
|
{
|
||||||
|
fresh Kir: SessionKey;
|
||||||
|
var Ni,Nr: Nonce;
|
||||||
|
|
||||||
|
read_2(R,S, R, Nr, {I,Ni}k(R,S) );
|
||||||
|
send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,Kir,Nr}k(R,S) );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
const Alice,Bob,Charlie,David: Agent;
|
||||||
|
|
||||||
54
gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl
Normal file
54
gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl
Normal file
@ -0,0 +1,54 @@
|
|||||||
|
# Lowe's modified version of Yahalom
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/yahalomLowe.html
|
||||||
|
#
|
||||||
|
#
|
||||||
|
|
||||||
|
usertype SessionKey;
|
||||||
|
|
||||||
|
|
||||||
|
protocol yahalom-Lowe(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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
|
||||||
|
{
|
||||||
|
fresh 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
|
||||||
|
{
|
||||||
|
fresh 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;
|
||||||
|
|
||||||
59
gui/Protocols/MultiProtocolAttacks/yahalom.spdl
Normal file
59
gui/Protocols/MultiProtocolAttacks/yahalom.spdl
Normal file
@ -0,0 +1,59 @@
|
|||||||
|
# Yahalom
|
||||||
|
#
|
||||||
|
# Modelled after the description in the SPORE library
|
||||||
|
# http://www.lsv.ens-cachan.fr/spore/yahalom.html
|
||||||
|
#
|
||||||
|
#
|
||||||
|
|
||||||
|
usertype SessionKey;
|
||||||
|
|
||||||
|
protocol yahalom(I,R,S)
|
||||||
|
{
|
||||||
|
role I
|
||||||
|
{
|
||||||
|
fresh 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);
|
||||||
|
}
|
||||||
|
|
||||||
|
role R
|
||||||
|
{
|
||||||
|
fresh 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);
|
||||||
|
}
|
||||||
|
|
||||||
|
role S
|
||||||
|
{
|
||||||
|
fresh 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) );
|
||||||
|
|
||||||
|
claim(S, Secret, Ni);
|
||||||
|
claim(S, Secret, Nr);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
const Alice,Bob,Simon : Agent;
|
||||||
|
|
||||||
|
const Eve: Agent;
|
||||||
|
untrusted Eve;
|
||||||
|
|
||||||
|
compromised k(Eve,Simon);
|
||||||
|
|
||||||
Loading…
Reference in New Issue
Block a user