From fd9d4816f97984cef268558c66fa6c1007ee425e Mon Sep 17 00:00:00 2001
From: jm71syxy <jonas.mueller.97@stud.tu-darmstadt.de>
Date: Wed, 19 Jun 2024 09:11:45 +0200
Subject: [PATCH] Encrypt iid in KEM to match certC encryption layer
---
FastKemPQEAC.spthy | 6 +++---
KemPQEAC.spthy | 4 ++--
2 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/FastKemPQEAC.spthy b/FastKemPQEAC.spthy
index f316e18..53c36b0 100644
--- a/FastKemPQEAC.spthy
+++ b/FastKemPQEAC.spthy
@@ -47,7 +47,7 @@ let
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), Started() ]->
- [ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, ~skCe, kTMAC, kTCNF) ]
+ [ Out(msg2), Out(senc(~iid, kTENC)), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, ~skCe, kTMAC, kTCNF) ]
#else
rule TA_CHALLENGE_C:
let
@@ -61,7 +61,7 @@ let
in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~r2), Fr(~iid), !Cert($C, certC, 'chip') ]
--[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
- [ Out(msg2), Out(~iid), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, kTMAC, kTCNF) ]
+ [ Out(msg2), Out(senc(~iid, kTENC)), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, kTMAC, kTCNF) ]
#endif
#ifdef PFS
@@ -156,7 +156,7 @@ let
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) ]
+ [ In(msg4), TAResponseT(<$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
diff --git a/KemPQEAC.spthy b/KemPQEAC.spthy
index 6c46f49..deec497 100644
--- a/KemPQEAC.spthy
+++ b/KemPQEAC.spthy
@@ -82,7 +82,7 @@ let
in
[ !Cert($C, certC, 'chip'), 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) ]
+ [ Out(msg4), Out(senc(iid, kTENC)), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, ~r2, ~skCe) ]
#else
rule CA_INIT_C:
let
@@ -91,7 +91,7 @@ let
in
[ !Cert($C, certC, 'chip'), 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) ]
+ [ Out(msg4), Out(senc(iid, kTENC)), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, ~r2) ]
#endif
--
GitLab