Fixed protocol

secondcw/ag01598_6644818_1_1.spdl

@@ -1,7 +1,7 @@
 /* 
  * Coursework 2 PI protocol
 */
-
+usertype String;
 usertype Timestamp;
 usertype Sessionkey;
 
@@ -19,15 +19,15 @@ protocol protocolPI(Network, Application, Phone) {
 		var SesK: SessionKey;
 		var tl: Timestamp;
 
-		recv_keysPhone(Network, Phone, Mac({SesK, tl}k(Network, Phone)), {SesK, tl}k(Network, Phone));
+		recv_keysPhone(Network, Phone, {Mac(SesK, tl)}k(Network, Phone), {SesK, tl}k(Network, Phone));
 
-		var mApp: Nonce;
+		var mApp: String;
 
-		recv_1(Application,Phone, {mApp}k(SesK));
+		recv_1(Application,Phone, {mApp}SesK);
 
-		fresh mPhone: Nonce;
+		fresh mPhone: String;
 
-		send_2(Phone,Application, {mApp, mPhone}k(SesK));
+		send_2(Phone,Application, {mApp, mPhone}SesK);
 	}
 
 	/* Role S - Application
@@ -42,14 +42,14 @@ protocol protocolPI(Network, Application, Phone) {
 		var SesK: SessionKey;
 		var tl: Timestamp;
 
-		recv_keysApp(Network,Application, Mac({SesK, tl}k(Network, Application)), {SesK, tl}k(Network, Application));
+		recv_keysApp(Network,Application, {Mac(SesK, tl)}k(Network, Application), {SesK, tl}k(Network, Application));
 
-		fresh mApp: Nonce;
+		fresh mApp: String;
-		var mPhone: Nonce;
+		var mPhone: String;
 
-		send_1(Application,Phone, {mApp}k(SesK));
+		send_1(Application,Phone, {mApp}SesK);
 
-		recv_2(Phone,Application, {mApp, mPhone}k(SesK));
+		recv_2(Phone,Application, {mApp, mPhone}SesK);
 	}
 
 	/* Role N - Network
@@ -64,9 +64,9 @@ protocol protocolPI(Network, Application, Phone) {
 		fresh SesK: SessionKey;
 		fresh tl: Timestamp;
 
-		send_keysApp(Network,Application, Mac({SesK, tl}k(Network, Application)), {SesK, tl}k(Network, Application));
+		send_keysApp(Network,Application, {Mac(SesK, tl)}k(Network, Application), {SesK, tl}k(Network, Application));
 
-		send_keysPhone(Network,Phone, Mac({SesK, tl}k(Network, Phone)), {SesK, tl}k(Network, Phone));
+		send_keysPhone(Network,Phone, {Mac(SesK, tl)}k(Network, Phone), {SesK, tl}k(Network, Phone));
 	}
 
 	

secondcw/ag01598_6644818_1_2.spdl

@@ -19,17 +19,17 @@ protocol protocolPI(Network, Application, Phone) {
 		var SesK: SessionKey;
 		var tl: Timestamp;
 
-		recv_keysPhone(Network, Phone, Mac({SesK, tl}k(Network, Phone)), {SesK, tl}k(Network, Phone));
+		recv_keysPhone(Network, Phone, {Mac(SesK, tl)}k(Network, Phone), {SesK, tl}k(Network, Phone));
 
 		var mApp: String;
 
-		recv_1(Application,Phone, {mApp}k(SesK));
+		recv_1(Application,Phone, {mApp}SesK);
 
 		fresh mPhone: String;
 
 		claim_phone1(Phone, Running, Application, mApp);
 
-		send_2(Phone,Application, {mApp, mPhone}k(SesK));
+		send_2(Phone,Application, {mApp, mPhone}SesK);
 
 		claim_phone2(Phone, Secret, SesK);
 		claim_application1(Phone, Commit, Application, mApp);
@@ -49,16 +49,16 @@ protocol protocolPI(Network, Application, Phone) {
 		var SesK: SessionKey;
 		var tl: Timestamp;
 
-		recv_keysApp(Network,Application, Mac({SesK, tl}k(Network, Application)), {SesK, tl}k(Network, Application));
+		recv_keysApp(Network,Application, {Mac(SesK, tl)}k(Network, Application), {SesK, tl}k(Network, Application));
 
 		fresh mApp: String;
 		var mPhone: String;
 
 		claim_application1(Application, Running, Phone, mApp);
 
-		send_1(Application,Phone, {mApp}k(SesK));
+		send_1(Application,Phone, {mApp}SesK);
 
-		recv_2(Phone,Application, {mApp, mPhone}k(SesK));
+		recv_2(Phone,Application, {mApp, mPhone}SesK);
 
 		claim_application2(Application, Secret, SesK);
 		claim_phone1(Application, Commit, Phone, mApp);
@@ -80,14 +80,12 @@ protocol protocolPI(Network, Application, Phone) {
 		fresh tl: Timestamp;
 
 		claim_netwrok1(Network, Running, Application, SesK, tl);
-		send_keysApp(Network,Application, Mac({SesK, tl}k(Network, Application)), {SesK, tl}k(Network, Application));
+		send_keysApp(Network,Application, {Mac(SesK, tl)}k(Network, Application), {SesK, tl}k(Network, Application));
 
 		claim_network2(Network, Running, Phone, SesK, tl);
-		send_keysPhone(Network,Phone, Mac({SesK, tl}k(Network, Phone)), {SesK, tl}k(Network, Phone));
+		send_keysPhone(Network,Phone, {Mac(SesK, tl)}k(Network, Phone), {SesK, tl}k(Network, Phone));
 
 		claim_network3(Network, Secret, SesK);
-
-		claim_network4(Network, Nisynch);
 	}
 
 	

secondcw/ag01598_6644818_1_3.spdl

@@ -0,0 +1,113 @@
+/* 
+ * Coursework 2 PI protocol
+*/
+usertype String;
+usertype Timestamp;
+usertype Sessionkey;
+
+hashfunction H1;
+
+protocol protocolPI(Network, Application, Phone) {
+
+	/* Role R - Phone
+	 *
+	 * has keys k(N,R)
+	 *
+	 */
+	role Phone {
+
+		var SesK: SessionKey;
+		var tl: Timestamp;
+
+		var TApp: Ticket;
+
+		recv_keysPhone(Network,Phone, {H1(SesK, tl)}k(Network, Phone), {SesK, tl}k(Network, Phone), TApp);
+
+		var mApp: String;
+
+		var temp: Ticket;
+
+		recv_1(Application,Phone, {mApp, {Network, Application, Phone, tl}k(Network, Phone), Application, Phone }SesK);
+
+		fresh mPhone: String;
+
+		claim_phone1(Phone, Running, Application, mApp);
+
+		fresh nApp3: Nonce;
+
+		send_2(Phone,Application, {mApp, mPhone, TApp, nApp3}SesK);
+
+		recv_3(Application,Phone, {nApp3}SesK);
+
+		claim_phone2(Phone, Secret, SesK);
+		claim_application1(Phone, Commit, Application, mApp);
+		claim_network2(Phone, Commit, Network, SesK, tl);
+		claim_phone3(Phone, Nisynch);
+
+	}
+
+	/* Role S - Application
+	 *
+	 * has keys k(N,S)
+	 *
+	 */
+	role Application {
+
+		fresh nApp: Nonce;
+
+		send_refreshKeys(Application,Network, Application, Phone, nApp);
+
+		var SesK: SessionKey;
+		var tl: Timestamp;
+
+		var TPhone: Ticket;
+
+		recv_keysApp(Network,Application, {H1(SesK, tl)}k(Network, Application), {SesK, tl, nApp}k(Network, Application), TPhone);
+
+		fresh mApp: String;
+		var mPhone: String;
+
+		claim_application1(Application, Running, Phone, mApp);
+
+		send_1(Application,Phone, {mApp, TPhone, Application, Phone}SesK);
+
+		var nApp3: Nonce;
+
+		recv_2(Phone,Application, {mApp, mPhone, {Network, Application, Phone, tl}k(Network, Application), nApp3}SesK);
+
+		send_3(Application,Phone, {nApp3}SesK);
+
+		claim_application2(Application, Secret, SesK);
+		claim_phone1(Application, Commit, Phone, mApp);
+		claim_network1(Application, Commit, Network, SesK, tl);
+
+		claim_application3(Application, Nisynch);
+	}
+
+	/* Role N - Network
+	 *
+	 * has keys k(N,R) and k(N,S)
+	 *
+	 */
+	role Network {
+
+		var nApp: Nonce;
+
+		recv_refreshKeys(Application,Network, Application, Phone, nApp);
+
+		fresh SesK: SessionKey;
+		fresh tl: Timestamp;
+
+		claim_netwrok1(Network, Running, Application, SesK, tl);
+
+		send_keysApp(Network,Application, {H1(SesK, tl)}k(Network, Application), {SesK, tl, nApp}k(Network, Application), {Network, Application, Phone, tl}k(Network, Phone));
+
+		claim_network2(Network, Running, Phone, SesK, tl);
+		send_keysPhone(Network,Phone, {H1(SesK, tl)}k(Network, Phone), {SesK, tl}k(Network, Phone), {Network, Application, Phone, tl}k(Network, Application));
+
+		claim_network3(Network, Secret, SesK);
+	}
+
+	
+}
+

secondcw/cw/cw.tex

@@ -63,10 +63,12 @@
 
 		The Phone and the Application verify the Mac and then the phone sends a nonce to the phone and the phone answers back with a new nonce and the original nonce.
 
+		The Mac was modeled as a hashing function then encryption this was done this way because scyther does not have a way of creating a mac function with keys so the hashing is done first followed by the encrypted so that an attacker can not modify it.
+
 	\subsection*{1.2}
 		The file ag01598\_6644818\_1\_2.spdl contains the base model of $\text{protocol}\Pi$ and the claims.
 
-		I added non-injective synchronization(nisynch) to all the roles to guarantee that  all the roles, at least, some roles communicated as described by the protocol.
+		I added non-injective synchronization(nisynch) to the Phone and Network, at least, some roles communicated as described by the protocol.
 		I added a secret claim to SesK (Session key) to all roles, as the session key should be private.
  		Furthermore, I added Commit and Running claims between some roles to check for agreement between some variables:
 		\begin{itemize}
@@ -75,12 +77,10 @@
 			\item{Agreement between Application and Phone over the message and the message m}
 		\end{itemize}
 
-		There are 10 overall claims, where only three do not fail. The secrecy of SesK from the perspective of the Network. And agreement over the SesK and the time to live between the Phone and the Network, and the Application and the Network.
+		There are 9 overall claims, where only three do not fail. The secrecy of SesK from the perspective of the Network. And agreement over the SesK and the time to live between the Phone and the Network, and the Application and the Network.
 
 		The protocol as it stands does not guarantee secrecy and agreement.
 
-	
-
 \end{document}