From 525bf74eefe2f6ac8dee4ae51e09fa1718a6fd44 Mon Sep 17 00:00:00 2001
From: jm71syxy <jonas.mueller.97@stud.tu-darmstadt.de>
Date: Tue, 18 Jun 2024 13:50:13 +0200
Subject: [PATCH] Remove different non-repudiation approaches
---
ClassicEAC.spthy | 6 +++---
include/lemmas.spthy | 33 ---------------------------------
2 files changed, 3 insertions(+), 36 deletions(-)
diff --git a/ClassicEAC.spthy b/ClassicEAC.spthy
index 1beea11..403fc9b 100644
--- a/ClassicEAC.spthy
+++ b/ClassicEAC.spthy
@@ -53,7 +53,7 @@ let
msg3 = <s, '3', 't'>
in
[ In(msg2), TAInitT(<$T, iid>, skTe), !Ltk($T, ~skT, 'terminal') ]
- --[ Computed($T, 'terminal', s) ]->
+ -->
[ Out(msg3), TAResponseT(<$T, iid>, skTe, id_c) ]
rule TA_COMPLETE_C:
@@ -100,7 +100,7 @@ let
sid = <certT, certC, pkTe, 'g'^~skC, id_c, r2>
in
[ In(msg5), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ]
- --[ Eq(pkTe_t, pkTe), Computed($C, 'chip', <k, kMac, kEnc, tag>), Completed(<kEnc, kMac>, sid, $C, 'chip', cert_id(certT)) ]->
+ --[ Eq(pkTe_t, pkTe), Completed(<kEnc, kMac>, sid, $C, 'chip', cert_id(certT)) ]->
[ Out(msg6), CAFinishC($C, cert_id(certT), kEnc) ]
@@ -116,7 +116,7 @@ let
sid = <certT, certC, pkTe, pkC, id_c, r2>
in
[ In(msg6), CAInitT(<$T, iid>, skTe, id_c, certC), !Cert($T, certT, 'terminal') ]
- --[ Eq(tag, tag_T), Computed($T, 'terminal', <k, kMac, kEnc, tag_T>), Completed(<kEnc, kMac>, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
+ --[ Eq(tag, tag_T), Completed(<kEnc, kMac>, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
[ CAFinishT(cert_id(certC), $T, kEnc), !SessionReveal(sid, <kEnc, kMac>) ]
diff --git a/include/lemmas.spthy b/include/lemmas.spthy
index 73ffbba..69b4025 100644
--- a/include/lemmas.spthy
+++ b/include/lemmas.spthy
@@ -109,41 +109,8 @@ lemma chip_hiding:
| (Ex #m . (K(iid) @ #m & #i < #m))
"
-/* 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(k2, sid2, T, 'chip', T2) @ #i2
- & Completed(k2, sid2, T2, 'terminal', T) @ #j2
- "
-*/
/* We simulate a one sided protocol execution */
-
// The terminal submits a transcript for a valid protocol execution and the chip verifies it
// 1.: We prohibit any previous protocol executions
// 2.: The chip should not be corrupted, so that the terminal needs to forge the values
--
GitLab