From 823db2c5303d8ccce6ecbe3b9d58533e4d892cfa Mon Sep 17 00:00:00 2001
From: jm71syxy <jonas.mueller.97@stud.tu-darmstadt.de>
Date: Wed, 19 Jun 2024 12:33:22 +0200
Subject: [PATCH] Fix missing T and pkCe in Verify_Transcript

---
 include/kem_verify_transcript.spthy | 4 ++--
 include/sig_verify_transcript.spthy | 6 ++----
 2 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/include/kem_verify_transcript.spthy b/include/kem_verify_transcript.spthy
index 7fe69d9..774a2f5 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 811c24f..c88f69e 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
-- 
GitLab