From fe3f789fa2204cbf1cb47e5eae27fead2ffba920 Mon Sep 17 00:00:00 2001
From: jm71syxy <jonas.mueller.97@stud.tu-darmstadt.de>
Date: Tue, 11 Jun 2024 17:01:12 +0200
Subject: [PATCH] Add possible lemmata for the chip not non-repudiation
---
include/lemmas.spthy | 29 +++++++++++++++++++++++++----
1 file changed, 25 insertions(+), 4 deletions(-)
diff --git a/include/lemmas.spthy b/include/lemmas.spthy
index 1ab0161..b7d47ed 100644
--- a/include/lemmas.spthy
+++ b/include/lemmas.spthy
@@ -109,13 +109,34 @@ lemma chip_hiding:
| (Ex #m . (K(iid) @ #m & #i < #m))
"
-lemma nonRepudiation: exists-trace
+/* This lemma shows that the chip has NOT non-repudiation */
+// We use the exists-trace keyword because it is enough to show the possibility
+// 1.: To exclude an empty trace, we check for a finished protocol run (with the two Completed facts)
+// 2.: We define that the chip is not corrupted
+// 3.: We say that for every data the chip computed (which we manually put into action facts) the adversary could know the value before
+ // We use the adversaries knowledge because it is easy to model and he can simple corrupt the terminal and execute the protocol instead
+// Problems: Some information required so that the other party can compute the data is sent after the Computed fact
+
+lemma notNonRepudiation: exists-trace
"Ex C T k sid #i #j .
+ Completed(k, sid, C, 'chip', T) @ #i // 1.
+ & Completed(k, sid, T, 'terminal', C) @ #j // 1.
+ & not(Ex #n . Corrupted(C) @ #n) // 2.
+ & (All data #m . Computed(C, 'chip', data) @ #m // 3.
+ ==> (Ex #k . K(data) @ #k & #k < #m)) // 3.
+ "
+
+/* This lemma shows that the chip has NOT non-repudiation */
+// We use the fact that every value the chip can calculate its partner could too
+// We state the possibility that with a finished protocol run the terminal could identify as a chip because it knows all the computations too
+// Problems: pkTe is a fresh value used in the DH key, T could simply get a chip certificate and key pair (this could be solved but would limit our model), limited by our model at the moment because the identity from Completed is from the sent certificate which prevents T from trying a replay scenario
+
+lemma notNonRepudiation2: exists-trace
+ "Ex C T T2 k k2 sid sid2 #i #i2 #j #j2 .
Completed(k, sid, C, 'chip', T) @ #i
& Completed(k, sid, T, 'terminal', C) @ #j
- & not(Ex #n . Corrupted(C) @ #n)
- & (All data #m . Computed(C, 'chip', data) @ #m
- ==> (Ex #k . K(data) @ #k & #k < #m))
+ & Completed(k2, sid2, T, 'chip', T2) @ #i2
+ & Completed(k2, sid2, T2, 'terminal', T) @ #j2
"
// Perfect forward secrecy
--
GitLab