diff --git a/FastKemPQEAC.spthy b/FastKemPQEAC.spthy index f316e188f212f3a2864de392f113f100f5a81f3f..53c36b0b7bd07a0fb1a32583b96a38f87677000a 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 6c46f4914bb4155edd6bd67a7b2cc38124bdceed..deec49730950fcfcea3e531b6aa0f75b0af6224b 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