Change flag in verify transcript and clean-up lemmas

include/kem_verify_transcript.spthy

-#ifdef PFS
+#ifdef ForwardSecrecy
 rule Verify_Transcript_C:
 let
     pkCe = pk(skCe)

include/lemmas.spthy

@@ -25,6 +25,15 @@ lemma two_session_exist: exists-trace
   "
 
 // Agreement
+lemma aliveness:
+  "All k sid A role B #i #t .
+    Completed(k, sid, A, role, B) @ #i
+    & Finished(sid) @ #t
+    ==> (Ex k2 sid2 role2 C #j .
+        Completed(k2, sid2, B, role2, C) @ #j)
+        | (Ex #k . Corrupted(B) @ #k)
+  "
+
 lemma weak_agreement_C:
   "All k sid C T #i #t .
     Completed(k, sid, C, 'chip', T) @ #i
@@ -65,15 +74,6 @@ 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
-    & Finished(sid) @ #t
-    ==> (Ex k2 sid2 role2 C #j .
-        Completed(k2, sid2, B, role2, C) @ #j)
-        | (Ex #k . Corrupted(B) @ #k)
-  "
-
 lemma session_uniqueness:
   "All A B k sid sid2 role #i #j .
     Completed(k, sid, A, role, B) @ #i
@@ -102,25 +102,14 @@ lemma key_secrecy:
         | (Ex #m . Corrupted(T) @ #m)
   "
 
-// Cannot track chip before CA
-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))
-  "
-
-
 /* We simulate a one sided protocol execution */
 // The terminal submits a transcript for a valid protocol execution and the chip verifies it
+// If the terminal succeeds it has disproven non-repudiation for the chip
 // 1.: We prohibit any previous protocol executions
 // 2.: The chip should not be corrupted, so that the terminal needs to forge the values
 // 3.: The terminal is not allowed to register a chip certificate
 
-// This should be possible for the terminal
-
-
-lemma nonRepudiation_terminal: exists-trace
+lemma notNonRepudiation_C: exists-trace
   "Ex C T #i .
     ValidTrans(C, 'chip', T) @ #i
     & not(Ex #k . Started() @ #k)                 // 1.
@@ -130,10 +119,9 @@ lemma nonRepudiation_terminal: exists-trace
 
 
 // The chip submits a transcript for a valid protocol execution and the terminal verifies it
+// If the chip succeeds it has disproven non-repudiation for the terminal
 
-// This should NOT be possible for the chip
-
-lemma nonRepudiation_chip: exists-trace
+lemma notNonRepudiation_T: exists-trace
   "Ex C T #i .
     ValidTrans(T, 'terminal', C) @ #i
     & not(Ex #k . Started() @ #k)
@@ -141,8 +129,7 @@ lemma nonRepudiation_chip: exists-trace
     & not(Ex #k . RegisteredRole(C, 'terminal') @ #k)
   "
 
-// Perfect forward secrecy
-lemma pfs:
+lemma forward_secrecy:
   "All C T k sid #i #j .
     Completed(k, sid, C, 'chip', T) @ #i
     & Completed(k, sid, T, 'terminal', C) @ #j
@@ -151,3 +138,13 @@ lemma pfs:
     ==> (not(Ex #m . K(k) @ #m)
         | (Ex #m . Revealed(sid) @ #m))
   "
+
+lemma forward_secrecy_T:
+  "All C T k sid #i #j .
+    Completed(k, sid, C, 'chip', T) @ #i
+    & Completed(k, sid, T, 'terminal', C) @ #j
+    & not(Ex #m . Corrupted(C) @ #m)
+    & not(Ex #m . Corrupted(T) @ #m & #m < #j)
+    ==> (not(Ex #m . K(k) @ #m)
+        | (Ex #m . Revealed(sid) @ #m))
+  "

include/setup.spthy

@@ -19,7 +19,7 @@ let
     pk = 'g'^~ltk
 in
     [ Fr(~ltk) ]
-  --[ TestMe() ]->
+  -->
     [ !Pk($A, pk, 'chip'), !Ltk($A, ~ltk, 'chip'), Out(pk) ]
 #else
 rule Generate_chip_key_pair:

include/sig_verify_transcript.spthy

-#ifdef PFS
+#ifdef ForwardSecrecy
 rule Verify_Transcript_C:
 let
     pkT = cert_pk(certT)