From 9060f3681976e6d3ca1cb8570cbbc0e1fa791c9b Mon Sep 17 00:00:00 2001
From: jm71syxy <jonas.mueller.97@stud.tu-darmstadt.de>
Date: Sat, 6 Jul 2024 14:41:57 +0200
Subject: [PATCH] Change flag in verify transcript and clean-up lemmas
---
include/kem_verify_transcript.spthy | 2 +-
include/lemmas.spthy | 51 ++++++++++++++---------------
include/setup.spthy | 2 +-
include/sig_verify_transcript.spthy | 2 +-
4 files changed, 27 insertions(+), 30 deletions(-)
diff --git a/include/kem_verify_transcript.spthy b/include/kem_verify_transcript.spthy
index 774a2f5..3d43d38 100644
--- a/include/kem_verify_transcript.spthy
+++ b/include/kem_verify_transcript.spthy
@@ -1,4 +1,4 @@
-#ifdef PFS
+#ifdef ForwardSecrecy
rule Verify_Transcript_C:
let
pkCe = pk(skCe)
diff --git a/include/lemmas.spthy b/include/lemmas.spthy
index 4335d5d..fbb6f3b 100644
--- a/include/lemmas.spthy
+++ b/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))
+ "
diff --git a/include/setup.spthy b/include/setup.spthy
index ad51ad8..3fa41f5 100644
--- a/include/setup.spthy
+++ b/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:
diff --git a/include/sig_verify_transcript.spthy b/include/sig_verify_transcript.spthy
index c88f69e..d461da3 100644
--- a/include/sig_verify_transcript.spthy
+++ b/include/sig_verify_transcript.spthy
@@ -1,4 +1,4 @@
-#ifdef PFS
+#ifdef ForwardSecrecy
rule Verify_Transcript_C:
let
pkT = cert_pk(certT)
--
GitLab