From 1e86d53ab40c8a91a51997285e0ca00f8f7a6fa9 Mon Sep 17 00:00:00 2001
From: jm71syxy <jonas.mueller.97@stud.tu-darmstadt.de>
Date: Wed, 12 Jun 2024 20:39:32 +0200
Subject: [PATCH] Add one-sided protocol simulation approach
---
ClassicEAC.spthy | 6 +-
FastKemPQEAC.spthy | 7 +-
FastSigPQEAC.spthy | 8 +-
KemPQEAC.spthy | 6 +-
SigPQEAC.spthy | 5 +-
include/classic_verify_transcript.spthy | 24 ++
include/kem_verify_transcript.spthy | 75 ++++
include/lemmas.spthy | 36 +-
include/setup.spthy | 2 +-
include/sig_verify_transcript.spthy | 46 +++
tmp.spthy | 463 ++++++++++++++++++++++++
11 files changed, 664 insertions(+), 14 deletions(-)
create mode 100644 include/classic_verify_transcript.spthy
create mode 100644 include/kem_verify_transcript.spthy
create mode 100644 include/sig_verify_transcript.spthy
create mode 100644 tmp.spthy
diff --git a/ClassicEAC.spthy b/ClassicEAC.spthy
index 33173fc..1beea11 100644
--- a/ClassicEAC.spthy
+++ b/ClassicEAC.spthy
@@ -32,7 +32,7 @@ let
msg1 = <certT, pkTe, '1', 't'>
in
[ !Cert($T, certT, 'terminal'), Fr(~skTe), Fr(~iid) ] // skTe is ephemeral session key, iid is instance id of user $T
- -->
+ --[ Started() ]->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>, ~skTe) ] // Publish T's iid as its identity gets revealed through certT
// We generate a fresh IDc to simulate the previous execution of PACE or BAC
@@ -42,7 +42,7 @@ let
msg2 = <~id_c, ~r1, '2', 'c'>
in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid) ]
- --[ Eq(verify_cert(certT, 'terminal'), true) ]->
+ --[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
[ Out(msg2), TAChallengeC(<$C, ~iid>, certT, pkTe, ~id_c, ~r1) ]
rule TA_RESPONSE_T:
@@ -120,7 +120,9 @@ in
[ CAFinishT(cert_id(certC), $T, kEnc), !SessionReveal(sid, <kEnc, kMac>) ]
+insert(include/classic_verify_transcript.spthy)
insert(include/lemmas.spthy)
+
end
diff --git a/FastKemPQEAC.spthy b/FastKemPQEAC.spthy
index 91ad6f0..f316e18 100644
--- a/FastKemPQEAC.spthy
+++ b/FastKemPQEAC.spthy
@@ -31,7 +31,7 @@ let
msg1 = <certT, '1', 't'>
in
[ !Cert($T, certT, 'terminal'), Fr(~iid) ]
- -->
+ --[ Started() ]->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ]
#ifdef PFS
@@ -46,7 +46,7 @@ let
msg2 = <~id_c, ~r1, cTA, cCA, '2', 'c'>
in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~r2), Fr(~skCe), Fr(~iid), !Cert($C, certC, 'chip') ]
- --[ Eq(verify_cert(certT, 'terminal'), true) ]->
+ --[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
[ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, ~skCe, kTMAC, kTCNF) ]
#else
rule TA_CHALLENGE_C:
@@ -60,7 +60,7 @@ let
msg2 = <~id_c, ~r1, cTA, cCA, '2', 'c'>
in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~r2), Fr(~iid), !Cert($C, certC, 'chip') ]
- --[ Eq(verify_cert(certT, 'terminal'), true) ]->
+ --[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
[ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, kTMAC, kTCNF) ]
#endif
@@ -162,6 +162,7 @@ in
#endif
+insert(include/kem_verify_transcript.spthy)
insert(include/lemmas.spthy)
diff --git a/FastSigPQEAC.spthy b/FastSigPQEAC.spthy
index 0e101cd..5b4f4cd 100644
--- a/FastSigPQEAC.spthy
+++ b/FastSigPQEAC.spthy
@@ -30,7 +30,7 @@ let
msg1 = <certT, '1', 't'>
in
[ !Cert($T, certT, 'terminal'), Fr(~iid) ]
- -->
+ --[ Started() ]->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ]
#ifdef PFS
@@ -40,7 +40,7 @@ let
msg2 = <~id_c, ~r1, certC, ~r2, pk(~skCe), '2', 'c'>
in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid), Fr(~skCe), Fr(~r2), !Cert($C, certC, 'chip') ]
- --[ Eq(verify_cert(certT, 'terminal'), true) ]->
+ --[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
[ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~skCe, ~r2) ]
#else
rule TA_CHALLENGE_C:
@@ -49,7 +49,7 @@ let
msg2 = <~id_c, ~r1, certC, ~r2, '2', 'c'>
in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid), Fr(~r2), !Cert($C, certC, 'chip') ]
- --[ Eq(verify_cert(certT, 'terminal'), true) ]->
+ --[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
[ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2) ]
#endif
@@ -138,6 +138,8 @@ in
#endif
+insert(include/sig_verify_transcript.spthy)
+
insert(include/lemmas.spthy)
diff --git a/KemPQEAC.spthy b/KemPQEAC.spthy
index f17d6b4..6c46f49 100644
--- a/KemPQEAC.spthy
+++ b/KemPQEAC.spthy
@@ -31,7 +31,7 @@ let
msg1 = <certT, '1', 't'>
in
[ !Cert($T, certT, 'terminal'), Fr(~iid) ]
- -->
+ --[ Started() ]->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ]
// We generate a fresh IDc to simulate the previous execution of PACE or BAC
@@ -42,7 +42,7 @@ let
msg2 = <~id_c, ~r1, cTA, '2', 'c'>
in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~iid) ]
- --[ Eq(verify_cert(certT, 'terminal'), true) ]->
+ --[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
[ Out(msg2), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, <~kTA, cTA>) ]
rule TA_RESPONSE_T:
@@ -187,6 +187,8 @@ in
#endif
+insert(include/kem_verify_transcript.spthy)
+
insert(include/lemmas.spthy)
diff --git a/SigPQEAC.spthy b/SigPQEAC.spthy
index 6ef2ee1..9ad48e5 100644
--- a/SigPQEAC.spthy
+++ b/SigPQEAC.spthy
@@ -31,7 +31,7 @@ let
msg1 = <certT, '1', 't'>
in
[ !Cert($T, certT, 'terminal'), Fr(~iid) ]
- -->
+ --[ Started() ]->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ]
// We generate a fresh IDc to simulate the previous execution of PACE or BAC
@@ -41,7 +41,7 @@ let
msg2 = <~id_c, ~r1, '2', 'c'>
in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid) ]
- --[ Eq(verify_cert(certT, 'terminal'), true) ]->
+ --[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
[ Out(msg2), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1) ]
rule TA_RESPONSE_T:
@@ -170,6 +170,7 @@ in
#endif
+insert(include/sig_verify_transcript.spthy)
insert(include/lemmas.spthy)
diff --git a/include/classic_verify_transcript.spthy b/include/classic_verify_transcript.spthy
new file mode 100644
index 0000000..2453ba3
--- /dev/null
+++ b/include/classic_verify_transcript.spthy
@@ -0,0 +1,24 @@
+rule Verify_Transcript_C:
+let
+ pkT = cert_pk(certT)
+ k = pkTe^skC
+ kMac = kdf_mac(k, r2)
+ tag_c = mac(pkTe, kMac)
+in
+ [ In(<certT, pkTe, IDc, r1, s1, certC, pkTe2, r2, tag>), !Ltk(C, skC, 'chip') ]
+ --[ Eq(C, cert_id(certC)), Eq(tag, tag_c), Eq(pkTe, pkTe2), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(s1, <IDc, r1, pkTe>, pkT), true), ValidTrans(C, 'chip', cert_id(certT)) ]->
+ [ ]
+
+rule Verify_Transcript_T:
+let
+ pkT = cert_pk(certT)
+ pkC = cert_pk(certC)
+ tag_t = mac(pkTe, kdf_mac(r2, skTe^pkC))
+ k = pkC^skTe
+ kMac = kdf_mac(k, r2)
+ tag_t = mac(pkTe, kMac)
+in
+ [ In(<certT, pkTe, IDc, r1, s1, certC, pkTe2, r2, tag>), In(<skTe, T>) ]
+ --[ Eq(T, cert_id(certT)), Eq(tag, tag_t), Eq(pkTe, pkTe2), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(s1, <IDc, r1, pkTe>, pkT), true), ValidTrans(T, 'terminal', cert_id(certC)) ]->
+ [ ]
+
diff --git a/include/kem_verify_transcript.spthy b/include/kem_verify_transcript.spthy
new file mode 100644
index 0000000..7fe69d9
--- /dev/null
+++ b/include/kem_verify_transcript.spthy
@@ -0,0 +1,75 @@
+#ifdef PFS
+rule Verify_Transcript_C:
+let
+ kTMAC = kdf(<'TMAC', r1>, kTA)
+ kTENC = kdf(<'TENC', r1>, kTA)
+ kTCNF_c = kdf(<'TCNF', r1>, kTA)
+ dmesg = sdec(cCA, kTENC)
+ certC = fst(dmesg)
+ r2 = snd(dmesg)
+ sid = <certT, certC, r2, cip, pkCe, cipe>
+ s_c = mac(<'CA', sid>, kTMAC)
+ k = decaps(cip, skC)
+ ke = decaps(cipe, skCe)
+ kCNF_c = kdf(<'CNF', sid>, <k, ke>)
+in
+ [ In(<certT, IDc, r1, cTA, kTCNF, cCA, cip, s, cipe, kCNF>), In(<kTA, skCe>), !Ltk(C, skC, 'chip') ]
+ --[ Eq(C, cert_id(certC)), Eq(verify_cert(certC, 'chip'), true), Eq(verify_cert(certT, 'terminal'), true), Eq(kTCNF, kTCNF_c), Eq(s, s_c), Eq(kCNF, kCNF_c), ValidTrans(C, 'chip', cert_id(certT)) ]->
+ [ ]
+#else
+rule Verify_Transcript_C:
+let
+ kTMAC = kdf(<'TMAC', r1>, kTA)
+ kTENC = kdf(<'TENC', r1>, kTA)
+ kTCNF_c = kdf(<'TCNF', r1>, kTA)
+ dmesg = sdec(cCA, kTENC)
+ certC = fst(dmesg)
+ r2 = fst(snd(dmesg))
+ pkCe = snd(snd(dmesg))
+ sid = <certT, certC, r2, cip>
+ s_c = mac(<'CA', sid>, kTMAC)
+ kKDF = decaps(cip, skC)
+ kCNF_c = kdf(<'CNF', sid>, kKDF)
+in
+ [ In(<certT, IDc, r1, cTA, kTCNF, cCA, cip, s, kCNF>), In(kTA), !Ltk(C, skC, 'chip') ]
+ --[ Eq(C, cert_id(certC)), Eq(verify_cert(certC, 'chip'), true), Eq(verify_cert(certT, 'terminal'), true), Eq(kTCNF, kTCNF_c), Eq(s, s_c), Eq(kCNF, kCNF_c), ValidTrans(C, 'chip', cert_id(certT)) ]->
+ [ ]
+#endif
+
+
+#ifdef PFS
+rule Verify_Transcript_T:
+let
+ kTA = decaps(cTA, skT)
+ kTMAC = kdf(<'TMAC', r1>, kTA)
+ kTENC = kdf(<'TENC', r1>, kTA)
+ kTCNF_t = kdf(<'TCNF', r1>, kTA)
+ dmesg = sdec(cCA, kTENC)
+ certC = fst(dmesg)
+ r2 = fst(snd(dmesg))
+ pkCe = snd(snd(dmesg))
+ sid = <certT, certC, r2, cip, pkCe, cipe>
+ s_t = mac(<'CA', sid>, kTMAC)
+ kCNF_t = kdf(<'CNF', sid>, <k, ke>)
+in
+ [ In(<certT, IDc, r1, cTA, kTCNF, cCA, cip, s, cipe, kCNF>), In(<k, ke>), !Ltk(T, skT, 'terminal') ]
+ --[ Eq(T, cert_id(certT)), Eq(verify_cert(certC, 'chip'), true), Eq(verify_cert(certT, 'terminal'), true), Eq(kTCNF, kTCNF_t), Eq(s, s_t), Eq(kCNF, kCNF_t), ValidTrans(T, 'terminal', cert_id(certC)) ]->
+ [ ]
+#else
+rule Verify_Transcript_T:
+let
+ kTA = decaps(cTA, skT)
+ kTMAC = kdf(<'TMAC', r1>, kTA)
+ kTENC = kdf(<'TENC', r1>, kTA)
+ kTCNF_t = kdf(<'TCNF', r1>, kTA)
+ dmesg = sdec(cCA, kTENC)
+ certC = fst(dmesg)
+ r2 = snd(dmesg)
+ sid = <certT, certC, r2, cip>
+ s_t = mac(<'CA', sid>, kTMAC)
+ kCNF_t = kdf(<'CNF', sid>, kKDF)
+in
+ [ In(<certT, IDc, r1, cTA, kTCNF, cCA, cip, s, kCNF>), In(kKDF), !Ltk(T, skT, 'terminal') ]
+ --[ Eq(T, cert_id(certT)), Eq(verify_cert(certC, 'chip'), true), Eq(verify_cert(certT, 'terminal'), true), Eq(kTCNF, kTCNF_t), Eq(s, s_t), Eq(kCNF, kCNF_t), ValidTrans(T, 'terminal', cert_id(certC)) ]->
+ [ ]
+#endif
diff --git a/include/lemmas.spthy b/include/lemmas.spthy
index b7d47ed..73ffbba 100644
--- a/include/lemmas.spthy
+++ b/include/lemmas.spthy
@@ -117,6 +117,7 @@ lemma chip_hiding:
// 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.
@@ -125,19 +126,52 @@ lemma notNonRepudiation: exists-trace
& (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
& 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
+// 3.: The terminal is not allowed to register a chip certificate
+
+// This should be possible for the terminal
+
+
+lemma nonRepudiation_terminal: exists-trace
+ "Ex C T #i .
+ ValidTrans(C, 'chip', T) @ #i
+ & not(Ex #k . Started() @ #k) // 1.
+ & not(Ex #k . Corrupted(C) @ #k) // 2.
+ & not(Ex #k . RegisteredRole(T, 'chip') @ #k) // 3.
+ "
+
+
+// The chip submits a transcript for a valid protocol execution and the terminal verifies it
+
+// This should NOT be possible for the chip
+
+lemma nonRepudiation_chip: exists-trace
+ "Ex C T #i .
+ ValidTrans(T, 'terminal', C) @ #i
+ & not(Ex #k . Started() @ #k)
+ & not(Ex #k . Corrupted(T) @ #k)
+ & not(Ex #k . RegisteredRole(C, 'terminal') @ #k)
+ "
// Perfect forward secrecy
lemma pfs:
diff --git a/include/setup.spthy b/include/setup.spthy
index 7903187..ad51ad8 100644
--- a/include/setup.spthy
+++ b/include/setup.spthy
@@ -45,5 +45,5 @@ let
certA = cert(pk, sign(<pk, A, role>, ca_sk), A)
in
[ !Pk(A, pk, role) ]
- -->
+ --[ RegisteredRole(A, role) ]->
[ !Cert(A, certA, role), Out(certA) ]
diff --git a/include/sig_verify_transcript.spthy b/include/sig_verify_transcript.spthy
new file mode 100644
index 0000000..811c24f
--- /dev/null
+++ b/include/sig_verify_transcript.spthy
@@ -0,0 +1,46 @@
+#ifdef PFS
+rule Verify_Transcript_C:
+let
+ pkT = cert_pk(certT)
+ sid = <certT, certC, r2, cip, pkCe, cipe>
+ k = decaps(cip, skC)
+ ke = decaps(cipe, skCe)
+ kCNF_c = kdf(<'CNF', sid>, <k, ke>)
+in
+ [ In(<certT, IDc, r1, sT, certC, r2, pkCe, cip, sC, cipe, kCNF>), In(skCe), !Ltk(C, skC, 'chip') ]
+ --[ Eq(C, cert_id(certC)), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(sT, <'TA', IDc, r1>, pkT), true), Eq(verify(sC, <'CA', sid>, pkT), true), Eq(kCNF, kCNF_c), ValidTrans(C, 'chip', cert_id(certT)) ]->
+ [ ]
+#else
+rule Verify_Transcript_C:
+let
+ pkT = cert_pk(certT)
+ sid = <certT, certC, r2, cip>
+ kKDF = decaps(cip, skC)
+ kCNF_c = kdf(<'CNF', sid>, kKDF)
+in
+ [ In(<certT, IDc, r1, sT, certC, r2, cip, sC, kCNF>), !Ltk(C, skC, 'chip') ]
+ --[ Eq(C, cert_id(certC)), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(sT, <'TA', IDc, r1>, pkT), true), Eq(verify(sC, <'CA', sid>, pkT), true), Eq(kCNF, kCNF_c), ValidTrans(C, 'chip', cert_id(certT)) ]->
+ [ ]
+#endif
+
+#ifdef PFS
+rule Verify_Transcript_T:
+let
+ pkT = cert_pk(certT)
+ sid = <certT, certC, r2, cip, pkCe, cipe>
+ kCNF_t = kdf(<'CNF', sid>, <k, ke>)
+in
+ [ In(<certT, IDc, r1, sT, certC, r2, pkCe, cip, sC, cipe, kCNF>), In(<k, ke>) ]
+ --[ Eq(T, cert_id(certT)), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(sT, <'TA', IDc, r1>, pkT), true), Eq(verify(sC, <'CA', sid>, pkT), true), Eq(kCNF, kCNF_t), ValidTrans(T, 'terminal', cert_id(certC)) ]->
+ [ ]
+#else
+rule Verify_Transcript_T:
+let
+ pkT = cert_pk(certT)
+ sid = <certT, certC, r2, cip>
+ kCNF_t = kdf(<'CNF', sid>, kKDF)
+in
+ [ In(<certT, IDc, r1, sT, certC, r2, cip, sC, kCNF>), In(kKDF) ]
+ --[ Eq(T, cert_id(certT)), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(sT, <'TA', IDc, r1>, pkT), true), Eq(verify(sC, <'CA', sid>, pkT), true), Eq(kCNF, kCNF_t), ValidTrans(T, 'terminal', cert_id(certC)) ]->
+ [ ]
+#endif
diff --git a/tmp.spthy b/tmp.spthy
new file mode 100644
index 0000000..9d54c88
--- /dev/null
+++ b/tmp.spthy
@@ -0,0 +1,463 @@
+/*
+PQ-EAC with Terminal Signatures
+======================================
+
+Author: Jonas Mueller
+Date: May 2024
+
+*/
+
+theory SigPQEAC
+begin
+
+builtins: signing
+functions: kdf/2
+functions: encaps/2, decaps/2
+equations: decaps((encaps(k, pk(sk))), sk) = k
+
+
+/* Key setup and Certificate model for all EAC models */
+
+
+functions: cert/3, cert_pk/1, cert_sig/1, cert_id/1, ca_sk/0 [private]
+equations: cert_pk(cert(pk, s, id)) = pk, cert_sig(cert(pk, s, id)) = s, cert_id(cert(pk, s, id)) = id
+
+macros: verify_cert(cert, role) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert), role>, pk(ca_sk))
+
+
+rule Publish_ca_pk:
+ [ ]
+ -->
+ [ Out(pk(ca_sk)) ]
+
+// Generate long-term key pair for the chip. Classic version needs dh key pair
+#ifdef CLASSIC
+rule Generate_chip_key_pair:
+let
+ pk = 'g'^~ltk
+in
+ [ Fr(~ltk) ]
+ --[ TestMe() ]->
+ [ !Pk($A, pk, 'chip'), !Ltk($A, ~ltk, 'chip'), Out(pk) ]
+#else
+rule Generate_chip_key_pair:
+let
+ pk = pk(~ltk)
+in
+ [ Fr(~ltk) ]
+ -->
+ [ !Pk($A, pk, 'chip'), !Ltk($A, ~ltk, 'chip'), Out(pk) ]
+#endif
+
+// Generate static long-term key pair for the terminal.
+rule Generate_terminal_key_pair:
+let
+ pk = pk(~ltk)
+in
+ [ Fr(~ltk) ]
+ -->
+ [ !Pk($A, pk, 'terminal'), !Ltk($A, ~ltk, 'terminal'), Out(pk) ]
+
+rule CA_Sign_ltk:
+let
+ certA = cert(pk, sign(<pk, A, role>, ca_sk), A)
+in
+ [ !Pk(A, pk, role) ]
+ --[ RegisteredRole(A, role) ]->
+ [ !Cert(A, certA, role), Out(certA) ]
+
+/* Attacker model */
+// We extend the Dolev-Yao attack model in tamarin with Reveal and Corrupt capabilities
+
+rule Corrupt_ltk:
+ [ !Ltk($A, ltk, role) ]
+ --[ Corrupted($A) ]->
+ [ Out(<ltk, role>) ]
+
+rule Reveal_session:
+ [ !SessionReveal(sid, k) ]
+ --[ Revealed(sid) ]->
+ [ Out(k) ]
+
+
+
+/* Terminal Authentication */
+// State machine: TA_INIT_T -> TA_CHALLENGE_C -> TA_RESPONSE_T -> TA_COMPLETE_C
+
+
+rule TA_INIT_T:
+let
+ msg1 = <certT, '1', 't'>
+in
+ [ !Cert($T, certT, 'terminal'), Fr(~iid) ]
+ --[ Started() ]->
+ [ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ]
+
+// We generate a fresh IDc to simulate the previous execution of PACE or BAC
+rule TA_CHALLENGE_C:
+let
+ msg1 = <certT, '1', 't'>
+ msg2 = <~id_c, ~r1, '2', 'c'>
+in
+ [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid) ]
+ --[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
+ [ Out(msg2), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1) ]
+
+rule TA_RESPONSE_T:
+let
+ msg2 = <id_c, r1, '2', 'c'>
+ s = sign(<'TA', id_c, r1>, ~skT)
+ msg3 = <s, '3', 't'>
+in
+ [ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT, 'terminal') ]
+ -->
+ [ Out(msg3), TAResponseT(<$T, iid>, id_c) ]
+
+rule TA_COMPLETE_C:
+let
+ msg3 = <s, '3', 't'>
+in
+ [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1) ]
+ --[ Eq(verify(s, <'TA', id_c, r1>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)) ]->
+ [ TACompleteC(<$C, iid>, certT, id_c, r1) ]
+
+
+
+/* Chip Authentication */
+// State machine: CA_INIT_C -> CA_INIT_T -> CA_FINISH_C -> CA_FINISH_T
+
+#ifdef PFS
+rule CA_INIT_C:
+let
+ msg4 = <certC, ~r2, pk(~skCe), '4', 'c'>
+in
+ [ Fr(~r2), Fr(~skCe), TACompleteC(<$C, iid>, certT, id_c, r1), !Cert($C, certC, 'chip') ]
+ -->
+ [ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, ~r2, ~skCe) ]
+#else
+rule CA_INIT_C:
+let
+ msg4 = <certC, ~r2, '4', 'c'>
+in
+ [ Fr(~r2), TACompleteC(<$C, iid>, certT, id_c, r1), !Cert($C, certC, 'chip') ]
+ -->
+ [ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, ~r2) ]
+#endif
+
+
+#ifdef PFS
+rule CA_INIT_T:
+let
+ msg4 = <certC, r2, pkCe, '4', 'c'>
+ pkC = cert_pk(certC)
+ cip = encaps(~k, pkC)
+ cipe = encaps(~ke, pkCe)
+ sid = <certT, certC, r2, cip, pkCe, cipe>
+ s = sign(<'CA', sid>, ~skT)
+ msg5 = <cip, s, cipe, '5', 't'>
+in
+ [ In(msg4), Fr(~k), Fr(~ke), TAResponseT(<$T, iid>, id_c), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ]
+ --[ Eq(verify_cert(certC, 'chip'), true) ]->
+ [ Out(msg5), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ]
+#else
+rule CA_INIT_T:
+let
+ msg4 = <certC, r2, '4', 'c'>
+ pkC = cert_pk(certC)
+ cip = encaps(~k, pkC)
+ sid = <certT, certC, r2, cip>
+ s = sign(<'CA', sid>, ~skT)
+ msg5 = <cip, s, '5', 't'>
+in
+ [ In(msg4), Fr(~k), TAResponseT(<$T, iid>, id_c), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ]
+ --[ Eq(verify_cert(certC, 'chip'), true) ]->
+ [ Out(msg5), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>) ]
+#endif
+
+
+#ifdef PFS
+rule CA_FINISH_C:
+let
+ msg5 = <cip, s, cipe, '5', 't'>
+ sid = <certT, certC, r2, cip, pk(skCe), cipe>
+ k = decaps(cip, ~skC)
+ ke = decaps(cipe, skCe)
+ kCNF = kdf(<'CNF', sid>, <k, ke>)
+ kKEY = kdf(<'KEY', sid>, <k, ke>)
+ msg6 = <kCNF, '6', 'c'>
+in
+ [ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, r2, skCe), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ]
+ --[ Eq(verify(s, <'CA', sid>, cert_pk(certT)), true), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
+ [ Out(msg6), CAFinishC($C, cert_id(certT), kKEY) ]
+#else
+rule CA_FINISH_C:
+let
+ msg5 = <cip, s, '5', 't'>
+ sid = <certT, certC, r2, cip>
+ k = decaps(cip, ~skC)
+ kCNF = kdf(<'CNF', sid>, k)
+ kKEY = kdf(<'KEY', sid>, k)
+ msg6 = <kCNF, '6', 'c'>
+in
+ [ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ]
+ --[ Eq(verify(s, <'CA', sid>, cert_pk(certT)), true), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
+ [ Out(msg6), CAFinishC($C, cert_id(certT), kKEY) ]
+#endif
+
+#ifdef PFS
+rule CA_FINISH_T:
+let
+ msg6 = <kCNF_C, '6', 'c'>
+ sid = <certT, certC, r2, cip, pkCe, cipe>
+ kCNF = kdf(<'CNF', sid>, <k, ke>)
+ kKEY = kdf(<'KEY', sid>, <k, ke>)
+in
+ [ In(msg6), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT, 'terminal') ]
+ --[ Eq(kCNF, kCNF_C), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
+ [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ]
+#else
+rule CA_FINISH_T:
+let
+ msg6 = <kCNF_c, '6', 'c'>
+ sid = <certT, certC, r2, cip>
+ kCNF = kdf(<'CNF', sid>, k)
+ kKEY = kdf(<'KEY', sid>, k)
+in
+ [ In(msg6), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>), !Cert($T, certT, 'terminal') ]
+ --[ Eq(kCNF, kCNF_c), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
+ [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ]
+#endif
+
+
+
+
+/* Contains the restrictions and lemmas for all EAC models */
+
+restriction Equality:
+ "All x y #i. Eq(x, y) @ i ==> x = y"
+
+
+// Correctness
+
+lemma session_exist: exists-trace
+ " Ex C T k sid #i #j.
+ Completed(k, sid, C, 'chip', T) @ #i
+ & Completed(k, sid, T, 'terminal', C) @ #j
+ & #i < #j
+ "
+
+lemma two_session_exist: exists-trace
+ " Ex C T k k2 sid sid2 #i #j #i2 #j2.
+ Completed(k, sid, C, 'chip', T) @ #i
+ & Completed(k, sid, T, 'terminal', C) @ #j
+ & #i < #j
+ & Completed(k2, sid2, C, 'chip', T) @ #i2
+ & Completed(k2, sid2, T, 'terminal', C) @ #j2
+ & #i2 < #j2
+ & not(k=k2)
+ "
+
+// Agreement
+lemma weak_agreement_C:
+ "All k sid C T #i #t .
+ Completed(k, sid, C, 'chip', T) @ #i
+ & Finished(sid) @ #t
+ ==> (Ex k2 sid2 #j .
+ Completed(k2, sid2, T, 'terminal', C) @ #j)
+ | (Ex #k . Corrupted(C) @ #k)
+ | (Ex #k . Corrupted(T) @ #k)
+ "
+
+lemma weak_agreement_T:
+ "All k sid C T #i #t .
+ Completed(k, sid, T, 'terminal', C) @ #i
+ & Finished(sid) @ #t
+ ==> (Ex k2 sid2 #j .
+ Completed(k2, sid2, C, 'chip', T) @ #j)
+ | (Ex #k . Corrupted(C) @ #k)
+ | (Ex #k . Corrupted(T) @ #k)
+ "
+
+lemma agreement_C:
+ "All k sid C T #i #t .
+ Completed(k, sid, C, 'chip', T) @ #i
+ & Finished(sid) @ #t
+ ==> (Ex #j .
+ Completed(k, sid, T, 'terminal', C) @ #j)
+ | (Ex #k . Corrupted(C) @ #k)
+ | (Ex #k . Corrupted(T) @ #k)
+ "
+
+lemma agreement_T:
+ "All k sid C T #i #t .
+ Completed(k, sid, T, 'terminal', C) @ #i
+ & Finished(sid) @ #t
+ ==> (Ex #j .
+ Completed(k, sid, C, 'chip', T) @ #j)
+ | (Ex #k . Corrupted(C) @ #k)
+ | (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
+ & Completed(k, sid2, A, role, B) @ #j
+ ==> (#i = #j) & (sid = sid2)
+ "
+
+// Sole purpose of static key of T is authentication
+// The final keys k/k2 are only derived from pkC/skC, pkTe/skTe and r2
+lemma consistency:
+ "All C T k k2 sid #i #j .
+ Completed(k, sid, C, 'chip', T) @ #i
+ & Completed(k2, sid, T, 'terminal', C) @ #j
+ ==> (k=k2)
+ | (Ex #m . Corrupted(C) @ #m)
+ "
+
+// Key secrecy
+lemma key_secrecy:
+ "All C T k sid #i #j .
+ Completed(k, sid, C, 'chip', T) @ #i
+ & Completed(k, sid, T, 'terminal', C) @ #j
+ ==> not(Ex #m . K(k) @ #m)
+ | (Ex #m . Revealed(sid) @ #m)
+ | (Ex #m . Corrupted(C) @ #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))
+ "
+
+/* 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 finishes the protocol by itself
+// It does not register a chip certificate and the chip shouldn't be involved in the protocol execution
+// This should be possible for the terminal
+
+lemma nonRepudiation_terminal: exists-trace
+ "Ex C T #i .
+ ValidTrans(C, 'chip', T) @ #i
+ & not(Ex #k . Started() @ #k)
+ & not(Ex #k . Corrupted(C) @ #k)
+ & not(Ex #k . RegisteredRole(T, 'chip') @ #k)
+ "
+
+// The chip finishes the protocol by itself
+// It does not register a terminal certificate and the terminal shouldn't be involved in the protocol execution
+// This should NOT be possible for the chip
+
+lemma nonRepudiation_chip: exists-trace
+ "Ex C T #i .
+ ValidTrans(T, 'terminal', C) @ #i
+ & not(Ex #k . Started() @ #k)
+ & not(Ex #k . Corrupted(T) @ #k)
+ & not(Ex #k . RegisteredRole(C, 'terminal') @ #k)
+ "
+
+// Perfect forward secrecy
+lemma pfs:
+ "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 & #m < #j)
+ & not(Ex #m . Corrupted(T) @ #m & #m < #j)
+ ==> (not(Ex #m . K(k) @ #m)
+ | (Ex #m . Revealed(sid) @ #m))
+ "
+
+
+#ifdef PFS
+rule Verify_Transcript_C:
+let
+ pkT = cert_pk(certT)
+ sid = <certT, certC, r2, cip, pkCe, cipe>
+ k = decaps(cip, skC)
+ ke = decaps(cipe, skCe)
+ kCNF_c = kdf(<'CNF', sid>, <k, ke>)
+in
+ [ In(<certT, IDc, r1, sT, certC, r2, pkCe, cip, sC, cipe, kCNF>), In(skCe), !Ltk(C, skC, 'chip') ]
+ --[ Eq(C, cert_id(certC)), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(sT, <'TA', IDc, r1>, pkT), true), Eq(verify(sC, <'CA', sid>, pkT), true), Eq(kCNF, kCNF_c), ValidTrans(C, 'chip', cert_id(certT)) ]->
+ [ ]
+#else
+rule Verify_Transcript_C:
+let
+ pkT = cert_pk(certT)
+ sid = <certT, certC, r2, cip>
+ kKDF = decaps(cip, skC)
+ kCNF_c = kdf(<'CNF', sid>, kKDF)
+in
+ [ In(<certT, IDc, r1, sT, certC, r2, cip, sC, kCNF>), !Ltk(C, skC, 'chip') ]
+ --[ Eq(C, cert_id(certC)), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(sT, <'TA', IDc, r1>, pkT), true), Eq(verify(sC, <'CA', sid>, pkT), true), Eq(kCNF, kCNF_c), ValidTrans(C, 'chip', cert_id(certT)) ]->
+ [ ]
+#endif
+
+#ifdef PFS
+rule Verify_Transcript_T:
+let
+ pkT = cert_pk(certT)
+ sid = <certT, certC, r2, cip, pkCe, cipe>
+ kCNF_t = kdf(<'CNF', sid>, <k, ke>)
+in
+ [ In(<certT, IDc, r1, sT, certC, r2, pkCe, cip, sC, cipe, kCNF>), In(<k, ke>) ]
+ --[ Eq(T, cert_id(certT)), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(sT, <'TA', IDc, r1>, pkT), true), Eq(verify(sC, <'CA', sid>, pkT), true), Eq(kCNF, kCNF_t), ValidTrans(T, 'terminal', cert_id(certC)) ]->
+ [ ]
+#else
+rule Verify_Transcript_T:
+let
+ pkT = cert_pk(certT)
+ sid = <certT, certC, r2, cip>
+ kCNF_t = kdf(<'CNF', sid>, kKDF)
+in
+ [ In(<certT, IDc, r1, sT, certC, r2, cip, sC, kCNF>), In(kKDF) ]
+ --[ Eq(T, cert_id(certT)), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(sT, <'TA', IDc, r1>, pkT), true), Eq(verify(sC, <'CA', sid>, pkT), true), Eq(kCNF, kCNF_t), ValidTrans(T, 'terminal', cert_id(certC)) ]->
+ [ ]
+#endif
+
+end
--
GitLab