Add one-sided protocol simulation approach

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

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)

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)
 

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)
 

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)

include/classic_verify_transcript.spthy

+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)) ]->
+    [  ]
+

include/kem_verify_transcript.spthy

+#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

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:

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) ]

include/sig_verify_transcript.spthy

+#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

tmp.spthy

+/*
+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