Skip to content
Snippets Groups Projects
Commit 525bf74e authored by Müller, Jonas's avatar Müller, Jonas
Browse files

Remove different non-repudiation approaches

parent 1e86d53a
Branches
Tags
No related merge requests found
...@@ -53,7 +53,7 @@ let ...@@ -53,7 +53,7 @@ let
msg3 = <s, '3', 't'> msg3 = <s, '3', 't'>
in in
[ In(msg2), TAInitT(<$T, iid>, skTe), !Ltk($T, ~skT, 'terminal') ] [ In(msg2), TAInitT(<$T, iid>, skTe), !Ltk($T, ~skT, 'terminal') ]
--[ Computed($T, 'terminal', s) ]-> -->
[ Out(msg3), TAResponseT(<$T, iid>, skTe, id_c) ] [ Out(msg3), TAResponseT(<$T, iid>, skTe, id_c) ]
rule TA_COMPLETE_C: rule TA_COMPLETE_C:
...@@ -100,7 +100,7 @@ let ...@@ -100,7 +100,7 @@ let
sid = <certT, certC, pkTe, 'g'^~skC, id_c, r2> sid = <certT, certC, pkTe, 'g'^~skC, id_c, r2>
in in
[ In(msg5), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] [ 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) ] [ Out(msg6), CAFinishC($C, cert_id(certT), kEnc) ]
...@@ -116,7 +116,7 @@ let ...@@ -116,7 +116,7 @@ let
sid = <certT, certC, pkTe, pkC, id_c, r2> sid = <certT, certC, pkTe, pkC, id_c, r2>
in in
[ In(msg6), CAInitT(<$T, iid>, skTe, id_c, certC), !Cert($T, certT, 'terminal') ] [ 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>) ] [ CAFinishT(cert_id(certC), $T, kEnc), !SessionReveal(sid, <kEnc, kMac>) ]
......
...@@ -109,41 +109,8 @@ lemma chip_hiding: ...@@ -109,41 +109,8 @@ lemma chip_hiding:
| (Ex #m . (K(iid) @ #m & #i < #m)) | (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 */ /* We simulate a one sided protocol execution */
// The terminal submits a transcript for a valid protocol execution and the chip verifies it // The terminal submits a transcript for a valid protocol execution and the chip verifies it
// 1.: We prohibit any previous protocol executions // 1.: We prohibit any previous protocol executions
// 2.: The chip should not be corrupted, so that the terminal needs to forge the values // 2.: The chip should not be corrupted, so that the terminal needs to forge the values
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment