diff --git a/BasicEAC.spthy b/BasicEAC.spthy
deleted file mode 100644
index dfc0d9a3cbb34926708dadacb6c6d2207ac6834b..0000000000000000000000000000000000000000
--- a/BasicEAC.spthy
+++ /dev/null
@@ -1,308 +0,0 @@
-/*
-EAC Protocol
-======================================
-
-Author:  Jonas Mueller
-Date:    November 2023
-
-*/
-
-theory BasicEAC
-begin
-
-builtins: signing, diffie-hellman
-functions: cert/3, cert_pk/1, cert_sig/1, cert_id/1, ca_sk/0 [private]
-functions: mac/2, kdf_mac/2, kdf_enc/2
-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) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert)>, pk(ca_sk))
-
-
-
-rule Publish_ca_pk:
-    [ ]
-  -->
-    [ Out(pk(ca_sk)) ]
-
-
-// Registering a static long-term key for terminal
-rule Generate_static_ltk:
-let
-    pk = pk(~ltk)
-in
-    [ Fr(~ltk) ]
-  -->
-    [ !Pk($A, pk), !Ltk($A, ~ltk), Out(pk) ]
-
-// Registering a static diffie-hellman key for chip
-rule Generate_static_dh:
-let
-    pk = 'g'^~ltk
-in
-    [ Fr(~ltk) ]
-  -->
-    [ !PkDH($A, pk), !LtkDH($A, ~ltk), Out(pk) ]
-
-rule CA_Sign_ltk:
-let
-    certA = cert(pk, sign(<pk, A>, ca_sk), A)
-in
-    [ !Pk(A, pk) ]
-  -->
-    [ !Cert(A, certA), Out(certA) ]
-
-rule CA_Sign_dh:
-let
-    certA = cert(pk, sign(<pk, A>, ca_sk), A)
-in
-    [ !PkDH(A, pk) ]
-  -->
-    [ !CertDH(A, certA), Out(certA) ]
-
-
-/* Attacker model */
-
-rule Reveal_ltk:
-    [ !Ltk($A, ltk) ]
-  --[ Corrupted($A) ]->
-    [ Out(ltk) ]
-
-rule Reveal_dh:
-    [ !LtkDH($A, ltk) ]
-  --[ Corrupted($A) ]->
-    [ Out(ltk) ]
-
-rule Reveal_session:
-    [ !SessionReveal(uid, k) ]
-  --[ Revealed(uid) ]->
-    [ Out(k) ]
-
-
-
-/* Terminal Authentication */
-// State machine: TA_INIT_T -> TA_CHALLENGE_C -> TA_RESPONSE_T -> TA_COMPLETE_C
-
-
-rule TA_INIT_T:
-let
-    pkTe = 'g'^~skTe
-    msg1 = <certT, pkTe, 'TA_INIT', '1', 't'>
-in
-    [ !Cert($T, certT), Fr(~skTe), Fr(~iid) ] // skTe is ephemeral session key, iid is instance id of user $T
-  -->
-    [ 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
-rule TA_CHALLENGE_C:
-let
-    ca_pk = pk(ca_sk)
-    msg1 = <certT, pkTe, 'TA_INIT', '1', 't'>
-    msg2 = <~id_c, ~r1, 'TA_CHALLENGE', '2', 'c'>
-in
-    [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid) ]
-  --[ Eq(verify_cert(certT), true) ]->
-    [ Out(msg2), TAChallengeC(<$C, ~iid>, certT, pkTe, ~id_c, ~r1) ]
-
-rule TA_RESPONSE_T:
-let
-    msg2 = <id_c, r1, 'TA_CHALLENGE', '2', 'c'>
-    pkTe = 'g'^skTe
-    s = sign(<id_c, r1, pkTe>, ~skT)
-    msg3 = <s, 'TA_RESPONSE', '3', 't'>
-in
-    [ In(msg2), TAInitT(<$T, iid>, skTe), !Ltk($T, ~skT) ]
-  -->
-    [ Out(msg3), TAResponseT(<$T, iid>, skTe, id_c) ]
-
-rule TA_COMPLETE_C:
-let
-    msg3 = <s, 'TA_RESPONSE', '3', 't'>
-in
-    [ In(msg3), TAChallengeC(<$C, iid>, certT, pkTe, id_c, r1) ]
-  --[ Eq(verify(s, <id_c, r1, pkTe>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)) ]->
-    [ TACompleteC(<$C, iid>, certT, pkTe, id_c, r1) ]
-
-
-
-/* Chip Authentication */
-// State machine: CA_INIT_C -> CA_INIT_T -> CA_FINISH_C -> CA_FINISH_T
-
-rule CA_INIT_C:
-let
-    msg4 = <certC, 'CA_INIT', '4', 'c'>
-in
-    [ !CertDH($C, certC), Fr(~r2), TACompleteC(<$C, iid>, certT, pkTe, id_c, r1) ]
-  -->
-    [ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, ~r2) ] // Publish C's iid as its identity gets revealed through certC
-
-
-rule CA_INIT_T:
-let
-    pkTe = 'g'^skTe
-    msg4 = <certC, 'CA_INIT', '4', 'c'>
-    msg5 = <pkTe, 'CA_COMMIT', '5', 't'>
-in
-    [ In(msg4), TAResponseT(<$T, iid>, skTe, id_c) ]
-  --[ Eq(verify_cert(certC), true) ]->
-    [ Out(msg5), CAInitT(<$T, iid>, skTe, id_c, certC) ]
-
-
-rule CA_FINISH_C:
-let 
-    msg5 = <pkTe_t, 'CA_COMMIT', '5', 't'>
-    k = pkTe^~skC
-    kMac = kdf_mac(k, r2)
-    kEnc = kdf_enc(k, r2)
-    tag = mac(pkTe, kMac)
-    msg6 = <r2, tag, 'CA_RESPONSE', '6', 'c'>
-    sid = <certT, certC, pkTe, 'g'^~skC, id_c, r2, k>
-in
-    [ In(msg5), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, r2), !LtkDH($C, ~skC), !CertDH($C, certC) ]
-  --[ Eq(pkTe_t, pkTe), Completed(<kEnc, kMac>, sid, $C, 'chip', cert_id(certT)) ]->
-    [ Out(msg6), CAFinishC($C, cert_id(certT), kEnc) ]
-
-
-rule CA_FINISH_T:
-let
-    msg6 = <r2, tag, 'CA_RESPONSE', '6', 'c'>
-    pkTe = 'g'^skTe
-    pkC = cert_pk(certC)
-    k = pkC^skTe
-    kMac = kdf_mac(k, r2)
-    kEnc = kdf_enc(k, r2)
-    tag_T = mac(pkTe, kMac)
-    sid = <certT, certC, pkTe, pkC, id_c, r2, k>
-in
-    [ In(msg6), CAInitT(<$T, iid>, skTe, id_c, certC), !Cert($T, certT) ]
-  --[ Eq(tag, tag_T), Completed(<kEnc, kMac>, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
-    [ CAFinishT(cert_id(certC), $T, kEnc), !SessionReveal(<$T, iid>, skTe) ]
-
-
-
-
-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 iid #m . Revealed(<T, iid>) @ #m)
-        | (Ex #m . Corrupted(C) @ #m)
-  "
-
-// Cannot track chip after TA
-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))
-  "
-
-// Perfect forward secrecy
-lemma pfs:
-  "All A k sid role B #i #j .
-    Corrupted(A) @ #i
-    & Completed(k, sid, A, role, B) @ #j
-    & #j < #i
-    ==> not(Ex #m . K(k) @ #m)
-        | (Ex #m . (Corrupted(A) @ #m & #m < #j))
-        | (Ex #m . Corrupted(B) @ #m)
-        | (Ex iid #m . Revealed(<B, iid>) @ #m)
-        | (Ex iid #m . Revealed(<A, iid>) @ #m)
-  "
-*/
-
-end
-
diff --git a/ClassicEAC.spthy b/ClassicEAC.spthy
new file mode 100644
index 0000000000000000000000000000000000000000..87d968871719123f6e0e377aa73465e8fb042ba9
--- /dev/null
+++ b/ClassicEAC.spthy
@@ -0,0 +1,190 @@
+/*
+Classic EAC Protocol in tamarin
+======================================
+
+Author:  Jonas Mueller
+Date:    November 2023
+
+*/
+
+theory ClassicEAC
+begin
+
+builtins: signing, diffie-hellman
+functions: mac/2, kdf_mac/2, kdf_enc/2
+
+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) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert)>, pk(ca_sk))
+
+
+
+rule Publish_ca_pk:
+    [ ]
+  -->
+    [ Out(pk(ca_sk)) ]
+
+
+// Registering a static long-term key for terminal
+rule Generate_static_ltk:
+let
+    pk = pk(~ltk)
+in
+    [ Fr(~ltk) ]
+  -->
+    [ !Pk($A, pk), !Ltk($A, ~ltk), Out(pk) ]
+
+// Registering a static diffie-hellman key for chip
+rule Generate_static_dh:
+let
+    pk = 'g'^~ltk
+in
+    [ Fr(~ltk) ]
+  -->
+    [ !PkDH($A, pk), !LtkDH($A, ~ltk), Out(pk) ]
+
+rule CA_Sign_ltk:
+let
+    certA = cert(pk, sign(<pk, A>, ca_sk), A)
+in
+    [ !Pk(A, pk) ]
+  --[ Registered(A) ]->
+    [ !Cert(A, certA), Out(certA) ]
+
+rule CA_Sign_dh:
+let
+    certA = cert(pk, sign(<pk, A>, ca_sk), A)
+in
+    [ !PkDH(A, pk) ]
+  --[ Registered(A) ]->
+    [ !CertDH(A, certA), Out(certA) ]
+
+
+/* Attacker model */
+
+rule Reveal_ltk:
+    [ !Ltk($A, ltk) ]
+  --[ Corrupted($A) ]->
+    [ Out(ltk) ]
+
+rule Reveal_dh:
+    [ !LtkDH($A, ltk) ]
+  --[ Corrupted($A) ]->
+    [ Out(ltk) ]
+
+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
+    pkTe = 'g'^~skTe
+    msg1 = <certT, pkTe, '1', 't'>
+in
+    [ !Cert($T, certT), Fr(~skTe), Fr(~iid) ] // skTe is ephemeral session key, iid is instance id of user $T
+  -->
+    [ 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
+rule TA_CHALLENGE_C:
+let
+    msg1 = <certT, pkTe, '1', 't'>
+    msg2 = <~id_c, ~r1, '2', 'c'>
+in
+    [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid) ]
+  --[ Eq(verify_cert(certT), true) ]->
+    [ Out(msg2), TAChallengeC(<$C, ~iid>, certT, pkTe, ~id_c, ~r1) ]
+
+rule TA_RESPONSE_T:
+let
+    msg2 = <id_c, r1, '2', 'c'>
+    pkTe = 'g'^skTe
+    s = sign(<id_c, r1, pkTe>, ~skT)
+    msg3 = <s, '3', 't'>
+in
+    [ In(msg2), TAInitT(<$T, iid>, skTe), !Ltk($T, ~skT) ]
+  --[ Computed($T, 'terminal', s) ]->
+    [ Out(msg3), TAResponseT(<$T, iid>, skTe, id_c) ]
+
+rule TA_COMPLETE_C:
+let
+    msg3 = <s, '3', 't'>
+in
+    [ In(msg3), TAChallengeC(<$C, iid>, certT, pkTe, id_c, r1) ]
+  --[ Eq(verify(s, <id_c, r1, pkTe>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)) ]->
+    [ TACompleteC(<$C, iid>, certT, pkTe, id_c, r1) ]
+
+
+
+/* Chip Authentication */
+// State machine: CA_INIT_C -> CA_INIT_T -> CA_FINISH_C -> CA_FINISH_T
+
+rule CA_INIT_C:
+let
+    msg4 = <certC, '4', 'c'>
+in
+    [ !CertDH($C, certC), Fr(~r2), TACompleteC(<$C, iid>, certT, pkTe, id_c, r1) ]
+  -->
+    [ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, ~r2) ] // Publish C's iid as its identity gets revealed through certC
+
+
+rule CA_INIT_T:
+let
+    pkTe = 'g'^skTe
+    msg4 = <certC, '4', 'c'>
+    msg5 = <pkTe, '5', 't'>
+in
+    [ In(msg4), TAResponseT(<$T, iid>, skTe, id_c) ]
+  --[ Eq(verify_cert(certC), true) ]->
+    [ Out(msg5), CAInitT(<$T, iid>, skTe, id_c, certC) ]
+
+
+rule CA_FINISH_C:
+let 
+    msg5 = <pkTe_t, '5', 't'>
+    k = pkTe^~skC
+    kMac = kdf_mac(k, r2)
+    kEnc = kdf_enc(k, r2)
+    tag = mac(pkTe, kMac)
+    msg6 = <r2, tag, '6', 'c'>
+    sid = <certT, certC, pkTe, 'g'^~skC, id_c, r2>
+in
+    [ In(msg5), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, r2), !LtkDH($C, ~skC), !CertDH($C, certC) ]
+  --[ Eq(pkTe_t, pkTe), Computed($C, 'chip', <k, kMac, kEnc, tag>), Completed(<kEnc, kMac>, sid, $C, 'chip', cert_id(certT)) ]->
+    [ Out(msg6), CAFinishC($C, cert_id(certT), kEnc) ]
+
+
+rule CA_FINISH_T:
+let
+    msg6 = <r2, tag, '6', 'c'>
+    pkTe = 'g'^skTe
+    pkC = cert_pk(certC)
+    k = pkC^skTe
+    kMac = kdf_mac(k, r2)
+    kEnc = kdf_enc(k, r2)
+    tag_T = mac(pkTe, kMac)
+    sid = <certT, certC, pkTe, pkC, id_c, r2>
+in
+    [ In(msg6), CAInitT(<$T, iid>, skTe, id_c, certC), !Cert($T, certT) ]
+  --[ Eq(tag, tag_T), Computed($T, 'terminal', <k, kMac, kEnc, tag_T>), Completed(<kEnc, kMac>, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
+    [ CAFinishT(cert_id(certC), $T, kEnc), !SessionReveal(sid, <kEnc, kMac>) ]
+
+
+
+restriction OneCertPerIdentity:
+    "All id #i #j. Registered(id) @ #i & Registered(id) @ #j ==> #i = #j"
+
+restriction Equality:
+    "All x y #i. Eq(x, y) @ i ==> x = y"
+
+
+insert(lemmas.spthy)
+
+end
diff --git a/FastKemPQEAC.spthy b/FastKemPQEAC.spthy
new file mode 100644
index 0000000000000000000000000000000000000000..186c1f40d3dfb6c46cf1debefa93ba64f9fef000
--- /dev/null
+++ b/FastKemPQEAC.spthy
@@ -0,0 +1,210 @@
+/*
+PQ-EAC with Terminal Authentication through Long-Term KEM with reduced round-trip
+======================================
+
+Author:  Jonas Mueller
+Date:    May 2024
+
+*/
+
+theory FastKemPQEAC
+begin
+
+builtins: signing, symmetric-encryption
+functions: mac/2, kdf/2
+functions: encaps/2, decaps/2
+equations: decaps((encaps(k, pk(sk))), sk) = k
+
+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) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert)>, pk(ca_sk))
+
+
+
+rule Publish_ca_pk:
+    [ ]
+  -->
+    [ Out(pk(ca_sk)) ]
+
+
+// Registering a static long-term key for terminal
+rule Generate_static_ltk:
+let
+    pk = pk(~ltk)
+in
+    [ Fr(~ltk) ]
+  -->
+    [ !Pk($A, pk), !Ltk($A, ~ltk), Out(pk) ]
+
+rule CA_Sign_ltk:
+let
+    certA = cert(pk, sign(<pk, A>, ca_sk), A)
+in
+    [ !Pk(A, pk) ]
+  -->
+    [ !Cert(A, certA), Out(certA) ]
+
+
+/* Attacker model */
+
+rule Reveal_ltk:
+    [ !Ltk($A, ltk) ]
+  --[ Corrupted($A) ]->
+    [ Out(ltk) ]
+
+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), Fr(~iid) ]
+  -->
+    [ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ]
+
+#ifdef PFS
+rule TA_CHALLENGE_C:
+let
+    msg1 = <certT, '1', 't'>
+    cTA = encaps(~kTA, cert_pk(certT))
+    kTMAC = kdf(<'TMAC', ~r1>, ~kTA)
+    kTENC = kdf(<'TENC', ~r1>, ~kTA)
+    kTCNF = kdf(<'TCNF', ~r1>, ~kTA)
+    cCA = senc(<certC, ~r2, pk(~skCe)>, kTENC)
+    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) ]
+  --[ Eq(verify_cert(certT), true) ]->
+    [ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, ~skCe, kTMAC, kTCNF) ]
+#else
+rule TA_CHALLENGE_C:
+let
+    msg1 = <certT, '1', 't'>
+    cTA = encaps(~kTA, cert_pk(certT))
+    kTMAC = kdf(<'TMAC', ~r1>, ~kTA)
+    kTENC = kdf(<'TENC', ~r1>, ~kTA)
+    kTCNF = kdf(<'TCNF', ~r1>, ~kTA)
+    cCA = senc(<certC, ~r2>, kTENC)
+    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) ]
+  --[ Eq(verify_cert(certT), true) ]->
+    [ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, kTMAC, kTCNF) ]
+#endif
+
+#ifdef PFS
+rule TA_RESPONSE_T:
+let
+    msg2 = <id_c, r1, cTA, cCA, '2', 'c'>
+    kTA = decaps(cTA, ~skT)
+    kTMAC = kdf(<'TMAC', r1>, kTA)
+    kTENC = kdf(<'TENC', r1>, kTA)
+    kTCNF = kdf(<'TCNF', r1>, kTA)
+    dmesg = sdec(cCA, kTENC)
+    certC = fst(dmesg)
+    r2 = fst(snd(dmesg))
+    pkCe = snd(snd(dmesg))
+    pkC = cert_pk(certC)
+    cip = encaps(~k, pkC)
+    cipe = encaps(~ke, pkCe)
+    sid = <certT, certC, r2, cip, pkCe, cipe>
+    s = mac(<'CA', sid>, kTMAC)
+    msg3 = <kTCNF, cip, s, cipe, '3', 't'>
+in
+    [ In(msg2), Fr(~k), Fr(~ke), TAInitT(<$T, iid>), !Ltk($T, ~skT), !Cert($T, certT) ]
+  --[ Eq(verify_cert(certC), true) ]->
+    [ Out(msg3), TAResponseT(<$T, iid>, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ]
+#else
+rule TA_RESPONSE_T:
+let
+    msg2 = <id_c, r1, cTA, cCA, '2', 'c'>
+    kTA = decaps(cTA, ~skT)
+    kTMAC = kdf(<'TMAC', r1>, kTA)
+    kTENC = kdf(<'TENC', r1>, kTA)
+    kTCNF = kdf(<'TCNF', r1>, kTA)
+    dmesg = sdec(cCA, kTENC)
+    certC = fst(dmesg)
+    r2 = snd(dmesg)
+    pkC = cert_pk(certC)
+    cip = encaps(~k, pkC)
+    sid = <certT, certC, r2, cip>
+    s = mac(<'CA', sid>, kTMAC)
+    msg3 = <kTCNF, cip, s, '3', 't'>
+in
+    [ In(msg2), Fr(~k), TAInitT(<$T, iid>), !Ltk($T, ~skT), !Cert($T, certT) ]
+  --[ Eq(verify_cert(certC), true) ]->
+    [ Out(msg3), TAResponseT(<$T, iid>, id_c, certC, r2, <~k, cip>) ]
+#endif
+
+#ifdef PFS
+rule TA_COMPLETE_C:
+let
+    msg3 = <kTCNF_T, cip, s, cipe, '3', '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>)
+    msg4 = <kCNF, '4', 'c'>
+in
+    [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, r2, skCe, kTMAC, kTCNF), !Ltk($C, ~skC), !Cert($C, certC) ]
+  --[ Eq(kTCNF_T, kTCNF), Eq(s, mac(<'CA', sid>, kTMAC)), CompletedTA($C, iid, cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
+    [ Out(msg4), TACompleteC(<$C, iid>, kKEY) ]
+#else
+rule TA_COMPLETE_C:
+let
+    msg3 = <kTCNF_T, cip, s, '3', 't'>
+    sid = <certT, certC, r2, cip>
+    k = decaps(cip, ~skC)
+    kCNF = kdf(<'CNF', sid>, k)
+    kKEY = kdf(<'KEY', sid>, k)
+    msg4 = <kCNF, '4', 'c'>
+in
+    [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, r2, kTMAC, kTCNF), !Ltk($C, ~skC), !Cert($C, certC) ]
+  --[ Eq(kTCNF_T, kTCNF), Eq(s, mac(<'CA', sid>, kTMAC)), CompletedTA($C, iid, cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
+    [ Out(msg4), TACompleteC(<$C, iid>, kKEY) ]
+#endif
+
+#ifdef PFS
+rule CA_FINISH_T:
+let
+    msg4 = <kCNF_C, '4', 'c'>
+    sid = <certT, certC, r2, cip, pkCe, cipe>
+    kCNF = kdf(<'CNF', sid>, <k, ke>)
+    kKEY = kdf(<'KEY', sid>, <k, ke>)
+in
+    [ In(msg4), TAResponseT(<$T, iid>, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT) ]
+  --[ 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
+    msg4 = <kCNF_C, '4', 'c'>
+    sid = <certT, certC, r2, cip>
+    kCNF = kdf(<'CNF', sid>, k)
+    kKEY = kdf(<'KEY', sid>, k)
+in
+    [ In(msg4), TAResponseT(<$T, iid>, id_c, certC, r2, <k, cip>), !Cert($T, certT) ]
+  --[ Eq(kCNF, kCNF_C), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
+    [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ]
+#endif
+
+
+
+
+
+restriction Equality:
+    "All x y #i. Eq(x, y) @ i ==> x = y"
+
+insert(lemmas.spthy)
+
+end
diff --git a/FastSigPQEAC.spthy b/FastSigPQEAC.spthy
new file mode 100644
index 0000000000000000000000000000000000000000..48a3cad0f28fb681852d668b0f6b205850b9048b
--- /dev/null
+++ b/FastSigPQEAC.spthy
@@ -0,0 +1,186 @@
+/*
+PQ-EAC with Terminal Signatures and reduced round-trip
+======================================
+
+Author:  Jonas Mueller
+Date:    May 2024
+
+*/
+
+theory FastSigPQEAC
+begin
+
+builtins: signing
+functions: kdf/2
+functions: encaps/2, decaps/2
+equations: decaps((encaps(k, pk(sk))), sk) = k
+
+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) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert)>, pk(ca_sk))
+
+
+
+rule Publish_ca_pk:
+    [ ]
+  -->
+    [ Out(pk(ca_sk)) ]
+
+
+// Registering a static long-term key for terminal
+rule Generate_static_ltk:
+let
+    pk = pk(~ltk)
+in
+    [ Fr(~ltk) ]
+  -->
+    [ !Pk($A, pk), !Ltk($A, ~ltk), Out(pk) ]
+
+rule CA_Sign_ltk:
+let
+    certA = cert(pk, sign(<pk, A>, ca_sk), A)
+in
+    [ !Pk(A, pk) ]
+  -->
+    [ !Cert(A, certA), Out(certA) ]
+
+
+/* Attacker model */
+
+rule Reveal_ltk:
+    [ !Ltk($A, ltk) ]
+  --[ Corrupted($A) ]->
+    [ Out(ltk) ]
+
+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), Fr(~iid) ]
+  -->
+    [ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ]
+
+#ifdef PFS
+rule TA_CHALLENGE_C:
+let
+    msg1 = <certT, '1', 't'>
+    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) ]
+  --[ Eq(verify_cert(certT), true) ]->
+    [ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~skCe, ~r2) ]
+#else
+rule TA_CHALLENGE_C:
+let
+    msg1 = <certT, '1', 't'>
+    msg2 = <~id_c, ~r1, certC, ~r2, '2', 'c'>
+in
+    [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid), Fr(~r2), !Cert($C, certC) ]
+  --[ Eq(verify_cert(certT), true) ]->
+    [ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2) ]
+#endif
+
+#ifdef PFS
+rule TA_RESPONSE_T:
+let
+    msg2 = <id_c, r1, certC, r2, pkCe, '2', 'c'>
+    s1 = sign(<'TA', id_c, r1>, ~skT)
+    pkC = cert_pk(certC)
+    cip = encaps(~k, pkC)
+    cipe = encaps(~ke, pkCe)
+    sid = <certT, certC, r2, cip, pkCe, cipe>
+    s2 = sign(<'CA', sid>, ~skT)
+    msg3 = <cip, cipe, s1, s2, '3', 't'>
+in
+    [ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT), !Cert($T, certT), Fr(~k), Fr(~ke) ]
+  --[ Eq(verify_cert(certC), true) ]->
+    [ Out(msg3), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ]
+#else
+rule TA_RESPONSE_T:
+let
+    msg2 = <id_c, r1, certC, r2, '2', 'c'>
+    s1 = sign(<'TA', id_c, r1>, ~skT)
+    pkC = cert_pk(certC)
+    cip = encaps(~k, pkC)
+    sid = <certT, certC, r2, cip>
+    s2 = sign(<'CA', sid>, ~skT)
+    msg3 = <cip, s1, s2, '3', 't'>
+in
+    [ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT), !Cert($T, certT), Fr(~k) ]
+  --[ Eq(verify_cert(certC), true) ]->
+    [ Out(msg3), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>) ]
+#endif
+
+#ifdef PFS
+rule TA_COMPLETE_C:
+let
+    msg3 = <cip, cipe, s1, s2, '3', '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>)
+    msg4 = <kCNF, '4', 'c'>
+in
+    [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, skCe, r2), !Ltk($C, ~skC), !Cert($C, certC) ]
+  --[ Eq(verify(s1, <'TA', id_c, r1>, cert_pk(certT)), true), Eq(verify(s2, <'CA', sid>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
+    [ Out(msg4), TACompleteC(<$C, iid>, certT, id_c, r1, skCe, r2) ]
+#else
+rule TA_COMPLETE_C:
+let
+    msg3 = <cip, s1, s2, '3', 't'>
+    sid = <certT, certC, r2, cip>
+    k = decaps(cip, ~skC)
+    kCNF = kdf(<'CNF', sid>, k)
+    kKEY = kdf(<'KEY', sid>, k)
+    msg4 = <kCNF, '4', 'c'>
+in
+    [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, r2), !Ltk($C, ~skC), !Cert($C, certC) ]
+  --[ Eq(verify(s1, <'TA', id_c, r1>, cert_pk(certT)), true), Eq(verify(s2, <'CA', sid>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
+    [ Out(msg4), TACompleteC(<$C, iid>, certT, id_c, r1, r2) ]
+#endif
+
+#ifdef PFS
+rule CA_FINISH_T:
+let
+    msg4 = <kCNF_C, '4', 'c'>
+    sid = <certT, certC, r2, cip, pkCe, cipe>
+    kCNF = kdf(<'CNF', sid>, <k, ke>)
+    kKEY = kdf(<'KEY', sid>, <k, ke>)
+in
+    [ In(msg4), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT) ]
+  --[ 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
+    msg4 = <kCNF_C, '4', 'c'>
+    sid = <certT, certC, r2, cip>
+    kCNF = kdf(<'CNF', sid>, k)
+    kKEY = kdf(<'KEY', sid>, k)
+in
+    [ In(msg4), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>), !Cert($T, certT) ]
+  --[ Eq(kCNF, kCNF_C), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
+    [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ]
+#endif
+
+
+
+
+restriction Equality:
+    "All x y #i. Eq(x, y) @ i ==> x = y"
+
+insert(lemmas.spthy)
+
+end
diff --git a/InsertLemmas.py b/InsertLemmas.py
new file mode 100644
index 0000000000000000000000000000000000000000..93f20e331b52e431cc6bdade9f30874347694580
--- /dev/null
+++ b/InsertLemmas.py
@@ -0,0 +1,13 @@
+import sys, re
+pattern = re.compile(r"insert\((.*)\)")
+
+out = open('tmp.spthy', 'w')
+
+for i, line in enumerate(open(sys.argv[1])):
+    match = re.search(pattern, line)
+    if match:
+        for line in open(match.group(1)):
+            out.write(line)
+    else:
+        out.write(line)
+
diff --git a/KemPQEAC.spthy b/KemPQEAC.spthy
new file mode 100644
index 0000000000000000000000000000000000000000..227f0cfc7a9382ec8a93f6d97a0dee0d64bf8c45
--- /dev/null
+++ b/KemPQEAC.spthy
@@ -0,0 +1,233 @@
+/*
+PQ-EAC with Terminal Authentication through Long-Term KEM
+======================================
+
+Author:  Jonas Mueller
+Date:    May 2024
+
+*/
+
+theory KemPQEAC
+begin
+
+builtins: signing, symmetric-encryption
+functions: mac/2, kdf/2
+functions: encaps/2, decaps/2
+equations: decaps((encaps(k, pk(sk))), sk) = k
+
+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) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert)>, pk(ca_sk))
+
+
+
+rule Publish_ca_pk:
+    [ ]
+  -->
+    [ Out(pk(ca_sk)) ]
+
+
+// Registering a static long-term key for terminal
+rule Generate_static_ltk:
+let
+    pk = pk(~ltk)
+in
+    [ Fr(~ltk) ]
+  -->
+    [ !Pk($A, pk), !Ltk($A, ~ltk), Out(pk) ]
+
+rule CA_Sign_ltk:
+let
+    certA = cert(pk, sign(<pk, A>, ca_sk), A)
+in
+    [ !Pk(A, pk) ]
+  -->
+    [ !Cert(A, certA), Out(certA) ]
+
+
+/* Attacker model */
+
+rule Reveal_ltk:
+    [ !Ltk($A, ~ltk) ]
+  --[ Corrupted($A) ]->
+    [ Out(~ltk) ]
+
+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), Fr(~iid) ]
+  -->
+    [ 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'>
+    cTA = encaps(~kTA, cert_pk(certT))
+    msg2 = <~id_c, ~r1, cTA, '2', 'c'>
+in
+    [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~iid) ]
+  --[ Eq(verify_cert(certT), true) ]->
+    [ Out(msg2), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, <~kTA, cTA>) ]
+
+rule TA_RESPONSE_T:
+let
+    msg2 = <id_c, r1, cTA, '2', 'c'>
+    kTA = decaps(cTA, ~skT)
+    kTMAC = kdf(<'TMAC', r1>, kTA)
+    kTENC = kdf(<'TENC', r1>, kTA)
+    kTCNF = kdf(<'TCNF', r1>, kTA)
+    msg3 = <kTCNF, '3', 't'>
+in
+    [ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT) ]
+  -->
+    [ Out(msg3), TAResponseT(<$T, iid>, id_c, kTMAC, kTENC) ]
+
+rule TA_COMPLETE_C:
+let
+    msg3 = <kTCNF_T, '3', 't'>
+    kTMAC = kdf(<'TMAC', r1>, kTA)
+    kTENC = kdf(<'TENC', r1>, kTA)
+    kTCNF = kdf(<'TCNF', r1>, kTA)
+in
+    [ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, <kTA, cTA>) ]
+  --[ Eq(kTCNF_T, kTCNF), CompletedTA($C, iid, cert_id(certT)) ]->
+    [ TACompleteC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC) ]
+
+
+
+/* Chip Authentication */
+// State machine: CA_INIT_C -> CA_INIT_T -> CA_FINISH_C -> CA_FINISH_T
+
+#ifdef PFS
+rule CA_INIT_C:
+let
+    cCA = senc(<certC, ~r2, pk(~skCe)>, kTENC)
+    msg4 = <cCA, '4', 'c'>
+in
+    [ !Cert($C, certC), Fr(~r2), Fr(~skCe), TACompleteC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC) ]
+  -->
+    [ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, ~r2, ~skCe) ]
+#else
+rule CA_INIT_C:
+let
+    cCA = senc(<certC, ~r2>, kTENC)
+    msg4 = <cCA, '4', 'c'>
+in
+    [ !Cert($C, certC), Fr(~r2), TACompleteC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC) ]
+  -->
+    [ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, ~r2) ]
+#endif
+
+
+#ifdef PFS
+rule CA_INIT_T:
+let
+    msg4 = <cCA, '4', 'c'>
+    dmesg = sdec(cCA, kTENC)
+    certC = fst(dmesg)
+    r2 = fst(snd(dmesg))
+    pkCe = snd(snd(dmesg))
+    pkC = cert_pk(certC)
+    cip = encaps(~k, pkC)
+    cipe = encaps(~ke, pkCe)
+    sid = <certT, certC, r2, cip, pkCe, cipe>
+    s = mac(<'CA', sid>, kTMAC)
+    msg5 = <cip, s, cipe, '5', 't'>
+in
+    [ In(msg4), TAResponseT(<$T, iid>, id_c, kTMAC, kTENC), !Cert($T, certT), Fr(~k), Fr(~ke) ]
+  --[ Eq(verify_cert(certC), true) ]->
+    [ Out(msg5), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ]
+#else
+rule CA_INIT_T:
+let
+    msg4 = <cCA, 'CA_INIT', '4', 'c'>
+    dmesg = sdec(cCA, kTENC)
+    certC = fst(dmesg)
+    r2 = snd(dmesg)
+    pkC = cert_pk(certC)
+    cip = encaps(~k, pkC)
+    sid = <certT, certC, r2, cip>
+    s = mac(<'CA', sid>, kTMAC)
+    msg5 = <cip, s, '5', 't'>
+in
+    [ In(msg4), TAResponseT(<$T, iid>, id_c, kTMAC, kTENC), !Cert($T, certT), Fr(~k) ]
+  --[ Eq(verify_cert(certC), true) ]->
+    [ Out(msg5), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, 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, <kTA, cTA>, kTMAC, kTENC, r2, skCe), !Ltk($C, ~skC), !Cert($C, certC) ]
+  --[ Eq(s, mac(<'CA', sid>, kTMAC)), 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, <kTA, cTA>, kTMAC, kTENC, r2), !Ltk($C, ~skC), !Cert($C, certC) ]
+  --[ Eq(s, mac(<'CA', sid>, kTMAC)), 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, kTMAC, kTENC, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT) ]
+  --[ 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, kTMAC, kTENC, certC, r2, <k, cip>), !Cert($T, certT) ]
+  --[ Eq(kCNF, kCNF_c), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
+    [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ]
+#endif
+
+
+
+restriction Equality:
+    "All x y #i. Eq(x, y) @ i ==> x = y"
+
+insert(lemmas.spthy)
+
+end
diff --git a/SigPQEAC.spthy b/SigPQEAC.spthy
new file mode 100644
index 0000000000000000000000000000000000000000..2150cf6566d100ea4d11a9080da49ca73faf580f
--- /dev/null
+++ b/SigPQEAC.spthy
@@ -0,0 +1,217 @@
+/*
+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
+
+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) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert)>, pk(ca_sk))
+
+
+
+rule Publish_ca_pk:
+    [ ]
+  -->
+    [ Out(pk(ca_sk)) ]
+
+
+// Registering a static long-term key for terminal
+rule Generate_static_ltk:
+let
+    pk = pk(~ltk)
+in
+    [ Fr(~ltk) ]
+  -->
+    [ !Pk($A, pk), !Ltk($A, ~ltk), Out(pk) ]
+
+rule CA_Sign_ltk:
+let
+    certA = cert(pk, sign(<pk, A>, ca_sk), A)
+in
+    [ !Pk(A, pk) ]
+  -->
+    [ !Cert(A, certA), Out(certA) ]
+
+
+/* Attacker model */
+
+rule Reveal_ltk:
+    [ !Ltk($A, ltk) ]
+  --[ Corrupted($A) ]->
+    [ Out(ltk) ]
+
+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), Fr(~iid) ]
+  -->
+    [ 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), true) ]->
+    [ 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) ]
+  -->
+    [ 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) ]
+  -->
+    [ 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) ]
+  -->
+    [ 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), !Cert($T, certT) ]
+  --[ Eq(verify_cert(certC), 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), !Cert($T, certT) ]
+  --[ Eq(verify_cert(certC), 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), !Cert($C, certC) ]
+  --[ 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), !Cert($C, certC) ]
+  --[ 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) ]
+  --[ 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) ]
+  --[ Eq(kCNF, kCNF_c), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
+    [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ]
+#endif
+
+
+
+
+restriction Equality:
+    "All x y #i. Eq(x, y) @ i ==> x = y"
+
+insert(lemmas.spthy)
+
+end
diff --git a/lemmas.spthy b/lemmas.spthy
new file mode 100644
index 0000000000000000000000000000000000000000..41cde129e8fc8c5559186124c1f5b294b51ee7b5
--- /dev/null
+++ b/lemmas.spthy
@@ -0,0 +1,126 @@
+// 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))
+  "
+
+/*
+lemma nonRepudiation:
+  "All sid #n .
+     Finished(sid) @ #n
+     ==> (Ex T data #m . Computed(T, 'terminal', data) @ #m
+          & not(Ex #k . K(data) @ #k & #k < #m)
+          & not(Ex #k . Corrupted(T) @ #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))
+  "
+