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

Remove chip hiding property and add forward secrecy for terminal ltk

parent 2bccaf0b
Branches
No related tags found
No related merge requests found
Expand all Show whitespace changes
Inline Side-by-side
Showing
with 1876 additions and 2124 deletions
ClassicEAC.spthy
+ 21
− 21
View file @ e7f75533
...@@ -31,9 +31,9 @@ let ...@@ -31,9 +31,9 @@ let
pkTe = 'g'^~skTe pkTe = 'g'^~skTe
msg1 = <certT, pkTe, '1', 't'> msg1 = <certT, pkTe, '1', 't'>
in in
[ !Cert($T, certT, 'terminal'), Fr(~skTe), Fr(~iid) ] // skTe is ephemeral session key, iid is instance id of user $T [ !Cert($T, certT, 'terminal'), Fr(~skTe) ] // skTe is ephemeral session key
--[ Started() ]-> --[ Started() ]->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>, ~skTe) ] // Publish T's iid as its identity gets revealed through certT [ Out(msg1), TAInitT($T, ~skTe) ]
// We generate a fresh IDc to simulate the previous execution of PACE or BAC // We generate a fresh IDc to simulate the previous execution of PACE or BAC
rule TA_CHALLENGE_C: rule TA_CHALLENGE_C:
...@@ -41,9 +41,9 @@ let ...@@ -41,9 +41,9 @@ let
msg1 = <certT, pkTe, '1', 't'> msg1 = <certT, pkTe, '1', 't'>
msg2 = <~id_c, ~r1, '2', 'c'> msg2 = <~id_c, ~r1, '2', 'c'>
in in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid) ] [ In(msg1), Fr(~r1), Fr(~id_c) ]
--[ Eq(verify_cert(certT, 'terminal'), true), Started() ]-> --[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
[ Out(msg2), TAChallengeC(<$C, ~iid>, certT, pkTe, ~id_c, ~r1) ] [ Out(msg2), TAChallengeC($C, certT, pkTe, ~id_c, ~r1) ]
rule TA_RESPONSE_T: rule TA_RESPONSE_T:
let let
...@@ -52,17 +52,17 @@ let ...@@ -52,17 +52,17 @@ let
s = sign(<id_c, r1, pkTe>, ~skT) s = sign(<id_c, r1, pkTe>, ~skT)
msg3 = <s, '3', 't'> msg3 = <s, '3', 't'>
in in
[ In(msg2), TAInitT(<$T, iid>, skTe), !Ltk($T, ~skT, 'terminal') ] [ In(msg2), TAInitT($T, skTe), !Ltk($T, ~skT, 'terminal') ]
--> -->
[ Out(msg3), TAResponseT(<$T, iid>, skTe, id_c) ] [ Out(msg3), TAResponseT($T, skTe, id_c) ]
rule TA_COMPLETE_C: rule TA_COMPLETE_C:
let let
msg3 = <s, '3', 't'> msg3 = <s, '3', 't'>
in in
[ In(msg3), TAChallengeC(<$C, iid>, certT, pkTe, id_c, r1) ] [ In(msg3), TAChallengeC($C, certT, pkTe, id_c, r1) ]
--[ Eq(verify(s, <id_c, r1, pkTe>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)) ]-> --[ Eq(verify(s, <id_c, r1, pkTe>, cert_pk(certT)), true) ]->
[ TACompleteC(<$C, iid>, certT, pkTe, id_c, r1) ] [ TACompleteC($C, certT, pkTe, id_c, r1) ]
...@@ -73,9 +73,9 @@ rule CA_INIT_C: ...@@ -73,9 +73,9 @@ rule CA_INIT_C:
let let
msg4 = <certC, ~r2, '4', 'c'> msg4 = <certC, ~r2, '4', 'c'>
in in
[ !Cert($C, certC, 'chip'), Fr(~r2), TACompleteC(<$C, iid>, certT, pkTe, id_c, r1) ] [ !Cert($C, certC, 'chip'), Fr(~r2), TACompleteC($C, certT, pkTe, id_c, r1) ]
--> -->
[ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, ~r2) ] // Publish C's iid as its identity gets revealed through certC [ Out(msg4), CAInitC($C, certT, pkTe, id_c, r1, ~r2) ]
rule CA_INIT_T: rule CA_INIT_T:
...@@ -84,9 +84,9 @@ let ...@@ -84,9 +84,9 @@ let
msg4 = <certC, r2, '4', 'c'> msg4 = <certC, r2, '4', 'c'>
msg5 = <pkTe, '5', 't'> msg5 = <pkTe, '5', 't'>
in in
[ In(msg4), TAResponseT(<$T, iid>, skTe, id_c) ] [ In(msg4), TAResponseT($T, skTe, id_c) ]
--[ Eq(verify_cert(certC, 'chip'), true) ]-> --[ Eq(verify_cert(certC, 'chip'), true) ]->
[ Out(msg5), CAInitT(<$T, iid>, skTe, id_c, certC) ] [ Out(msg5), CAInitT($T, skTe, id_c, certC) ]
rule CA_FINISH_C: rule CA_FINISH_C:
...@@ -95,13 +95,13 @@ let ...@@ -95,13 +95,13 @@ let
k = pkTe^~skC k = pkTe^~skC
kMac = kdf_mac(k, r2) kMac = kdf_mac(k, r2)
kEnc = kdf_enc(k, r2) kEnc = kdf_enc(k, r2)
sid = <certT, certC, pkTe, 'g'^~skC, id_c, r2>
tag = mac(pkTe, kMac) tag = mac(pkTe, kMac)
msg6 = <r2, tag, '6', 'c'> msg6 = <r2, tag, '6', 'c'>
sid = <certT, certC, pkTe, 'g'^~skC, id_c, r2>
in in
[ In(msg5), CAInitC(<$C, iid>, certT, pkTe, id_c, r1, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] [ In(msg5), CAInitC($C, certT, pkTe, id_c, r1, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ]
--[ Eq(pkTe_t, pkTe), Completed(<kEnc, kMac>, sid, $C, 'chip', cert_id(certT)) ]-> --[ Eq(pkTe_t, pkTe), Completed(kEnc, sid, $C, 'chip', cert_id(certT)) ]->
[ Out(msg6), CAFinishC($C, cert_id(certT), kEnc) ] [ Out(msg6) ]
rule CA_FINISH_T: rule CA_FINISH_T:
...@@ -112,12 +112,12 @@ let ...@@ -112,12 +112,12 @@ let
k = pkC^skTe k = pkC^skTe
kMac = kdf_mac(k, r2) kMac = kdf_mac(k, r2)
kEnc = kdf_enc(k, r2) kEnc = kdf_enc(k, r2)
tag_T = mac(pkTe, kMac)
sid = <certT, certC, pkTe, pkC, id_c, r2> sid = <certT, certC, pkTe, pkC, id_c, r2>
tag_T = mac(pkTe, kMac)
in in
[ In(msg6), CAInitT(<$T, iid>, skTe, id_c, certC), !Cert($T, certT, 'terminal') ] [ In(msg6), CAInitT($T, skTe, id_c, certC), !Cert($T, certT, 'terminal') ]
--[ Eq(tag, tag_T), Completed(<kEnc, kMac>, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]-> --[ Eq(tag, tag_T), Completed(kEnc, sid, $T, 'terminal', cert_id(certC)), Finished(sid) ]->
[ CAFinishT(cert_id(certC), $T, kEnc), !SessionReveal(sid, <kEnc, kMac>) ] [ !SessionReveal(sid, kEnc) ]
insert(include/classic_verify_transcript.spthy) insert(include/classic_verify_transcript.spthy)
......
FastKemPQEAC.spthy
+ 24
− 24
View file @ e7f75533
...@@ -30,11 +30,11 @@ rule TA_INIT_T: ...@@ -30,11 +30,11 @@ rule TA_INIT_T:
let let
msg1 = <certT, '1', 't'> msg1 = <certT, '1', 't'>
in in
[ !Cert($T, certT, 'terminal'), Fr(~iid) ] [ !Cert($T, certT, 'terminal') ]
--[ Started() ]-> --[ Started() ]->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ] [ Out(msg1), TAInitT($T) ]
#ifdef PFS #ifdef ForwardSecrecy
rule TA_CHALLENGE_C: rule TA_CHALLENGE_C:
let let
msg1 = <certT, '1', 't'> msg1 = <certT, '1', 't'>
...@@ -45,9 +45,9 @@ let ...@@ -45,9 +45,9 @@ let
cCA = senc(<certC, ~r2, pk(~skCe)>, kTENC) cCA = senc(<certC, ~r2, pk(~skCe)>, kTENC)
msg2 = <~id_c, ~r1, cTA, cCA, '2', 'c'> msg2 = <~id_c, ~r1, cTA, cCA, '2', 'c'>
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), !Cert($C, certC, 'chip') ]
--[ Eq(verify_cert(certT, 'terminal'), true), Started() ]-> --[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
[ Out(msg2), Out(senc(~iid, kTENC)), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, ~skCe, kTMAC, kTCNF) ] [ Out(msg2), TAChallengeC($C, certT, ~id_c, ~r1, ~r2, ~skCe, kTMAC, kTCNF) ]
#else #else
rule TA_CHALLENGE_C: rule TA_CHALLENGE_C:
let let
...@@ -59,12 +59,12 @@ let ...@@ -59,12 +59,12 @@ let
cCA = senc(<certC, ~r2>, kTENC) cCA = senc(<certC, ~r2>, kTENC)
msg2 = <~id_c, ~r1, cTA, cCA, '2', 'c'> msg2 = <~id_c, ~r1, cTA, cCA, '2', 'c'>
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), !Cert($C, certC, 'chip') ]
--[ Eq(verify_cert(certT, 'terminal'), true), Started() ]-> --[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
[ Out(msg2), Out(senc(~iid, kTENC)), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, ~r2, kTMAC, kTCNF) ] [ Out(msg2), TAChallengeC($C, certT, ~id_c, ~r1, ~r2, kTMAC, kTCNF) ]
#endif #endif
#ifdef PFS #ifdef ForwardSecrecy
rule TA_RESPONSE_T: rule TA_RESPONSE_T:
let let
msg2 = <id_c, r1, cTA, cCA, '2', 'c'> msg2 = <id_c, r1, cTA, cCA, '2', 'c'>
...@@ -83,9 +83,9 @@ let ...@@ -83,9 +83,9 @@ let
s = mac(<'CA', sid>, kTMAC) s = mac(<'CA', sid>, kTMAC)
msg3 = <kTCNF, cip, s, cipe, '3', 't'> msg3 = <kTCNF, cip, s, cipe, '3', 't'>
in in
[ In(msg2), Fr(~k), Fr(~ke), TAInitT(<$T, iid>), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ] [ In(msg2), Fr(~k), Fr(~ke), TAInitT($T), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ]
--[ Eq(verify_cert(certC, 'chip'), true) ]-> --[ Eq(verify_cert(certC, 'chip'), true) ]->
[ Out(msg3), TAResponseT(<$T, iid>, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ] [ Out(msg3), TAResponseT($T, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ]
#else #else
rule TA_RESPONSE_T: rule TA_RESPONSE_T:
let let
...@@ -103,12 +103,12 @@ let ...@@ -103,12 +103,12 @@ let
s = mac(<'CA', sid>, kTMAC) s = mac(<'CA', sid>, kTMAC)
msg3 = <kTCNF, cip, s, '3', 't'> msg3 = <kTCNF, cip, s, '3', 't'>
in in
[ In(msg2), Fr(~k), TAInitT(<$T, iid>), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ] [ In(msg2), Fr(~k), TAInitT($T), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ]
--[ Eq(verify_cert(certC, 'chip'), true) ]-> --[ Eq(verify_cert(certC, 'chip'), true) ]->
[ Out(msg3), TAResponseT(<$T, iid>, id_c, certC, r2, <~k, cip>) ] [ Out(msg3), TAResponseT($T, id_c, certC, r2, <~k, cip>) ]
#endif #endif
#ifdef PFS #ifdef ForwardSecrecy
rule TA_COMPLETE_C: rule TA_COMPLETE_C:
let let
msg3 = <kTCNF_T, cip, s, cipe, '3', 't'> msg3 = <kTCNF_T, cip, s, cipe, '3', 't'>
...@@ -119,9 +119,9 @@ let ...@@ -119,9 +119,9 @@ let
kKEY = kdf(<'KEY', sid>, <k, ke>) kKEY = kdf(<'KEY', sid>, <k, ke>)
msg4 = <kCNF, '4', 'c'> msg4 = <kCNF, '4', 'c'>
in in
[ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, r2, skCe, kTMAC, kTCNF), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] [ In(msg3), TAChallengeC($C, certT, id_c, r1, r2, skCe, kTMAC, kTCNF), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ]
--[ Eq(kTCNF_T, kTCNF), Eq(s, mac(<'CA', sid>, kTMAC)), CompletedTA($C, iid, cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> --[ Eq(kTCNF_T, kTCNF), Eq(s, mac(<'CA', sid>, kTMAC)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
[ Out(msg4), TACompleteC(<$C, iid>, kKEY) ] [ Out(msg4) ]
#else #else
rule TA_COMPLETE_C: rule TA_COMPLETE_C:
let let
...@@ -132,12 +132,12 @@ let ...@@ -132,12 +132,12 @@ let
kKEY = kdf(<'KEY', sid>, k) kKEY = kdf(<'KEY', sid>, k)
msg4 = <kCNF, '4', 'c'> msg4 = <kCNF, '4', 'c'>
in in
[ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, r2, kTMAC, kTCNF), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] [ In(msg3), TAChallengeC($C, certT, id_c, r1, r2, kTMAC, kTCNF), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ]
--[ Eq(kTCNF_T, kTCNF), Eq(s, mac(<'CA', sid>, kTMAC)), CompletedTA($C, iid, cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> --[ Eq(kTCNF_T, kTCNF), Eq(s, mac(<'CA', sid>, kTMAC)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
[ Out(msg4), TACompleteC(<$C, iid>, kKEY) ] [ Out(msg4) ]
#endif #endif
#ifdef PFS #ifdef ForwardSecrecy
rule CA_FINISH_T: rule CA_FINISH_T:
let let
msg4 = <kCNF_C, '4', 'c'> msg4 = <kCNF_C, '4', 'c'>
...@@ -145,9 +145,9 @@ let ...@@ -145,9 +145,9 @@ let
kCNF = kdf(<'CNF', sid>, <k, ke>) kCNF = kdf(<'CNF', sid>, <k, ke>)
kKEY = kdf(<'KEY', sid>, <k, ke>) kKEY = kdf(<'KEY', sid>, <k, ke>)
in in
[ In(msg4), TAResponseT(<$T, iid>, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT, 'terminal') ] [ In(msg4), TAResponseT($T, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !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) ] [ !SessionReveal(sid, kKEY) ]
#else #else
rule CA_FINISH_T: rule CA_FINISH_T:
let let
...@@ -156,9 +156,9 @@ let ...@@ -156,9 +156,9 @@ 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, 'terminal') ] [ In(msg4), TAResponseT($T, 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) ] [ !SessionReveal(sid, kKEY) ]
#endif #endif
......
FastSigPQEAC.spthy
+ 24
− 24
View file @ e7f75533
...@@ -29,31 +29,31 @@ rule TA_INIT_T: ...@@ -29,31 +29,31 @@ rule TA_INIT_T:
let let
msg1 = <certT, '1', 't'> msg1 = <certT, '1', 't'>
in in
[ !Cert($T, certT, 'terminal'), Fr(~iid) ] [ !Cert($T, certT, 'terminal') ]
--[ Started() ]-> --[ Started() ]->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ] [ Out(msg1), TAInitT($T) ]
#ifdef PFS #ifdef ForwardSecrecy
rule TA_CHALLENGE_C: rule TA_CHALLENGE_C:
let let
msg1 = <certT, '1', 't'> msg1 = <certT, '1', 't'>
msg2 = <~id_c, ~r1, certC, ~r2, pk(~skCe), '2', 'c'> msg2 = <~id_c, ~r1, certC, ~r2, pk(~skCe), '2', 'c'>
in in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid), Fr(~skCe), Fr(~r2), !Cert($C, certC, 'chip') ] [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~skCe), Fr(~r2), !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, ~skCe, ~r2) ] [ Out(msg2), TAChallengeC($C, certT, ~id_c, ~r1, ~skCe, ~r2) ]
#else #else
rule TA_CHALLENGE_C: rule TA_CHALLENGE_C:
let let
msg1 = <certT, '1', 't'> msg1 = <certT, '1', 't'>
msg2 = <~id_c, ~r1, certC, ~r2, '2', 'c'> msg2 = <~id_c, ~r1, certC, ~r2, '2', 'c'>
in in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid), Fr(~r2), !Cert($C, certC, 'chip') ] [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~r2), !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) ] [ Out(msg2), TAChallengeC($C, certT, ~id_c, ~r1, ~r2) ]
#endif #endif
#ifdef PFS #ifdef ForwardSecrecy
rule TA_RESPONSE_T: rule TA_RESPONSE_T:
let let
msg2 = <id_c, r1, certC, r2, pkCe, '2', 'c'> msg2 = <id_c, r1, certC, r2, pkCe, '2', 'c'>
...@@ -65,9 +65,9 @@ let ...@@ -65,9 +65,9 @@ let
s2 = sign(<'CA', sid>, ~skT) s2 = sign(<'CA', sid>, ~skT)
msg3 = <cip, cipe, s1, s2, '3', 't'> msg3 = <cip, cipe, s1, s2, '3', 't'>
in in
[ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal'), Fr(~k), Fr(~ke) ] [ In(msg2), TAInitT($T), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal'), Fr(~k), Fr(~ke) ]
--[ Eq(verify_cert(certC, 'chip'), true) ]-> --[ Eq(verify_cert(certC, 'chip'), true) ]->
[ Out(msg3), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ] [ Out(msg3), CAInitT($T, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ]
#else #else
rule TA_RESPONSE_T: rule TA_RESPONSE_T:
let let
...@@ -79,12 +79,12 @@ let ...@@ -79,12 +79,12 @@ let
s2 = sign(<'CA', sid>, ~skT) s2 = sign(<'CA', sid>, ~skT)
msg3 = <cip, s1, s2, '3', 't'> msg3 = <cip, s1, s2, '3', 't'>
in in
[ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal'), Fr(~k) ] [ In(msg2), TAInitT($T), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal'), Fr(~k) ]
--[ Eq(verify_cert(certC, 'chip'), true) ]-> --[ Eq(verify_cert(certC, 'chip'), true) ]->
[ Out(msg3), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>) ] [ Out(msg3), CAInitT($T, id_c, certC, r2, <~k, cip>) ]
#endif #endif
#ifdef PFS #ifdef ForwardSecrecy
rule TA_COMPLETE_C: rule TA_COMPLETE_C:
let let
msg3 = <cip, cipe, s1, s2, '3', 't'> msg3 = <cip, cipe, s1, s2, '3', 't'>
...@@ -95,9 +95,9 @@ let ...@@ -95,9 +95,9 @@ let
kKEY = kdf(<'KEY', sid>, <k, ke>) kKEY = kdf(<'KEY', sid>, <k, ke>)
msg4 = <kCNF, '4', 'c'> msg4 = <kCNF, '4', 'c'>
in in
[ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, skCe, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] [ In(msg3), TAChallengeC($C, certT, id_c, r1, skCe, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ]
--[ Eq(verify(s1, <'TA', id_c, r1>, cert_pk(certT)), true), Eq(verify(s2, <'CA', sid>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> --[ Eq(verify(s1, <'TA', id_c, r1>, cert_pk(certT)), true), Eq(verify(s2, <'CA', sid>, cert_pk(certT)), true), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
[ Out(msg4), TACompleteC(<$C, iid>, certT, id_c, r1, skCe, r2) ] [ Out(msg4) ]
#else #else
rule TA_COMPLETE_C: rule TA_COMPLETE_C:
let let
...@@ -108,12 +108,12 @@ let ...@@ -108,12 +108,12 @@ let
kKEY = kdf(<'KEY', sid>, k) kKEY = kdf(<'KEY', sid>, k)
msg4 = <kCNF, '4', 'c'> msg4 = <kCNF, '4', 'c'>
in in
[ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] [ In(msg3), TAChallengeC($C, certT, id_c, r1, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ]
--[ Eq(verify(s1, <'TA', id_c, r1>, cert_pk(certT)), true), Eq(verify(s2, <'CA', sid>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> --[ Eq(verify(s1, <'TA', id_c, r1>, cert_pk(certT)), true), Eq(verify(s2, <'CA', sid>, cert_pk(certT)), true), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
[ Out(msg4), TACompleteC(<$C, iid>, certT, id_c, r1, r2) ] [ Out(msg4) ]
#endif #endif
#ifdef PFS #ifdef ForwardSecrecy
rule CA_FINISH_T: rule CA_FINISH_T:
let let
msg4 = <kCNF_C, '4', 'c'> msg4 = <kCNF_C, '4', 'c'>
...@@ -121,9 +121,9 @@ let ...@@ -121,9 +121,9 @@ let
kCNF = kdf(<'CNF', sid>, <k, ke>) kCNF = kdf(<'CNF', sid>, <k, ke>)
kKEY = kdf(<'KEY', sid>, <k, ke>) kKEY = kdf(<'KEY', sid>, <k, ke>)
in in
[ In(msg4), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT, 'terminal') ] [ In(msg4), CAInitT($T, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !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) ] [ !SessionReveal(sid, kKEY) ]
#else #else
rule CA_FINISH_T: rule CA_FINISH_T:
let let
...@@ -132,9 +132,9 @@ let ...@@ -132,9 +132,9 @@ 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), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>), !Cert($T, certT, 'terminal') ] [ In(msg4), CAInitT($T, 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) ] [ !SessionReveal(sid, kKEY) ]
#endif #endif
......
KemPQEAC.spthy
+ 29
− 29
View file @ e7f75533
...@@ -30,9 +30,9 @@ rule TA_INIT_T: ...@@ -30,9 +30,9 @@ rule TA_INIT_T:
let let
msg1 = <certT, '1', 't'> msg1 = <certT, '1', 't'>
in in
[ !Cert($T, certT, 'terminal'), Fr(~iid) ] [ !Cert($T, certT, 'terminal') ]
--[ Started() ]-> --[ Started() ]->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ] [ Out(msg1), TAInitT($T) ]
// We generate a fresh IDc to simulate the previous execution of PACE or BAC // We generate a fresh IDc to simulate the previous execution of PACE or BAC
rule TA_CHALLENGE_C: rule TA_CHALLENGE_C:
...@@ -41,9 +41,9 @@ let ...@@ -41,9 +41,9 @@ let
cTA = encaps(~kTA, cert_pk(certT)) cTA = encaps(~kTA, cert_pk(certT))
msg2 = <~id_c, ~r1, cTA, '2', 'c'> msg2 = <~id_c, ~r1, cTA, '2', 'c'>
in in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA), Fr(~iid) ] [ In(msg1), Fr(~r1), Fr(~id_c), Fr(~kTA) ]
--[ Eq(verify_cert(certT, 'terminal'), true), Started() ]-> --[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
[ Out(msg2), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1, <~kTA, cTA>) ] [ Out(msg2), TAChallengeC($C, certT, ~id_c, ~r1, <~kTA, cTA>) ]
rule TA_RESPONSE_T: rule TA_RESPONSE_T:
let let
...@@ -54,9 +54,9 @@ let ...@@ -54,9 +54,9 @@ let
kTCNF = kdf(<'TCNF', r1>, kTA) kTCNF = kdf(<'TCNF', r1>, kTA)
msg3 = <kTCNF, '3', 't'> msg3 = <kTCNF, '3', 't'>
in in
[ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT, 'terminal') ] [ In(msg2), TAInitT($T), !Ltk($T, ~skT, 'terminal') ]
--> -->
[ Out(msg3), TAResponseT(<$T, iid>, id_c, kTMAC, kTENC) ] [ Out(msg3), TAResponseT($T, id_c, kTMAC, kTENC) ]
rule TA_COMPLETE_C: rule TA_COMPLETE_C:
let let
...@@ -65,37 +65,37 @@ let ...@@ -65,37 +65,37 @@ let
kTENC = kdf(<'TENC', r1>, kTA) kTENC = kdf(<'TENC', r1>, kTA)
kTCNF = kdf(<'TCNF', r1>, kTA) kTCNF = kdf(<'TCNF', r1>, kTA)
in in
[ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1, <kTA, cTA>) ] [ In(msg3), TAChallengeC($C, certT, id_c, r1, <kTA, cTA>) ]
--[ Eq(kTCNF_T, kTCNF), CompletedTA($C, iid, cert_id(certT)) ]-> --[ Eq(kTCNF_T, kTCNF) ]->
[ TACompleteC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC) ] [ TACompleteC($C, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC) ]
/* Chip Authentication */ /* Chip Authentication */
// State machine: CA_INIT_C -> CA_INIT_T -> CA_FINISH_C -> CA_FINISH_T // State machine: CA_INIT_C -> CA_INIT_T -> CA_FINISH_C -> CA_FINISH_T
#ifdef PFS #ifdef ForwardSecrecy
rule CA_INIT_C: rule CA_INIT_C:
let let
cCA = senc(<certC, ~r2, pk(~skCe)>, kTENC) cCA = senc(<certC, ~r2, pk(~skCe)>, kTENC)
msg4 = <cCA, '4', 'c'> msg4 = <cCA, '4', 'c'>
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) ]
--> -->
[ Out(msg4), Out(senc(iid, kTENC)), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, ~r2, ~skCe) ] [ Out(msg4), CAInitC($C, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, ~r2, ~skCe) ]
#else #else
rule CA_INIT_C: rule CA_INIT_C:
let let
cCA = senc(<certC, ~r2>, kTENC) cCA = senc(<certC, ~r2>, kTENC)
msg4 = <cCA, '4', 'c'> msg4 = <cCA, '4', 'c'>
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, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC) ]
--> -->
[ Out(msg4), Out(senc(iid, kTENC)), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, ~r2) ] [ Out(msg4), CAInitC($C, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, ~r2) ]
#endif #endif
#ifdef PFS #ifdef ForwardSecrecy
rule CA_INIT_T: rule CA_INIT_T:
let let
msg4 = <cCA, '4', 'c'> msg4 = <cCA, '4', 'c'>
...@@ -110,9 +110,9 @@ let ...@@ -110,9 +110,9 @@ let
s = mac(<'CA', sid>, kTMAC) s = mac(<'CA', sid>, kTMAC)
msg5 = <cip, s, cipe, '5', 't'> msg5 = <cip, s, cipe, '5', 't'>
in in
[ In(msg4), TAResponseT(<$T, iid>, id_c, kTMAC, kTENC), !Cert($T, certT, 'terminal'), Fr(~k), Fr(~ke) ] [ In(msg4), TAResponseT($T, id_c, kTMAC, kTENC), !Cert($T, certT, 'terminal'), Fr(~k), Fr(~ke) ]
--[ Eq(verify_cert(certC, 'chip'), true) ]-> --[ Eq(verify_cert(certC, 'chip'), true) ]->
[ Out(msg5), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ] [ Out(msg5), CAInitT($T, id_c, kTMAC, kTENC, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ]
#else #else
rule CA_INIT_T: rule CA_INIT_T:
let let
...@@ -126,13 +126,13 @@ let ...@@ -126,13 +126,13 @@ let
s = mac(<'CA', sid>, kTMAC) s = mac(<'CA', sid>, kTMAC)
msg5 = <cip, s, '5', 't'> msg5 = <cip, s, '5', 't'>
in in
[ In(msg4), TAResponseT(<$T, iid>, id_c, kTMAC, kTENC), !Cert($T, certT, 'terminal'), Fr(~k) ] [ In(msg4), TAResponseT($T, id_c, kTMAC, kTENC), !Cert($T, certT, 'terminal'), Fr(~k) ]
--[ Eq(verify_cert(certC, 'chip'), true) ]-> --[ Eq(verify_cert(certC, 'chip'), true) ]->
[ Out(msg5), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, certC, r2, <~k, cip>) ] [ Out(msg5), CAInitT($T, id_c, kTMAC, kTENC, certC, r2, <~k, cip>) ]
#endif #endif
#ifdef PFS #ifdef ForwardSecrecy
rule CA_FINISH_C: rule CA_FINISH_C:
let let
msg5 = <cip, s, cipe, '5', 't'> msg5 = <cip, s, cipe, '5', 't'>
...@@ -143,9 +143,9 @@ let ...@@ -143,9 +143,9 @@ let
kKEY = kdf(<'KEY', sid>, <k, ke>) kKEY = kdf(<'KEY', sid>, <k, ke>)
msg6 = <kCNF, '6', 'c'> msg6 = <kCNF, '6', 'c'>
in in
[ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, r2, skCe), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] [ In(msg5), CAInitC($C, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, r2, skCe), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ]
--[ Eq(s, mac(<'CA', sid>, kTMAC)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> --[ Eq(s, mac(<'CA', sid>, kTMAC)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
[ Out(msg6), CAFinishC($C, cert_id(certT), kKEY) ] [ Out(msg6) ]
#else #else
rule CA_FINISH_C: rule CA_FINISH_C:
let let
...@@ -156,13 +156,13 @@ let ...@@ -156,13 +156,13 @@ let
kKEY = kdf(<'KEY', sid>, k) kKEY = kdf(<'KEY', sid>, k)
msg6 = <kCNF, '6', 'c'> msg6 = <kCNF, '6', 'c'>
in in
[ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] [ In(msg5), CAInitC($C, certT, id_c, r1, <kTA, cTA>, kTMAC, kTENC, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ]
--[ Eq(s, mac(<'CA', sid>, kTMAC)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> --[ Eq(s, mac(<'CA', sid>, kTMAC)), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
[ Out(msg6), CAFinishC($C, cert_id(certT), kKEY) ] [ Out(msg6) ]
#endif #endif
#ifdef PFS #ifdef ForwardSecrecy
rule CA_FINISH_T: rule CA_FINISH_T:
let let
msg6 = <kCNF_c, '6', 'c'> msg6 = <kCNF_c, '6', 'c'>
...@@ -170,9 +170,9 @@ let ...@@ -170,9 +170,9 @@ let
kCNF = kdf(<'CNF', sid>, <k, ke>) kCNF = kdf(<'CNF', sid>, <k, ke>)
kKEY = kdf(<'KEY', sid>, <k, ke>) kKEY = kdf(<'KEY', sid>, <k, ke>)
in in
[ In(msg6), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT, 'terminal') ] [ In(msg6), CAInitT($T, id_c, kTMAC, kTENC, certC, r2, <k, cip>, <ke, cipe>, pkCe), !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) ] [ !SessionReveal(sid, kKEY) ]
#else #else
rule CA_FINISH_T: rule CA_FINISH_T:
let let
...@@ -181,9 +181,9 @@ let ...@@ -181,9 +181,9 @@ let
kCNF = kdf(<'CNF', sid>, k) kCNF = kdf(<'CNF', sid>, k)
kKEY = kdf(<'KEY', sid>, k) kKEY = kdf(<'KEY', sid>, k)
in in
[ In(msg6), CAInitT(<$T, iid>, id_c, kTMAC, kTENC, certC, r2, <k, cip>), !Cert($T, certT, 'terminal') ] [ In(msg6), CAInitT($T, id_c, kTMAC, kTENC, 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) ] [ !SessionReveal(sid, kKEY) ]
#endif #endif
......
README.md
+ 4
− 1
View file @ e7f75533
# EAC_Tamarin_Analysis # EAC_Tamarin_Analysis
This project contains the different versions of EAC from https://ia.cr/2023/352. This project contains the different versions of EAC from https://ia.cr/2023/352.
The models are the classic EAC, SigPQEAC and KemPQEAC as well as the forward security and full round trip save modifications. The models are the classic EAC, SigPQEAC and KemPQEAC as well as the forward seccrecy and saved round-trip modifications.
The [python script](InsertLemmas.py) inserts the different sections into the .spthy files and creates the tmp.spthy file. Usage: python InsertLemmas.py file.spthy The [python script](InsertLemmas.py) inserts the different sections into the .spthy files and creates the tmp.spthy file. Usage: python InsertLemmas.py file.spthy
The [include](include/) directory contains the code that will be included to the different models. The [include](include/) directory contains the code that will be included to the different models.
## Forward Secrecy modification
For each post-quantum model (SigPQEAC, FastSigPQEAC, KemPQEAC and FastKemPQEAC) exists a modification which is forward secrecy secure. To analyze the modified model, we need to add the '--defines=ForwardSecrecy' flag to the tamarin-prover execution command.
## Results ## Results
The directory [results](results/) contains the results of all variations executed on the Lichtenberg high performance computer of the TU Darmstadt. The directory [results](results/) contains the results of all variations executed on the Lichtenberg high performance computer of the TU Darmstadt.
......
SigPQEAC.spthy
+ 29
− 29
View file @ e7f75533
...@@ -30,9 +30,9 @@ rule TA_INIT_T: ...@@ -30,9 +30,9 @@ rule TA_INIT_T:
let let
msg1 = <certT, '1', 't'> msg1 = <certT, '1', 't'>
in in
[ !Cert($T, certT, 'terminal'), Fr(~iid) ] [ !Cert($T, certT, 'terminal') ]
--[ Started() ]-> --[ Started() ]->
[ Out(msg1), Out(~iid), TAInitT(<$T, ~iid>) ] [ Out(msg1), TAInitT($T) ]
// We generate a fresh IDc to simulate the previous execution of PACE or BAC // We generate a fresh IDc to simulate the previous execution of PACE or BAC
rule TA_CHALLENGE_C: rule TA_CHALLENGE_C:
...@@ -40,9 +40,9 @@ let ...@@ -40,9 +40,9 @@ let
msg1 = <certT, '1', 't'> msg1 = <certT, '1', 't'>
msg2 = <~id_c, ~r1, '2', 'c'> msg2 = <~id_c, ~r1, '2', 'c'>
in in
[ In(msg1), Fr(~r1), Fr(~id_c), Fr(~iid) ] [ In(msg1), Fr(~r1), Fr(~id_c) ]
--[ Eq(verify_cert(certT, 'terminal'), true), Started() ]-> --[ Eq(verify_cert(certT, 'terminal'), true), Started() ]->
[ Out(msg2), TAChallengeC(<$C, ~iid>, certT, ~id_c, ~r1) ] [ Out(msg2), TAChallengeC($C, certT, ~id_c, ~r1) ]
rule TA_RESPONSE_T: rule TA_RESPONSE_T:
let let
...@@ -50,43 +50,43 @@ let ...@@ -50,43 +50,43 @@ let
s = sign(<'TA', id_c, r1>, ~skT) s = sign(<'TA', id_c, r1>, ~skT)
msg3 = <s, '3', 't'> msg3 = <s, '3', 't'>
in in
[ In(msg2), TAInitT(<$T, iid>), !Ltk($T, ~skT, 'terminal') ] [ In(msg2), TAInitT($T), !Ltk($T, ~skT, 'terminal') ]
--> -->
[ Out(msg3), TAResponseT(<$T, iid>, id_c) ] [ Out(msg3), TAResponseT($T, id_c) ]
rule TA_COMPLETE_C: rule TA_COMPLETE_C:
let let
msg3 = <s, '3', 't'> msg3 = <s, '3', 't'>
in in
[ In(msg3), TAChallengeC(<$C, iid>, certT, id_c, r1) ] [ In(msg3), TAChallengeC($C, certT, id_c, r1) ]
--[ Eq(verify(s, <'TA', id_c, r1>, cert_pk(certT)), true), CompletedTA($C, iid, cert_id(certT)) ]-> --[ Eq(verify(s, <'TA', id_c, r1>, cert_pk(certT)), true) ]->
[ TACompleteC(<$C, iid>, certT, id_c, r1) ] [ TACompleteC($C, certT, id_c, r1) ]
/* Chip Authentication */ /* Chip Authentication */
// State machine: CA_INIT_C -> CA_INIT_T -> CA_FINISH_C -> CA_FINISH_T // State machine: CA_INIT_C -> CA_INIT_T -> CA_FINISH_C -> CA_FINISH_T
#ifdef PFS #ifdef ForwardSecrecy
rule CA_INIT_C: rule CA_INIT_C:
let let
msg4 = <certC, ~r2, pk(~skCe), '4', 'c'> msg4 = <certC, ~r2, pk(~skCe), '4', 'c'>
in in
[ Fr(~r2), Fr(~skCe), TACompleteC(<$C, iid>, certT, id_c, r1), !Cert($C, certC, 'chip') ] [ Fr(~r2), Fr(~skCe), TACompleteC($C, certT, id_c, r1), !Cert($C, certC, 'chip') ]
--> -->
[ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, ~r2, ~skCe) ] [ Out(msg4), CAInitC($C, certT, id_c, r1, ~r2, ~skCe) ]
#else #else
rule CA_INIT_C: rule CA_INIT_C:
let let
msg4 = <certC, ~r2, '4', 'c'> msg4 = <certC, ~r2, '4', 'c'>
in in
[ Fr(~r2), TACompleteC(<$C, iid>, certT, id_c, r1), !Cert($C, certC, 'chip') ] [ Fr(~r2), TACompleteC($C, certT, id_c, r1), !Cert($C, certC, 'chip') ]
--> -->
[ Out(msg4), Out(iid), CAInitC(<$C, iid>, certT, id_c, r1, ~r2) ] [ Out(msg4), CAInitC($C, certT, id_c, r1, ~r2) ]
#endif #endif
#ifdef PFS #ifdef ForwardSecrecy
rule CA_INIT_T: rule CA_INIT_T:
let let
msg4 = <certC, r2, pkCe, '4', 'c'> msg4 = <certC, r2, pkCe, '4', 'c'>
...@@ -97,9 +97,9 @@ let ...@@ -97,9 +97,9 @@ let
s = sign(<'CA', sid>, ~skT) s = sign(<'CA', sid>, ~skT)
msg5 = <cip, s, cipe, '5', 't'> msg5 = <cip, s, cipe, '5', 't'>
in in
[ In(msg4), Fr(~k), Fr(~ke), TAResponseT(<$T, iid>, id_c), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ] [ In(msg4), Fr(~k), Fr(~ke), TAResponseT($T, id_c), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ]
--[ Eq(verify_cert(certC, 'chip'), true) ]-> --[ Eq(verify_cert(certC, 'chip'), true) ]->
[ Out(msg5), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ] [ Out(msg5), CAInitT($T, id_c, certC, r2, <~k, cip>, <~ke, cipe>, pkCe) ]
#else #else
rule CA_INIT_T: rule CA_INIT_T:
let let
...@@ -110,13 +110,13 @@ let ...@@ -110,13 +110,13 @@ let
s = sign(<'CA', sid>, ~skT) s = sign(<'CA', sid>, ~skT)
msg5 = <cip, s, '5', 't'> msg5 = <cip, s, '5', 't'>
in in
[ In(msg4), Fr(~k), TAResponseT(<$T, iid>, id_c), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ] [ In(msg4), Fr(~k), TAResponseT($T, id_c), !Ltk($T, ~skT, 'terminal'), !Cert($T, certT, 'terminal') ]
--[ Eq(verify_cert(certC, 'chip'), true) ]-> --[ Eq(verify_cert(certC, 'chip'), true) ]->
[ Out(msg5), CAInitT(<$T, iid>, id_c, certC, r2, <~k, cip>) ] [ Out(msg5), CAInitT($T, id_c, certC, r2, <~k, cip>) ]
#endif #endif
#ifdef PFS #ifdef ForwardSecrecy
rule CA_FINISH_C: rule CA_FINISH_C:
let let
msg5 = <cip, s, cipe, '5', 't'> msg5 = <cip, s, cipe, '5', 't'>
...@@ -127,9 +127,9 @@ let ...@@ -127,9 +127,9 @@ let
kKEY = kdf(<'KEY', sid>, <k, ke>) kKEY = kdf(<'KEY', sid>, <k, ke>)
msg6 = <kCNF, '6', 'c'> msg6 = <kCNF, '6', 'c'>
in in
[ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, r2, skCe), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] [ In(msg5), CAInitC($C, certT, id_c, r1, r2, skCe), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ]
--[ Eq(verify(s, <'CA', sid>, cert_pk(certT)), true), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> --[ Eq(verify(s, <'CA', sid>, cert_pk(certT)), true), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
[ Out(msg6), CAFinishC($C, cert_id(certT), kKEY) ] [ Out(msg6) ]
#else #else
rule CA_FINISH_C: rule CA_FINISH_C:
let let
...@@ -140,12 +140,12 @@ let ...@@ -140,12 +140,12 @@ let
kKEY = kdf(<'KEY', sid>, k) kKEY = kdf(<'KEY', sid>, k)
msg6 = <kCNF, '6', 'c'> msg6 = <kCNF, '6', 'c'>
in in
[ In(msg5), CAInitC(<$C, iid>, certT, id_c, r1, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ] [ In(msg5), CAInitC($C, certT, id_c, r1, r2), !Ltk($C, ~skC, 'chip'), !Cert($C, certC, 'chip') ]
--[ Eq(verify(s, <'CA', sid>, cert_pk(certT)), true), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]-> --[ Eq(verify(s, <'CA', sid>, cert_pk(certT)), true), Completed(kKEY, sid, $C, 'chip', cert_id(certT)) ]->
[ Out(msg6), CAFinishC($C, cert_id(certT), kKEY) ] [ Out(msg6) ]
#endif #endif
#ifdef PFS #ifdef ForwardSecrecy
rule CA_FINISH_T: rule CA_FINISH_T:
let let
msg6 = <kCNF_C, '6', 'c'> msg6 = <kCNF_C, '6', 'c'>
...@@ -153,9 +153,9 @@ let ...@@ -153,9 +153,9 @@ let
kCNF = kdf(<'CNF', sid>, <k, ke>) kCNF = kdf(<'CNF', sid>, <k, ke>)
kKEY = kdf(<'KEY', sid>, <k, ke>) kKEY = kdf(<'KEY', sid>, <k, ke>)
in in
[ In(msg6), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !Cert($T, certT, 'terminal') ] [ In(msg6), CAInitT($T, id_c, certC, r2, <k, cip>, <ke, cipe>, pkCe), !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) ] [ !SessionReveal(sid, kKEY) ]
#else #else
rule CA_FINISH_T: rule CA_FINISH_T:
let let
...@@ -164,9 +164,9 @@ let ...@@ -164,9 +164,9 @@ let
kCNF = kdf(<'CNF', sid>, k) kCNF = kdf(<'CNF', sid>, k)
kKEY = kdf(<'KEY', sid>, k) kKEY = kdf(<'KEY', sid>, k)
in in
[ In(msg6), CAInitT(<$T, iid>, id_c, certC, r2, <k, cip>), !Cert($T, certT, 'terminal') ] [ In(msg6), CAInitT($T, 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) ] [ !SessionReveal(sid, kKEY) ]
#endif #endif
......
include/include/attacker.spthy 0 → 100644
+ 12
− 0
View file @ e7f75533
/* Attacker model */
// We extend the Dolev-Yao attack model in tamarin with Reveal and Corrupt capabilities
rule Corrupt_ltk:
[ !Ltk($A, ltk, role) ]
--[ Corrupted($A) ]->
[ Out(<ltk, role>) ]
rule Reveal_session:
[ !SessionReveal(sid, k) ]
--[ Revealed(sid) ]->
[ Out(k) ]
include/include/classic_verify_transcript.spthy 0 → 100644
+ 24
− 0
View file @ e7f75533
rule Verify_Transcript_C:
let
pkT = cert_pk(certT)
k = pkTe^skC
kMac = kdf_mac(k, r2)
tag_c = mac(pkTe, kMac)
in
[ In(<certT, pkTe, IDc, r1, s1, certC, pkTe2, r2, tag>), !Ltk(C, skC, 'chip') ]
--[ Eq(C, cert_id(certC)), Eq(tag, tag_c), Eq(pkTe, pkTe2), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(s1, <IDc, r1, pkTe>, pkT), true), ValidTrans(C, 'chip', cert_id(certT)) ]->
[ ]
rule Verify_Transcript_T:
let
pkT = cert_pk(certT)
pkC = cert_pk(certC)
tag_t = mac(pkTe, kdf_mac(r2, skTe^pkC))
k = pkC^skTe
kMac = kdf_mac(k, r2)
tag_t = mac(pkTe, kMac)
in
[ In(<certT, pkTe, IDc, r1, s1, certC, pkTe2, r2, tag>), In(<skTe, T>) ]
--[ Eq(T, cert_id(certT)), Eq(tag, tag_t), Eq(pkTe, pkTe2), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(s1, <IDc, r1, pkTe>, pkT), true), ValidTrans(T, 'terminal', cert_id(certC)) ]->
[ ]
include/include/kem_verify_transcript.spthy 0 → 100644
+ 75
− 0
View file @ e7f75533
#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)
dmesg = sdec(cCA, kTENC)
certC = fst(dmesg)
r2 = snd(dmesg)
sid = <certT, certC, r2, cip, pkCe, cipe>
s_c = mac(<'CA', sid>, kTMAC)
k = decaps(cip, skC)
ke = decaps(cipe, skCe)
kCNF_c = kdf(<'CNF', sid>, <k, ke>)
in
[ In(<certT, IDc, r1, cTA, kTCNF, cCA, cip, s, cipe, kCNF>), In(<kTA, skCe>), !Ltk(C, skC, 'chip') ]
--[ Eq(C, cert_id(certC)), Eq(verify_cert(certC, 'chip'), true), Eq(verify_cert(certT, 'terminal'), true), Eq(kTCNF, kTCNF_c), Eq(s, s_c), Eq(kCNF, kCNF_c), ValidTrans(C, 'chip', cert_id(certT)) ]->
[ ]
#else
rule Verify_Transcript_C:
let
kTMAC = kdf(<'TMAC', r1>, kTA)
kTENC = kdf(<'TENC', r1>, kTA)
kTCNF_c = kdf(<'TCNF', r1>, kTA)
dmesg = sdec(cCA, kTENC)
certC = fst(dmesg)
r2 = snd(dmesg)
sid = <certT, certC, r2, cip>
s_c = mac(<'CA', sid>, kTMAC)
kKDF = decaps(cip, skC)
kCNF_c = kdf(<'CNF', sid>, kKDF)
in
[ In(<certT, IDc, r1, cTA, kTCNF, cCA, cip, s, kCNF>), In(kTA), !Ltk(C, skC, 'chip') ]
--[ Eq(C, cert_id(certC)), Eq(verify_cert(certC, 'chip'), true), Eq(verify_cert(certT, 'terminal'), true), Eq(kTCNF, kTCNF_c), Eq(s, s_c), Eq(kCNF, kCNF_c), ValidTrans(C, 'chip', cert_id(certT)) ]->
[ ]
#endif
#ifdef PFS
rule Verify_Transcript_T:
let
kTA = decaps(cTA, skT)
kTMAC = kdf(<'TMAC', r1>, kTA)
kTENC = kdf(<'TENC', r1>, kTA)
kTCNF_t = kdf(<'TCNF', r1>, kTA)
dmesg = sdec(cCA, kTENC)
certC = fst(dmesg)
r2 = fst(snd(dmesg))
pkCe = snd(snd(dmesg))
sid = <certT, certC, r2, cip, pkCe, cipe>
s_t = mac(<'CA', sid>, kTMAC)
kCNF_t = kdf(<'CNF', sid>, <k, ke>)
in
[ In(<certT, IDc, r1, cTA, kTCNF, cCA, cip, s, cipe, kCNF>), In(<k, ke>), !Ltk(T, skT, 'terminal') ]
--[ Eq(T, cert_id(certT)), Eq(verify_cert(certC, 'chip'), true), Eq(verify_cert(certT, 'terminal'), true), Eq(kTCNF, kTCNF_t), Eq(s, s_t), Eq(kCNF, kCNF_t), ValidTrans(T, 'terminal', cert_id(certC)) ]->
[ ]
#else
rule Verify_Transcript_T:
let
kTA = decaps(cTA, skT)
kTMAC = kdf(<'TMAC', r1>, kTA)
kTENC = kdf(<'TENC', r1>, kTA)
kTCNF_t = kdf(<'TCNF', r1>, kTA)
dmesg = sdec(cCA, kTENC)
certC = fst(dmesg)
r2 = snd(dmesg)
sid = <certT, certC, r2, cip>
s_t = mac(<'CA', sid>, kTMAC)
kCNF_t = kdf(<'CNF', sid>, kKDF)
in
[ In(<certT, IDc, r1, cTA, kTCNF, cCA, cip, s, kCNF>), In(kKDF), !Ltk(T, skT, 'terminal') ]
--[ Eq(T, cert_id(certT)), Eq(verify_cert(certC, 'chip'), true), Eq(verify_cert(certT, 'terminal'), true), Eq(kTCNF, kTCNF_t), Eq(s, s_t), Eq(kCNF, kCNF_t), ValidTrans(T, 'terminal', cert_id(certC)) ]->
[ ]
#endif
include/include/lemmas.spthy 0 → 100644
+ 151
− 0
View file @ e7f75533
/* Contains the restrictions and lemmas for all EAC models */
restriction Equality:
"All x y #i. Eq(x, y) @ i ==> x = y"
// Correctness
lemma session_exist: exists-trace
" Ex C T k sid #i #j.
Completed(k, sid, C, 'chip', T) @ #i
& Completed(k, sid, T, 'terminal', C) @ #j
& #i < #j
"
lemma two_session_exist: exists-trace
" Ex C T k k2 sid sid2 #i #j #i2 #j2.
Completed(k, sid, C, 'chip', T) @ #i
& Completed(k, sid, T, 'terminal', C) @ #j
& #i < #j
& Completed(k2, sid2, C, 'chip', T) @ #i2
& Completed(k2, sid2, T, 'terminal', C) @ #j2
& #i2 < #j2
& not(k=k2)
"
// Agreement
lemma aliveness:
"All k sid A role B #i #t .
Completed(k, sid, A, role, B) @ #i
& Finished(sid) @ #t
==> (Ex k2 sid2 role2 C #j .
Completed(k2, sid2, B, role2, C) @ #j)
| (Ex #k . Corrupted(B) @ #k)
"
lemma weak_agreement_C:
"All k sid C T #i #t .
Completed(k, sid, C, 'chip', T) @ #i
& Finished(sid) @ #t
==> (Ex k2 sid2 #j .
Completed(k2, sid2, T, 'terminal', C) @ #j)
| (Ex #k . Corrupted(C) @ #k)
| (Ex #k . Corrupted(T) @ #k)
"
lemma weak_agreement_T:
"All k sid C T #i #t .
Completed(k, sid, T, 'terminal', C) @ #i
& Finished(sid) @ #t
==> (Ex k2 sid2 #j .
Completed(k2, sid2, C, 'chip', T) @ #j)
| (Ex #k . Corrupted(C) @ #k)
| (Ex #k . Corrupted(T) @ #k)
"
lemma agreement_C:
"All k sid C T #i #t .
Completed(k, sid, C, 'chip', T) @ #i
& Finished(sid) @ #t
==> (Ex #j .
Completed(k, sid, T, 'terminal', C) @ #j)
| (Ex #k . Corrupted(C) @ #k)
| (Ex #k . Corrupted(T) @ #k)
"
lemma agreement_T:
"All k sid C T #i #t .
Completed(k, sid, T, 'terminal', C) @ #i
& Finished(sid) @ #t
==> (Ex #j .
Completed(k, sid, C, 'chip', T) @ #j)
| (Ex #k . Corrupted(C) @ #k)
| (Ex #k . Corrupted(T) @ #k)
"
lemma session_uniqueness:
"All A B k sid sid2 role #i #j .
Completed(k, sid, A, role, B) @ #i
& Completed(k, sid2, A, role, B) @ #j
==> (#i = #j) & (sid = sid2)
"
// Sole purpose of static key of T is authentication
// The final keys k/k2 are only derived from pkC/skC, pkTe/skTe and r2
lemma consistency:
"All C T k k2 sid #i #j .
Completed(k, sid, C, 'chip', T) @ #i
& Completed(k2, sid, T, 'terminal', C) @ #j
==> (k=k2)
| (Ex #m . Corrupted(C) @ #m)
| (Ex #m . Corrupted(T) @ #m)
"
// Key secrecy
lemma key_secrecy:
"All C T k sid #i #j .
Completed(k, sid, C, 'chip', T) @ #i
& Completed(k, sid, T, 'terminal', C) @ #j
==> not(Ex #m . K(k) @ #m)
| (Ex #m . Revealed(sid) @ #m)
| (Ex #m . Corrupted(C) @ #m)
| (Ex #m . Corrupted(T) @ #m)
"
/* We simulate a one sided protocol execution */
// The terminal submits a transcript for a valid protocol execution and the chip verifies it
// If the terminal succeeds it has disproven non-repudiation for the chip
// 1.: We prohibit any previous protocol executions
// 2.: The chip should not be corrupted, so that the terminal needs to forge the values
// 3.: The terminal is not allowed to register a chip certificate
lemma notNonRepudiation_C: exists-trace
"Ex C T #i .
ValidTrans(C, 'chip', T) @ #i
& not(Ex #k . Started() @ #k) // 1.
& not(Ex #k . Corrupted(C) @ #k) // 2.
& not(Ex #k . RegisteredRole(T, 'chip') @ #k) // 3.
"
// The chip submits a transcript for a valid protocol execution and the terminal verifies it
// If the chip succeeds it has disproven non-repudiation for the terminal
lemma notNonRepudiation_T: exists-trace
"Ex C T #i .
ValidTrans(T, 'terminal', C) @ #i
& not(Ex #k . Started() @ #k)
& not(Ex #k . Corrupted(T) @ #k)
& not(Ex #k . RegisteredRole(C, 'terminal') @ #k)
"
lemma forward_secrecy:
"All C T k sid #i #j .
Completed(k, sid, C, 'chip', T) @ #i
& Completed(k, sid, T, 'terminal', C) @ #j
& not(Ex #m . Corrupted(C) @ #m & #m < #j)
& not(Ex #m . Corrupted(T) @ #m & #m < #j)
==> (not(Ex #m . K(k) @ #m)
| (Ex #m . Revealed(sid) @ #m))
"
lemma forward_secrecy_T:
"All C T k sid #i #j .
Completed(k, sid, C, 'chip', T) @ #i
& Completed(k, sid, T, 'terminal', C) @ #j
& not(Ex #m . Corrupted(C) @ #m)
& not(Ex #m . Corrupted(T) @ #m & #m < #j)
==> (not(Ex #m . K(k) @ #m)
| (Ex #m . Revealed(sid) @ #m))
"
include/include/setup.spthy 0 → 100644
+ 49
− 0
View file @ e7f75533
/* Key setup and Certificate model for all EAC models */
functions: cert/3, cert_pk/1, cert_sig/1, cert_id/1, ca_sk/0 [private]
equations: cert_pk(cert(pk, s, id)) = pk, cert_sig(cert(pk, s, id)) = s, cert_id(cert(pk, s, id)) = id
macros: verify_cert(cert, role) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert), role>, pk(ca_sk))
rule Publish_ca_pk:
[ ]
-->
[ Out(pk(ca_sk)) ]
// Generate long-term key pair for the chip. Classic version needs dh key pair
#ifdef CLASSIC
rule Generate_chip_key_pair:
let
pk = 'g'^~ltk
in
[ Fr(~ltk) ]
-->
[ !Pk($A, pk, 'chip'), !Ltk($A, ~ltk, 'chip'), Out(pk) ]
#else
rule Generate_chip_key_pair:
let
pk = pk(~ltk)
in
[ Fr(~ltk) ]
-->
[ !Pk($A, pk, 'chip'), !Ltk($A, ~ltk, 'chip'), Out(pk) ]
#endif
// Generate static long-term key pair for the terminal.
rule Generate_terminal_key_pair:
let
pk = pk(~ltk)
in
[ Fr(~ltk) ]
-->
[ !Pk($A, pk, 'terminal'), !Ltk($A, ~ltk, 'terminal'), Out(pk) ]
rule CA_Sign_ltk:
let
certA = cert(pk, sign(<pk, A, role>, ca_sk), A)
in
[ !Pk(A, pk, role) ]
--[ RegisteredRole(A, role) ]->
[ !Cert(A, certA, role), Out(certA) ]
include/include/sig_verify_transcript.spthy 0 → 100644
+ 44
− 0
View file @ e7f75533
#ifdef PFS
rule Verify_Transcript_C:
let
pkT = cert_pk(certT)
sid = <certT, certC, r2, cip, pkCe, cipe>
k = decaps(cip, skC)
ke = decaps(cipe, skCe)
kCNF_c = kdf(<'CNF', sid>, <k, ke>)
in
[ In(<certT, IDc, r1, sT, certC, r2, pkCe, cip, sC, cipe, kCNF>), In(skCe), !Ltk(C, skC, 'chip') ]
--[ Eq(C, cert_id(certC)), 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_c), ValidTrans(C, 'chip', cert_id(certT)) ]->
[ ]
#else
rule Verify_Transcript_C:
let
pkT = cert_pk(certT)
sid = <certT, certC, r2, cip>
kKDF = decaps(cip, skC)
kCNF_c = kdf(<'CNF', sid>, kKDF)
in
[ In(<certT, IDc, r1, sT, certC, r2, cip, sC, kCNF>), !Ltk(C, skC, 'chip') ]
--[ Eq(C, cert_id(certC)), 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_c), ValidTrans(C, 'chip', cert_id(certT)) ]->
[ ]
#endif
#ifdef PFS
rule Verify_Transcript_T:
let
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>), !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
sid = <certT, certC, r2, cip>
kCNF_t = kdf(<'CNF', sid>, kKDF)
in
[ 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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment