diff --git a/analysis/03_identity_hiding.entry.mpv b/analysis/03_identity_hiding.entry.mpv index 93c9389..1a224d6 100644 --- a/analysis/03_identity_hiding.entry.mpv +++ b/analysis/03_identity_hiding.entry.mpv @@ -13,6 +13,7 @@ #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)); \ @@ -58,12 +59,18 @@ fun kem_private(kem_pk): 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)); +#else + initiator_seed <- prepare_kem_sk(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)); +#else responder_seed <- prepare_kem_sk(trusted_kem_sk(responder1)); - // initiator_seed <- prepare_kem_sk(trusted_kem_sk(initiator1)); - // 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)); +#endif secure_communication(initiator_seed, responder_seed) | !pipeChannel(D, C). let reveal_pks() =