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

- Created a directory to hold spdl files of all protocols in SPORE

Browse Source 
- Import Andrew secure RPC and derived protocols
This commit is contained in:
gijs 2005-04-29 10:50:53 +00:00
parent 38f6f42351
commit 0b22c4a4bb
4 changed files with 279 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -0,0 +1,70 @@
# 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)
# So it is possile that certain attacks that use this property are not found
#
# Note:
# The attack mentioned in SPORE is not found because of the property in the
# previous note
#
# 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;
protocol andrewConcrete(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_4(I,Secret,kir);
claim_5(I,Nisynch);
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_7(R,Secret,kir);
claim_8(R,Nisynch);
}
}
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 andrewConcrete.I(Agent,Agent);
run andrewConcrete.R(Agent,Agent);
run andrewConcrete.I(Agent,Agent);
run andrewConcrete.R(Agent,Agent);

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

@ -0,0 +1,66 @@
# 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;
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);

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

@ -0,0 +1,71 @@
# 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;
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,R}k(I,R) );
send_3(I,R, {ni}kir );
claim_5(I,Nisynch);
claim_6(I,Secret, 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_8(R,Nisynch);
claim_9(R,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 andrewLoweBan.I(Agent,Agent);
run andrewLoweBan.R(Agent,Agent);
run andrewLoweBan.I(Agent,Agent);
run andrewLoweBan.R(Agent,Agent);

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

@ -0,0 +1,72 @@
# 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;
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_5(I,Secret,kir);
claim_6(I,Nisynch);
}
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_7(R,Secret,kir);
claim_8(R,Nisynch);
}
}
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);