- New version of the protocol after communication with Anupam Datta.

spdl/misc/tls-HSDDM05-2.cpp

@@ -0,0 +1,84 @@
+/*
+ * This is an improved model of a version of the TLS protocol as modeled by
+ * He,Sundararajan,Datta,Derek and Mitchell in the paper: "A modular
+ * correctness proof of IEEE 802.11i and TLS".
+ *
+ * Modeled by: Cas Cremers
+ *
+ * The original model was broken: the secret was not part of the
+ * handshake, and the handshakes were not hashed. After an e-mail
+ * exchange with Anupam Datta this was cleared up.
+ *
+ * The .cpp file cannot be fed into scyther directly; rather, one needs
+ * to type: (for *nix type systems with cpp)
+ *
+ * 	cpp tls-HSDDM05-2.cpp >tls-HSDDM05-2.spdl
+ *
+ * in order to generate a valid spdl file for the Scyther.
+ *
+ * This allows for macro expansion, as seen in the next part, which is
+ * particularly useful for expanding the handshakes.
+ *
+ */
+#define CERT(a) { a,pk(a) }sk(Terence)
+#define msg1 X,Nx,pa
+#define msg2 Ny,pb,CERT(Y)
+#define handShake1 hash(msg1,msg2,msecret)
+#define msg3 CERT(X),{handShake1}sk(X),{msecret}pk(Y),hash(msecret,handShake1,clientstring)
+#define handShake2 hash(msg1,msg2,msg3)
+#define msg4 hash(msecret,handShake2,serverstring)
+
+
+/* below is just Scyther input and no further macro definitions */
+
+usertype Params, String;
+
+const pk,hash: Function;
+secret sk,unhash: Function;
+inversekeys(pk,sk);
+inversekeys(hash,unhash);
+
+const clientstring,serverstring: String;
+
+const Alice, Bob, Eve: Agent;
+const Terence: Agent;
+
+protocol tls-HSDDM05(X,Y)
+{
+	role X
+	{
+		const Nx: Nonce;
+		const msecret: Nonce;
+		const pa: Params;
+		var Ny: Nonce;
+		var pb: Params;
+
+		send_1( X,Y, msg1 );
+		read_2( Y,X, msg2 );
+		send_3( X,Y, msg3 );
+		read_4( Y,X, msg4 );
+
+		claim_X1( X, Secret, msecret );
+	}	
+	
+	role Y
+	{
+		var Nx: Nonce;
+		var msecret: Nonce;
+		var pa: Params;
+		const Ny: Nonce;
+		const pb: Params;
+
+		read_1( X,Y, msg1 );
+		send_2( Y,X, msg2 );
+		read_3( X,Y, msg3 );
+		send_4( Y,X, msg4 );
+
+		claim_Y1( Y, Secret, msecret );
+	}
+}
+
+
+untrusted Eve;
+compromised sk(Eve);
+

spdl/misc/tls-HSDDM05-2.spdl

@@ -0,0 +1,55 @@
+# 1 "tls-HSDDM05-2.cpp"
+# 1 "<built-in>"
+# 1 "<command line>"
+# 1 "tls-HSDDM05-2.cpp"
+# 34 "tls-HSDDM05-2.cpp"
+usertype Params, String;
+
+const pk,hash: Function;
+secret sk,unhash: Function;
+inversekeys(pk,sk);
+inversekeys(hash,unhash);
+
+const clientstring,serverstring: String;
+
+const Alice, Bob, Eve: Agent;
+const Terence: Agent;
+
+protocol tls-HSDDM05(X,Y)
+{
+ role X
+ {
+  const Nx: Nonce;
+  const msecret: Nonce;
+  const pa: Params;
+  var Ny: Nonce;
+  var pb: Params;
+
+  send_1( X,Y, X,Nx,pa );
+  read_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) );
+  send_3( X,Y, { X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring) );
+  read_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring)),serverstring) );
+
+  claim_X1( X, Secret, msecret );
+ }
+
+ role Y
+ {
+  var Nx: Nonce;
+  var msecret: Nonce;
+  var pa: Params;
+  const Ny: Nonce;
+  const pb: Params;
+
+  read_1( X,Y, X,Nx,pa );
+  send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) );
+  read_3( X,Y, { X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring) );
+  send_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring)),serverstring) );
+
+  claim_Y1( Y, Secret, msecret );
+ }
+}
+
+
+untrusted Eve;
+compromised sk(Eve);