diff --git a/ClassicEAC.spthy b/ClassicEAC.spthy
index 33173fc4703e1a921b93aa097a160985a13ccc79..1beea11e09343f38c60c63b055cd01d1dcdacd80 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 91ad6f0d0a0d247414d04b18955a4e6a3c9f1ccb..f316e188f212f3a2864de392f113f100f5a81f3f 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 0e101cd4c2de739f73c6d4c60062840c411ca05f..5b4f4cd09e44edbc1ab4ea8438a9e5541faede88 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 f17d6b454a28b5ff72d8eac6bd24ce052dd1b54b..6c46f4914bb4155edd6bd67a7b2cc38124bdceed 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 6ef2ee1817450f35c3a672e81ef1dded6a0a1551..9ad48e51b79a478f921874780cc62829ca4da660 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 0000000000000000000000000000000000000000..2453ba39ee7ae96b4e400363344850bd4fefd1e9
--- /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 0000000000000000000000000000000000000000..7fe69d97ee8ef148e9e21e82b66d82cfb392efe3
--- /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 b7d47edd04c89328adbf64f3252677c5e912c7d9..73ffbba17156908bd2d821c2950f5f18d2303e0a 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 79031874c7f21e8549ad24b5fa0fb6ca1eb6563c..ad51ad879674e71ed3b8423768e36764d9582dec 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 0000000000000000000000000000000000000000..811c24fb0f0a779d5a374badb8d552a2e2b266d1
--- /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 0000000000000000000000000000000000000000..9d54c88e2becae6d230b02717febc3958346f436
--- /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