diff --git a/include/kem_verify_transcript.spthy b/include/kem_verify_transcript.spthy
index 7fe69d97ee8ef148e9e21e82b66d82cfb392efe3..774a2f5f7a8aa99eb7cecc7219cecf5fa9e5baef 100644
--- a/include/kem_verify_transcript.spthy
+++ b/include/kem_verify_transcript.spthy
@@ -1,6 +1,7 @@
 #ifdef PFS
 rule Verify_Transcript_C:
 let
+    pkCe = pk(skCe)
     kTMAC = kdf(<'TMAC', r1>, kTA)
     kTENC = kdf(<'TENC', r1>, kTA)
     kTCNF_c = kdf(<'TCNF', r1>, kTA)
@@ -24,8 +25,7 @@ let
     kTCNF_c = kdf(<'TCNF', r1>, kTA)
     dmesg = sdec(cCA, kTENC)
     certC = fst(dmesg)
-    r2 = fst(snd(dmesg))
-    pkCe = snd(snd(dmesg))
+    r2 = snd(dmesg)
     sid = <certT, certC, r2, cip>
     s_c = mac(<'CA', sid>, kTMAC)
     kKDF = decaps(cip, skC)
diff --git a/include/sig_verify_transcript.spthy b/include/sig_verify_transcript.spthy
index 811c24fb0f0a779d5a374badb8d552a2e2b266d1..c88f69e31568064798fdaa7cd6c46762baff761a 100644
--- a/include/sig_verify_transcript.spthy
+++ b/include/sig_verify_transcript.spthy
@@ -26,21 +26,19 @@ in
 #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>) ]
+    [ In(<certT, IDc, r1, sT, certC, r2, pkCe, cip, sC, cipe, kCNF>), In(<k, ke>), !Pk(T, pkT, 'terminal') ]
   --[ 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) ]
+    [ In(<certT, IDc, r1, sT, certC, r2, cip, sC, kCNF>), In(kKDF), !Pk(T, pkT, 'terminal') ]
   --[ 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