From 8c469af6b14c6503a418dde236f856ff59492411 Mon Sep 17 00:00:00 2001 From: James Brownlee Date: Wed, 7 Feb 2024 16:40:57 -0500 Subject: [PATCH] adding identity hiding improvements: seperate files for responder and initiator tests test file that shows other participants leaking info has an effect general code clean up performance improvement: initiator and responder tests now run in ~10s --- .../03_identity_hiding_initiator.entry.mpv | 25 +++++ .../03_identity_hiding_responder.entry.mpv | 96 +++++++++++++++++++ analysis/03_identity_hiding_test.entry.mpv | 29 ++++++ .../03_identity_hiding.mpv} | 84 +++++++++++----- 4 files changed, 209 insertions(+), 25 deletions(-) create mode 100644 analysis/03_identity_hiding_initiator.entry.mpv create mode 100644 analysis/03_identity_hiding_responder.entry.mpv create mode 100644 analysis/03_identity_hiding_test.entry.mpv rename analysis/{03_identity_hiding.entry.mpv => rosenpass/03_identity_hiding.mpv} (65%) diff --git a/analysis/03_identity_hiding_initiator.entry.mpv b/analysis/03_identity_hiding_initiator.entry.mpv new file mode 100644 index 0000000..2d63043 --- /dev/null +++ b/analysis/03_identity_hiding_initiator.entry.mpv @@ -0,0 +1,25 @@ +#define INITIATOR_TEST 1 + +#include "rosenpass/03_identity_hiding.mpv" + +// nounif a:Atom, s:seed, a2:Atom; +// ConsumeSeed(a, s, a2) / 6300[conclusion]. + +nounif v:seed_prec; attacker(prepare_seed(trusted_seed( v )))/6217[hypothesis]. +nounif v:seed; attacker(prepare_seed( v ))/6216[hypothesis]. +nounif v:seed; attacker(rng_kem_sk( v ))/6215[hypothesis]. +nounif v:seed; attacker(rng_key( v ))/6214[hypothesis]. +nounif v:key_prec; attacker(prepare_key(trusted_key( v )))/6213[hypothesis]. +nounif v:kem_sk_prec; attacker(prepare_kem_sk(trusted_kem_sk( v )))/6212[hypothesis]. +nounif v:key; attacker(prepare_key( v ))/6211[hypothesis]. +nounif v:kem_sk; attacker(prepare_kem_sk( v ))/6210[hypothesis]. +nounif Spk:kem_sk_tmpl; + attacker(Creveal_kem_pk(Spk))/6110[conclusion]. +nounif sid:SessionId, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Seski:seed_tmpl, Ssptr:seed_tmpl; + attacker(Cinitiator( *sid, *Ssskm, *Spsk, *Sspkt, *Seski, *Ssptr ))/6109[conclusion]. +nounif sid:SessionId, biscuit_no:Atom, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Septi:seed_tmpl, Sspti:seed_tmpl, ih:InitHello_t; + attacker(Cinit_hello( *sid, *biscuit_no, *Ssskm, *Spsk, *Sspkt, *Septi, *Sspti, *ih ))/6108[conclusion]. +nounif rh:RespHello_t; + attacker(Cresp_hello( *rh ))/6107[conclusion]. +nounif Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t; + attacker(Cinit_conf( *Ssskm, *Spsk, *Sspkt, *ic ))/6106[conclusion]. diff --git a/analysis/03_identity_hiding_responder.entry.mpv b/analysis/03_identity_hiding_responder.entry.mpv new file mode 100644 index 0000000..5908a72 --- /dev/null +++ b/analysis/03_identity_hiding_responder.entry.mpv @@ -0,0 +1,96 @@ +#define RESPONDER_TEST 1 + +#include "rosenpass/03_identity_hiding.mpv" + +// select k:kem_pk,ih: InitHello_t; attacker(prf(prf(prf(prf(key0, PROTOCOL), MAC), kem_pk2b(k) ), IH2b(ih))) phase 1/6300[hypothesis]. + +// select epki:kem_pk, sctr:bits, pidiC:bits, auth:bits, epki2:kem_pk, sctr2:bits, pidiC2:bits, auth2:bits; +// mess(D, prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pk2b(kem_pub(trusted_kem_sk(responder1)))), +// IH2b(InitHello(secure_sidi, *epki, *sctr, *pidiC, *auth))) +// ) [hypothesis, conclusion]. + +// select epki:kem_pk, sctr:bits, pidiC:bits, auth:bits, epki2:kem_pk, sctr2:bits, pidiC2:bits, auth2:bits; +// attacker(choice[prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pk2b(kem_pub(trusted_kem_sk(responder1)))), +// IH2b(InitHello(secure_sidi, *epki, *sctr, *pidiC, *auth))), + +// prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pk2b(kem_pub(trusted_kem_sk(responder2)))), +// IH2b(InitHello(secure_sidi, *epki2, *sctr2, *pidiC2, *auth2)))] +// ) [hypothesis, conclusion]. + +// select +// attacker(prf(prf(key0,PROTOCOL),MAC)) [hypothesis, conclusion]. + +// select +// attacker(prf(key0,PROTOCOL)) [conclusion]. + +// select +// attacker(key0) [conclusion]. + +// select +// attacker(PROTOCOL) [conclusion]. + +// select +// attacker(kem_pub(trusted_kem_sk(responder1))) /9999 [hypothesis, conclusion]. + +// select +// attacker(kem_pub(trusted_kem_sk(responder2))) /9999 [hypothesis, conclusion]. + +// nounif ih:InitHello_t; +// attacker(ih) / 9999 [hypothesis]. + +// nounif rh:RespHello_t; +// attacker(rh) / 9999 [hypothesis]. + +// nounif ic:InitConf_t; +// attacker(ic) / 9999 [hypothesis]. + +// nounif k:key; +// attacker(ck_hs_enc( *k )) [hypothesis, conclusion]. + +// nounif k:key; +// attacker(ck_hs_enc( *k )) phase 1 [hypothesis, conclusion]. + +// nounif k:key, b:bits; +// attacker(ck_mix( *k , *b )) [hypothesis, conclusion]. + +// nounif k:key, b:bits; +// attacker(ck_mix( *k , *b ))phase 1 [hypothesis, conclusion]. + +// // select k:kem_pk, epki2:kem_pk, sctr2:bits, pidiC2:bits, auth2:bits, epki:kem_pk, sctr:bits, pidiC:bits, auth:bits; +// // attacker(choice[Envelope(prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pub(trusted_kem_sk(responder1))), +// // InitHello(secure_sidi, *epki2, *sctr2, *pidiC2, *auth2) +// // ), InitHello(secure_sidi, *epki2, *sctr2, *pidiC2, *auth2)) +// // Envelope(prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pub(trusted_kem_sk(responder2))), +// // InitHello(secure_sidi, *epki, *sctr, *pidiC, *auth)), +// // InitHello(secure_sidi, *epki, *sctr, *pidiC, *auth)) +// // ]) / 9999[hypothesis, conclusion]. + +// nounif k:key, b1:bits, b2:bits; +// attacker(xaead_enc( *k, *b1, *b2)) / 9999[hypothesis,conclusion]. + +// nounif pk:kem_pk, k:key; +// attacker(kem_enc( *pk , *k )) / 9999[hypothesis,conclusion]. + +// nounif sid:SessionId, biscuit_no:Atom, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Septi:seed_tmpl, Sspti:seed_tmpl, ih:InitHello_t; +// attacker(Cinit_hello( *sid, *biscuit_no, *Ssskm, *Spsk, *Sspkt, *Septi, *Sspti, *ih ))/9999[hypothesis, conclusion]. +// nounif Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t; +// attacker(Cinit_conf( *Ssskm, *Spsk, *Sspkt, *ic ))/9999[hypothesis, conclusion]. +// nounif sid:SessionId, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Seski:seed_tmpl, Ssptr:seed_tmpl; +// attacker(Cinitiator( *sid, *Ssskm, *Spsk, *Sspkt, *Seski, *Ssptr )) /9999 [hypothesis, conclusion]. + +// nounif sid:SessionId, biscuit_no:Atom, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Septi:seed_tmpl, Sspti:seed_tmpl, ih:InitHello_t; +// mess(C, Cinit_hello( *sid, *biscuit_no, *Ssskm, *Spsk, *Sspkt, *Septi, *Sspti, *ih ))/9999[hypothesis, conclusion]. +// nounif Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t; +// mess(C, Cinit_conf( *Ssskm, *Spsk, *Sspkt, *ic ))/9999[hypothesis, conclusion]. +// nounif sid:SessionId, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Seski:seed_tmpl, Ssptr:seed_tmpl; +// mess(C, Cinitiator( *sid, *Ssskm, *Spsk, *Sspkt, *Seski, *Ssptr )) /9999 [hypothesis, conclusion]. +// nounif rh:RespHello_t; +// attacker(Cresp_hello( *rh ))[conclusion]. +// nounif v:seed_prec; attacker(prepare_seed(trusted_seed( v )))/6217[hypothesis]. +// nounif v:seed; attacker(prepare_seed( v ))/6216[hypothesis]. +// nounif v:seed; attacker(rng_kem_sk( v ))/6215[hypothesis]. +// nounif v:seed; attacker(rng_key( v ))/6214[hypothesis]. +// nounif v:key_prec; attacker(prepare_key(trusted_key( v )))/6213[hypothesis]. +// nounif v:kem_sk_prec; attacker(prepare_kem_sk(trusted_kem_sk( v )))/6212[hypothesis]. +// nounif v:key; attacker(prepare_key( v ))/6211[hypothesis]. +// nounif v:kem_sk; attacker(prepare_kem_sk( v ))/6210[hypothesis]. diff --git a/analysis/03_identity_hiding_test.entry.mpv b/analysis/03_identity_hiding_test.entry.mpv new file mode 100644 index 0000000..1c7afc5 --- /dev/null +++ b/analysis/03_identity_hiding_test.entry.mpv @@ -0,0 +1,29 @@ +#define INITIATOR_TEST 1 +#define CUSTOM_MAIN 1 + +#include "rosenpass/03_identity_hiding.mpv" + +let Oinitiator_bad_actor_inner(sk_tmp:kem_sk_prec) = + + in(C, Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr)); + + #if RANDOMIZED_CALL_IDS + new call:Atom; + #else + call <- Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr); + #endif + + in(C, last_cookie:key); + tmpl <- make_trusted_kem_sk(sk_tmp); + out(C, setup_kem_sk(tmpl)); + Oinitiator_inner(sidi, Ssskm, Spsk, tmpl, Seski, Ssptr, last_cookie, C, call). + +let Oinitiator_bad_actor() = + Oinitiator_bad_actor_inner(responder1) | Oinitiator_bad_actor_inner(responder2) | Oinitiator_bad_actor_inner(initiator1) | Oinitiator_bad_actor_inner(initiator2). + + +let identity_hiding_main2() = + 0 | Oinitiator_bad_actor() | rosenpass_main2() | participants_communication() | phase 1; secretCommunication(). + + +let main = identity_hiding_main2. diff --git a/analysis/03_identity_hiding.entry.mpv b/analysis/rosenpass/03_identity_hiding.mpv similarity index 65% rename from analysis/03_identity_hiding.entry.mpv rename to analysis/rosenpass/03_identity_hiding.mpv index 985fda0..112ed6c 100644 --- a/analysis/03_identity_hiding.entry.mpv +++ b/analysis/rosenpass/03_identity_hiding.mpv @@ -28,7 +28,6 @@ In this case the test uses secure rng and a fresh secure biscuit key. */ - #include "config.mpv" #define CHAINING_KEY_EVENTS 1 @@ -44,7 +43,6 @@ #include "rosenpass/oracles.mpv" #include "crypto/kem.mpv" -#define INITIATOR_TEST #define NEW_TRUSTED_SEED(name) \ new MCAT(name, _secret_seed):seed_prec; \ name <- make_trusted_seed(MCAT(name, _secret_seed)); \ @@ -57,52 +55,86 @@ free initiator1, initiator2:kem_sk_prec. free responder1, responder2:kem_sk_prec. let secure_init_hello(initiator: kem_sk_tmpl, sidi : SessionId, psk: key_tmpl, responder: kem_sk_tmpl) = + + new epkit:kem_pk; // epki + new sctrt:bits; // sctr + new pidiCt:bits; // pidiC + new autht:bits; // auth + NEW_TRUSTED_SEED(seski_trusted_seed) NEW_TRUSTED_SEED(ssptr_trusted_seed) - Oinitiator_inner(sidi, initiator, psk, responder, seski_trusted_seed, ssptr_trusted_seed, D). + new last_cookie:key; + new call:Atom; + + Oinitiator_inner(sidi, initiator, psk, responder, seski_trusted_seed, ssptr_trusted_seed, last_cookie, D, call). + +let secure_resp_hello(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, sidi:SessionId, sidr:SessionId, biscuit_no:Atom, psk:key_tmpl) = + + in(D, InitHello(=secure_sidi, epki, sctr, pidiC, auth)); -let secure_resp_hello(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, sidr:SessionId, sidi:SessionId, biscuit_no:Atom, psk:key_tmpl) = - in(D, Envelope(k, IH2b(InitHello(=sidi, epki, sctr, pidiC, auth)))); ih <- InitHello(sidi, epki, sctr, pidiC, auth); NEW_TRUSTED_SEED(septi_trusted_seed) NEW_TRUSTED_SEED(sspti_trusted_seed) - Oinit_hello_inner(sidr, biscuit_no, responder, psk, initiator, septi_trusted_seed, sspti_trusted_seed, ih, D). + new last_cookie:key; + new call:Atom; + + Oinit_hello_inner(sidr, biscuit_no, responder, psk, initiator, septi_trusted_seed, sspti_trusted_seed, ih, last_cookie, D, call). let secure_init_conf(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, psk:key_tmpl, sidi:SessionId, sidr:SessionId) = - in(D, Envelope(k3, IC2b(InitConf(=sidi, =sidr, biscuit, auth3)))); + in(D, InitConf(=sidi, =sidr, biscuit, auth3)); ic <- InitConf(sidi,sidr,biscuit, auth3); NEW_TRUSTED_SEED(seski_trusted_seed) NEW_TRUSTED_SEED(ssptr_trusted_seed) - Oinit_conf_inner(initiator, psk, responder, ic). + new last_cookie:key; + call <- Cinit_conf(initiator, psk, responder, ic); -let secure_communication(initiator: kem_sk_tmpl, responder:kem_sk_tmpl) = - secure_key <- prepare_key(secure_psk); - (!secure_init_hello(initiator, secure_sidi, secure_key, responder)) - | !secure_resp_hello(initiator, responder, secure_sidr, secure_sidi, secure_biscuit_no, secure_key) - | !(secure_init_conf(initiator, responder, secure_key, secure_sidi, secure_sidr)). + Oinit_conf_inner(initiator, psk, responder, ic, call). + +let secure_communication(initiator: kem_sk_tmpl, responder:kem_sk_tmpl, key:key) = + key_tmpl <- prepare_key(key); + (!secure_init_hello(initiator, secure_sidi, key_tmpl, responder)) + | !secure_resp_hello(initiator, responder, secure_sidi, secure_sidr, secure_biscuit_no, key_tmpl) + | !(secure_init_conf(initiator, responder, key_tmpl, secure_sidi, secure_sidr)). + +let participant_communication_initiator(participant:kem_sk_tmpl) = + in(C, responder:kem_sk_tmpl); + in(C, k:key); + secure_communication(participant, responder, k). + +let participant_communication_responder(participant:kem_sk_tmpl) = + in(C, initiator:kem_sk_tmpl); + in(C, k:key); + secure_communication(initiator, participant, k). + +let participants_communication() = + initiator1_tmpl <- make_trusted_kem_sk(initiator1); + initiator2_tmpl <- make_trusted_kem_sk(initiator2); + responder1_tmpl <- make_trusted_kem_sk(responder1); + responder2_tmpl <- make_trusted_kem_sk(responder2); + + !participant_communication_initiator(initiator1_tmpl) | !participant_communication_responder(initiator1_tmpl) + | !participant_communication_initiator(initiator2_tmpl) | !participant_communication_responder(initiator2_tmpl) + | !participant_communication_initiator(responder1_tmpl) | !participant_communication_responder(responder1_tmpl) + | !participant_communication_initiator(responder2_tmpl) | !participant_communication_responder(responder2_tmpl). let pipeChannel(D:channel, C:channel) = in(D, b:bits); out(C, b). -fun kem_private(kem_pk): kem_sk - reduc forall sk_tmpl:kem_sk; - kem_private(kem_pub(sk_tmpl)) = sk_tmpl[private]. - let secretCommunication() = + #ifdef INITIATOR_TEST - initiator_pk <- choice[setup_kem_pk(make_trusted_kem_sk(initiator1)), setup_kem_pk(make_trusted_kem_sk(initiator2))]; - initiator_seed <- prepare_kem_sk(kem_private(initiator_pk)); + initiator_seed <- choice[make_trusted_kem_sk(initiator1), make_trusted_kem_sk(initiator2)]; #else - initiator_seed <- prepare_kem_sk(trusted_kem_sk(initiator1)); + initiator_seed <- make_trusted_kem_sk(initiator1); #endif #ifdef RESPONDER_TEST - responder_pk <- choice[setup_kem_pk(make_trusted_kem_sk(responder1)), setup_kem_pk(make_trusted_kem_sk(responder2))]; - responder_seed <- prepare_kem_sk(kem_private(responder_pk)); + responder_seed <- choice[make_trusted_kem_sk(responder1), make_trusted_kem_sk(responder2)]; #else - responder_seed <- prepare_kem_sk(trusted_kem_sk(responder1)); + responder_seed <- make_trusted_kem_sk(responder1); #endif - secure_communication(initiator_seed, responder_seed) | !pipeChannel(D, C). + + secure_communication(initiator_seed, responder_seed, secure_psk) | !pipeChannel(D, C). let reveal_pks() = out(C, setup_kem_pk(make_trusted_kem_sk(responder1))); @@ -116,6 +148,8 @@ let rosenpass_main2() = | REP(RESPONDER_BOUND, Oinit_conf). let identity_hiding_main() = - 0 | reveal_pks() | rosenpass_main2() | phase 1; secretCommunication(). + 0 | reveal_pks() | rosenpass_main2() | participants_communication() | phase 1; secretCommunication(). +#ifndef CUSTOM_MAIN let main = identity_hiding_main. +#endif