diff --git a/BasicEAC.spthy b/BasicEAC.spthy
index 6ca7c5049d1cf4cdc75c30280740c815b494f673..dfc0d9a3cbb34926708dadacb6c6d2207ac6834b 100644
--- a/BasicEAC.spthy
+++ b/BasicEAC.spthy
@@ -17,6 +17,7 @@ equations: cert_pk(cert(pk, s, id)) = pk, cert_sig(cert(pk, s, id)) = s, cert_id
 macros: verify_cert(cert) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert)>, pk(ca_sk))
 
 
+
 rule Publish_ca_pk:
     [ ]
   -->
@@ -88,7 +89,7 @@ let
 in
     [ !Cert($T, certT), Fr(~skTe), Fr(~iid) ] // skTe is ephemeral session key, iid is instance id of user $T
   -->
-    [ Out(msg1), TAInitT(<$T, ~iid>, ~skTe) ]
+    [ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>, ~skTe) ] // Publish T's iid as its identity gets revealed through certT
 
 // We generate a fresh IDc to simulate the previous execution of PACE or BAC
 rule TA_CHALLENGE_C:
@@ -117,7 +118,7 @@ let
     msg3 = <s, 'TA_RESPONSE', '3', 't'>
 in
     [ In(msg3), TAChallengeC(<$C, iid>, certT, pkTe, id_c, r1) ]
-  --[ Eq(verify(s, <id_c, r1, pkTe>, cert_pk(certT)), true) ]->
+  --[ Eq(verify(s, <id_c, r1, pkTe>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)) ]->
     [ TACompleteC(<$C, iid>, certT, pkTe, id_c, r1) ]
 
 
@@ -131,7 +132,7 @@ let
 in
     [ !CertDH($C, certC), Fr(~r2), TACompleteC(<$C, iid>, certT, pkTe, id_c, r1) ]
   -->
-    [ Out(msg4), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, ~r2) ]
+    [ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, ~r2) ] // Publish C's iid as its identity gets revealed through certC
 
 
 rule CA_INIT_T:
@@ -151,27 +152,29 @@ let
     k = pkTe^~skC
     kMac = kdf_mac(k, r2)
     kEnc = kdf_enc(k, r2)
-    tag = mac(kMac, pkTe)
+    tag = mac(pkTe, kMac)
     msg6 = <r2, tag, 'CA_RESPONSE', '6', 'c'>
-    sid = <pkTe, 'g'^~skC, id_c, r2>
+    sid = <certT, certC, pkTe, 'g'^~skC, id_c, r2, k>
 in
-    [ In(msg5), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, r2), !LtkDH($C, ~skC) ]
+    [ In(msg5), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, r2), !LtkDH($C, ~skC), !CertDH($C, certC) ]
   --[ Eq(pkTe_t, pkTe), Completed(<kEnc, kMac>, sid, $C, 'chip', cert_id(certT)) ]->
-    [ Out(msg6), CAFinishC($C, cert_id(certT), kEnc), Out(iid) ]
+    [ Out(msg6), CAFinishC($C, cert_id(certT), kEnc) ]
 
 
 rule CA_FINISH_T:
 let
     msg6 = <r2, tag, 'CA_RESPONSE', '6', 'c'>
     pkTe = 'g'^skTe
-    k = cert_pk(certC)^skTe
+    pkC = cert_pk(certC)
+    k = pkC^skTe
     kMac = kdf_mac(k, r2)
     kEnc = kdf_enc(k, r2)
-    sid = <pkTe, cert_pk(certC), id_c, r2>
+    tag_T = mac(pkTe, kMac)
+    sid = <certT, certC, pkTe, pkC, id_c, r2, k>
 in
-    [ In(msg6), CAInitT(<$T, iid>, skTe, id_c, certC) ]
-  --[ Eq(mac(kMac, pkTe), tag), Completed(<kEnc, kMac>, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
-    [ CAFinishT(cert_id(certC), $T, kEnc), !SessionReveal(<$T, iid>, skTe), Out(iid) ]
+    [ In(msg6), CAInitT(<$T, iid>, skTe, id_c, certC), !Cert($T, certT) ]
+  --[ Eq(tag, tag_T), Completed(<kEnc, kMac>, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
+    [ CAFinishT(cert_id(certC), $T, kEnc), !SessionReveal(<$T, iid>, skTe) ]
 
 
 
@@ -181,7 +184,6 @@ restriction Equality:
 
 // Correctness
 
-/*
 lemma session_exist: exists-trace
   " Ex C T k sid #i #j.
      Completed(k, sid, C, 'chip', T) @ #i
@@ -189,6 +191,7 @@ lemma session_exist: exists-trace
      & #i < #j
   "
 
+/*
 lemma two_session_exist: exists-trace
   " Ex C T k k2 sid sid2 #i #j #i2 #j2.
      Completed(k, sid, C, 'chip', T) @ #i
@@ -242,6 +245,7 @@ lemma agreement_T:
         | (Ex #k . Corrupted(T) @ #k)
   "
 
+/*
 lemma aliveness:
   "All k sid A role B #i #t .
     Completed(k, sid, A, role, B) @ #i
@@ -278,5 +282,27 @@ lemma key_secrecy:
         | (Ex #m . Corrupted(C) @ #m)
   "
 
+// Cannot track chip after TA
+lemma chip_hiding:
+  "All C T iid #i .
+    CompletedTA(C, iid, T) @ #i
+    ==> not(Ex #m . K(iid) @ #m)
+        | (Ex #m . (K(iid) @ #m & #i < #m))
+  "
+
+// Perfect forward secrecy
+lemma pfs:
+  "All A k sid role B #i #j .
+    Corrupted(A) @ #i
+    & Completed(k, sid, A, role, B) @ #j
+    & #j < #i
+    ==> not(Ex #m . K(k) @ #m)
+        | (Ex #m . (Corrupted(A) @ #m & #m < #j))
+        | (Ex #m . Corrupted(B) @ #m)
+        | (Ex iid #m . Revealed(<B, iid>) @ #m)
+        | (Ex iid #m . Revealed(<A, iid>) @ #m)
+  "
+*/
+
 end