- Added a few protocols to the list.

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);
+	}
+}
+
+

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

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);
+	}
+}

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);
+	}
+}

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

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;
 

spdl/yahalom-lowe.spdl

@@ -1,4 +1,7 @@
-// Yahalom protocol
+/*
+ * Yahalom Lowe
+ * As in Sjouke's list
+ */
 
 usertype Sessionkey;
 

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);
+