Added question 2

secondcw/ag01598_6644818_1_2.spdl

@@ -0,0 +1,95 @@
+/* 
+ * Coursework 2 PI protocol
+*/
+usertype String;
+usertype Timestamp;
+usertype Sessionkey;
+
+hashfunction Mac;
+
+protocol protocolPI(Network, Application, Phone) {
+
+	/* Role R - Phone
+	 *
+	 * has keys k(N,R)
+	 *
+	 */
+	role Phone {
+
+		var SesK: SessionKey;
+		var tl: Timestamp;
+
+		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));
+
+		fresh mPhone: String;
+
+		claim_phone1(Phone, Running, Application, mApp);
+
+		send_2(Phone,Application, {mApp, mPhone}k(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 {
+
+		send_refreshKeys(Application,Network, Application, Phone);
+
+		var SesK: SessionKey;
+		var tl: Timestamp;
+
+		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));
+
+		recv_2(Phone,Application, {mApp, mPhone}k(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 {
+
+		recv_refreshKeys(Application,Network, Application, Phone);
+
+		fresh SesK: SessionKey;
+		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));
+
+		claim_network2(Network, Running, Phone, SesK, tl);
+		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/cw/cw.tex

@@ -51,7 +51,7 @@
 \begin{document}
 	\section*{1}
 	\subsection*{1.1}
-		The file ag01598\_6644818\_1.1.spdl contains the base model of $\text{protocol}\Pi$.
+		The file ag01598\_6644818\_1\_1.spdl contains the base model of $\text{protocol}\Pi$.
 
 		I choose the names of the roles based on their functions since it would make the file more readable so R is Phone, S is Application, N is Network.
 
@@ -62,6 +62,24 @@
 		The Network then aswers to the Phone and the Application the keys and the time to live and the hashed value of that using a hash function named ``Mac''.
 
 		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.
+
+	\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 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}
+			\item{Agreement between Phone and Network over the time to live and the session key}
+			\item{Agreement between Application and Network over the time to live and the session key}
+			\item{Agreement between Application and Phone over the message and the message m}
+		\end{itemize}
+
+
+
+
+		
+
 	
 
 \end{document}