From a3f9d0dc65c4b98c9b8605f4bec80bac4a9ac36b Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 14 Jan 2005 09:52:48 +0000 Subject: [PATCH] - Added a few protocols to the list. --- spdl/denning-sacco-shared.spdl | 74 +++++++++++++++++++++++++++++++ spdl/multiprotocoltest.py | 2 +- spdl/ns-symmetric-amended.spdl | 79 ++++++++++++++++++++++++++++++++++ spdl/ns-symmetric.spdl | 72 +++++++++++++++++++++++++++++++ spdl/protocol-list.txt | 4 ++ spdl/woolam-cmv.spdl | 4 ++ spdl/yahalom-lowe.spdl | 5 ++- spdl/yahalom-paulson.spdl | 63 +++++++++++++++++++++++++++ 8 files changed, 301 insertions(+), 2 deletions(-) create mode 100644 spdl/denning-sacco-shared.spdl create mode 100644 spdl/ns-symmetric-amended.spdl create mode 100644 spdl/ns-symmetric.spdl create mode 100644 spdl/yahalom-paulson.spdl diff --git a/spdl/denning-sacco-shared.spdl b/spdl/denning-sacco-shared.spdl new file mode 100644 index 0000000..ceb7422 --- /dev/null +++ b/spdl/denning-sacco-shared.spdl @@ -0,0 +1,74 @@ +/* +* 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 denningsaccoshared(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); + } +} + + diff --git a/spdl/multiprotocoltest.py b/spdl/multiprotocoltest.py index b7f675d..17c7c81 100755 --- a/spdl/multiprotocoltest.py +++ b/spdl/multiprotocoltest.py @@ -36,7 +36,7 @@ ScytherProgram = "../src/scyther" # Scyther parameters ScytherDefaults = "--summary" -ScytherMethods = "--match=1 --arachne" +ScytherMethods = "--match=0 --arachne" ScytherBounds = "--timer=300 --max-runs=5 --max-depth=25 --max-length=30" # Build a large part of the command line (for Scyther) already diff --git a/spdl/ns-symmetric-amended.spdl b/spdl/ns-symmetric-amended.spdl new file mode 100644 index 0000000..82c7421 --- /dev/null +++ b/spdl/ns-symmetric-amended.spdl @@ -0,0 +1,79 @@ +/* + * 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 nssymmetric(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); + } + + 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); + } +} diff --git a/spdl/ns-symmetric.spdl b/spdl/ns-symmetric.spdl new file mode 100644 index 0000000..0eb0793 --- /dev/null +++ b/spdl/ns-symmetric.spdl @@ -0,0 +1,72 @@ +/* + * 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); + } +} diff --git a/spdl/protocol-list.txt b/spdl/protocol-list.txt index 9deb48d..b395f33 100644 --- a/spdl/protocol-list.txt +++ b/spdl/protocol-list.txt @@ -15,6 +15,7 @@ broken1.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 @@ -22,6 +23,8 @@ 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 @@ -45,4 +48,5 @@ woolam-ce.spdl woolam-cmv.spdl yahalom-ban.spdl yahalom-lowe.spdl +yahalom-paulson.spdl yahalom.spdl diff --git a/spdl/woolam-cmv.spdl b/spdl/woolam-cmv.spdl index 26e032b..4eda364 100644 --- a/spdl/woolam-cmv.spdl +++ b/spdl/woolam-cmv.spdl @@ -1,3 +1,7 @@ +/* + * Woo-lam version from Spore, as it is in Sjouke's list + */ + usertype Server, SessionKey, Token, Ticket; secret k: Function; diff --git a/spdl/yahalom-lowe.spdl b/spdl/yahalom-lowe.spdl index 87ecc5e..f49aaed 100644 --- a/spdl/yahalom-lowe.spdl +++ b/spdl/yahalom-lowe.spdl @@ -1,4 +1,7 @@ -// Yahalom protocol +/* + * Yahalom Lowe + * As in Sjouke's list + */ usertype Sessionkey; diff --git a/spdl/yahalom-paulson.spdl b/spdl/yahalom-paulson.spdl new file mode 100644 index 0000000..641e85f --- /dev/null +++ b/spdl/yahalom-paulson.spdl @@ -0,0 +1,63 @@ +/* + * Yahalom Paulson-strengthened + * As in Sjouke's list + */ + +usertype Sessionkey, Ticket; + +const Alice,Bob,Simon,Eve : Agent; +secret k : Function; + +untrusted Eve; +compromised k(Eve,Simon); +const ne: Nonce; +const kee: Sessionkey; + +protocol yahalomlowe(I,R,S) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: Sessionkey; + var T: Ticket; + + 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_8(I, Secret,kir); + claim_9(I, Nisynch); + } + + role R + { + const nr: Nonce; + var ni: Nonce; + 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_10(R, Secret,kir); + claim_11(R, Nisynch); + } + + 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) ); + } +} + +run yahalomlowe.I(Agent,Agent,Simon); +run yahalomlowe.R(Agent,Agent,Simon); +run yahalomlowe.S(Agent,Agent,Simon); + +run yahalomlowe.I(Agent,Agent,Simon); +run yahalomlowe.R(Agent,Agent,Simon); +