Fix missing T and pkCe in Verify_Transcript

include/kem_verify_transcript.spthy

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

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