From 70d136dbd37951443ed6a40e53da6e8b68ae9c5d Mon Sep 17 00:00:00 2001 From: James Brownlee Date: Fri, 15 Dec 2023 10:55:16 -0500 Subject: [PATCH] added INITIATOR_TEST and RESPONDER_TEST macros to the identity hiding mpv file that can be used to selectively test the anonymity of the initiator or the responder --- analysis/03_identity_hiding.entry.mpv | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) 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() =