Skip to content
Snippets Groups Projects
Commit fd9d4816 authored by Müller, Jonas's avatar Müller, Jonas
Browse files

Encrypt iid in KEM to match certC encryption layer

parent 525bf74e
Branches non-repudiation
Tags
No related merge requests found
...@@ -47,7 +47,7 @@ let ...@@ -47,7 +47,7 @@ let
in in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~r2), Fr(~skCe), Fr(~iid), !Cert($C, certC, 'chip') ] [ 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() ]-> --[ 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 #else
rule TA_CHALLENGE_C: rule TA_CHALLENGE_C:
let let
...@@ -61,7 +61,7 @@ let ...@@ -61,7 +61,7 @@ let
in in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~r2), Fr(~iid), !Cert($C, certC, 'chip') ] [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~r2), Fr(~iid), !Cert($C, certC, 'chip') ]
--[ Eq(verify_cert(certT, 'terminal'), true), Started() ]-> --[ 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 #endif
#ifdef PFS #ifdef PFS
...@@ -156,7 +156,7 @@ let ...@@ -156,7 +156,7 @@ let
kCNF = kdf(<'CNF', sid>, k) kCNF = kdf(<'CNF', sid>, k)
kKEY = kdf(<'KEY', sid>, k) kKEY = kdf(<'KEY', sid>, k)
in 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) ]-> --[ Eq(kCNF, kCNF_C), Completed(kKEY, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
[ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ] [ CAFinishT(cert_id(certC), $T, kKEY), !SessionReveal(sid, kKEY) ]
#endif #endif
......
...@@ -82,7 +82,7 @@ let ...@@ -82,7 +82,7 @@ let
in in
[ !Cert($C, certC, 'chip'), Fr(~r2), Fr(~skCe), TACompleteC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC) ] [ !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 #else
rule CA_INIT_C: rule CA_INIT_C:
let let
...@@ -91,7 +91,7 @@ let ...@@ -91,7 +91,7 @@ let
in in
[ !Cert($C, certC, 'chip'), Fr(~r2), TACompleteC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC) ] [ !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 #endif
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment