Done 1.4

secondcw/ag01598_6644818_1_3.spdl

@@ -23,18 +23,16 @@ protocol protocolPI(Network, Application, Phone) {
 
 		var mApp: String;
 
-		var temp: Ticket;
-
 		recv_1(Application,Phone, {mApp, Application, Phone }SesK);
 
 		fresh mPhone: String;
 
-		claim_phone1(Phone, Running, Application, mApp);
+		claim_phone1(Phone, Running, Application, mApp, SesK);
 
 		send_2(Phone,Application, {mApp, mPhone}SesK);
 
 		claim_phone2(Phone, Secret, SesK);
-		claim_application1(Phone, Commit, Application, mApp);
+		claim_application1(Phone, Commit, Application, mApp, SesK);
 		claim_network2(Phone, Commit, Network, SesK, tl);
 		claim_phone3(Phone, Nisynch);
 
@@ -59,14 +57,14 @@ protocol protocolPI(Network, Application, Phone) {
 		fresh mApp: String;
 		var mPhone: String;
 
-		claim_application1(Application, Running, Phone, mApp);
+		claim_application1(Application, Running, Phone, mApp, SesK);
 
 		send_1(Application,Phone, {mApp, Application, Phone}SesK);
 
 		recv_2(Phone,Application, {mApp, mPhone}SesK);
 
 		claim_application2(Application, Secret, SesK);
-		claim_phone1(Application, Commit, Phone, mApp);
+		claim_phone1(Application, Commit, Phone, mApp, SesK);
 		claim_network1(Application, Commit, Network, SesK, tl);
 
 		claim_application3(Application, Nisynch);

secondcw/cw/cw.tex

@@ -81,6 +81,35 @@
 
 		The protocol as it stands does not guarantee secrecy and agreement.
 
+	\subsection*{1.3}
+		The file ag01598\_6644818\_1\_3.spdl contains the fixed version of $\text{protocol}\Pi$
+
+		The first change was to require the refresh keys request was to require the application to send a nounce, this nonce is then sent back to application to verify that the key was generated, was requested to the application and not by the attacker.
+
+		The second change was to make the network send the identity of the other party to party that is reciving the message. i.e. Sending the identity of the Phone to the Application encrypted with the key Network,Application. This is done to guarantee that the Party reciving the communication is using a key that was intended for this communication.
+
+	\subsection*{1.4}
+
+		The original $\text{protocol}\Pi$ is not an apropiate solution of the the third party problem as it can not guarantee the secresy of the session key, and since an attacker can obtain the session key, $\text{protocol}\Pi$ is not an appropiate solution to the present problem.As scyther showed the are attacks in the Dolev-Yao model. There are also some attacks in outside of Dolev-Yao model.
+
+		For example:
+
+		With the assumptions that:
+		\begin{itemize}
+			\item{Dolev-Yao attacker.}
+			\item{Strong cryptographic primitives}
+			\item{The time to live is implemented as a counter not an endate timetamp.}
+			\item{One of the previous keys where the encrypted version of the key and timestamp were recorded and leaked.}
+		\end{itemize}
+
+		In this senario an attacker can record the messages where the key and the time to live were encrypted. Then when the key gets leaked, the attacker can perform a replay attack.
+
+		The attacker resends the previously recorded keys to the application server and the phone, because the time to live is based on a counter and not on a timestamp the phone and the server accept the ``new'' key, and since the attacker already knows this key the protocol failed at guarantee, the secrecy of the session key.
+
+		% Other possible attacks are possible, for example a senario where the time to live is large, and the cryptographic primitives are weak for that time frame, i.e. RSA with 100 decimal digits and time to live of 2 days, an attacter with enought computer power would be abble to obtain the key
+
+		But it can be improved, as we saw in the answers for the question 1.3 by modifing the protocol slightly we can achive secrecy of the session key in the dolev-yao model. Although it does not resolve issues related with the time to live if the protocol was implemented with counters for time to live instead of timestamp.
+
 \end{document}