feat: identity hiding in two stage process

Changed identity hiding test to work as a two stage process where participants with fresh secure secret keys communicate with each other and other compromised participants. Then the attacker is asked to identify the difference between two of the secure participants as on of them acts as a responder.
2025-12-05 20:40:02 -08:00 · 2023-11-25 20:49:32 -05:00
parent 4a170b1983
commit 91da0dfd2d
4 changed files with 142 additions and 107 deletions
--- a/analysis/03_identity_hiding.entry.mpv
+++ b/analysis/03_identity_hiding.entry.mpv
@@ -1,31 +1,114 @@
+/*
+  This identity hiding process tests whether the rosenpass protocol is able to protect the identity of an initiator or responder.
+  The participants in the test are trusted initiators, trusted responders and compromised initiators and responders.
+  The test consists of two phases. In the first phase all of the participants can communicate with each other using the rosenpass protocol.
+  An attacker observes the first phase and is able to intercept and modify messages and choose participants to communicate with each other
+
+  In the second phase if the anonymity of an initiator is being tested then one of two trusted initiators is chosen.
+  The chosen initiator communicates directly with a trusted responder.
+  If an attacker can determine which initiator was chosen then the anonymity of the initiator has been compromised.
+  Otherwise the protocol has successfully protected the initiators’ identity.
+
+  If the anonymity of a responder is being tested then one of two trusted responders is chosen instead.
+  Then an initiator communicates directly with the chosen responder.
+  If an attacker can determine which responder was chosen then the anonymity of the responder is compromised.
+  Otherwise the protocol successfully protects the identity of a responder.
+
+  The Proverif code treats the public key as synonymous with identity.
+  In the above test when a responder or initiator is chosen what is actually chosen is the public/private key pair to use for communication.
+  Traditionally when a responder or initiator is chosen they would be chosen randomly.
+  The way Proverif makes a "choice" is by simulating multiple processes, one process per choice
+  Then the processes are compared and if an association between a public key and a process can be made the test fails.
+  As the choice is at least as bad as choosing the worst possible option the credibility of the test is maintained.
+  The drawback is that Proverif is only able to tell if the identity can be brute forced but misses any probabilistic associations.
+  As usual Proverif also assumes perfect encryption and in particular assumes encryption cannot be linked to identity.
+
+  One of the tradeoffs made here is that the choice function in Proverif is slow but this is in favour of being able to write more precise tests.
+  Another issue is the choice function does not work with queries so a test needs to be run for each set of assumptions.
+  In this case the test uses secure rng and a fresh secure biscuit key.
+*/
+
+
 #include "config.mpv"

 #define CHAINING_KEY_EVENTS 1
 #define MESSAGE_TRANSMISSION_EVENTS 1
 #define SESSION_START_EVENTS 0
 #define RANDOMIZED_CALL_IDS 0
-#define CONSTANT_KEYS 1
-#define SECURE_RNG 1
 #undef FULL_MODEL
 #undef SIMPLE_MODEL
 #define SIMPLE_MODEL 1

 #include "prelude/basic.mpv"
 #include "crypto/key.mpv"
+#include "rosenpass/oracles.mpv"
 #include "crypto/kem.mpv"

-//free initiator_sk1, initiator_sk2, responder_sk: kem_sk [private].
-free initiator_pk, responder_pk: kem_pk[private].
-// noninterf initiator_pk among(kem_pub(initiator_sk1), kem_pub(initiator_sk2)).
+#define NEW_TRUSTED_SEED(name)            \
+  new MCAT(name, _secret_seed):seed_prec; \
+  name <- make_trusted_seed(MCAT(name, _secret_seed)); \

-#include "rosenpass/oracles.mpv"
+free D:channel [private].
+free secure_biscuit_no:Atom [private].
+free secure_sidi,secure_sidr:SessionId [private].
+free secure_psk:key [private].
+free initiator1, initiator2:kem_sk_prec.
+free responder1, responder2:kem_sk_prec.

-let identity_hiding_main() = 0
-  | REP(INITIATOR_BOUND, Oinitiator)
+let secure_init_hello(initiator: kem_sk_tmpl, sidi : SessionId, psk: key_tmpl, responder: kem_sk_tmpl) =
+  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).
+
+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).
+
+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))));
+  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).
+
+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)).
+
+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() =
+  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)); 
+  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));
+  secure_communication(initiator_seed, responder_seed) | !pipeChannel(D, C).
+
+let reveal_pks() =
+  out(C, setup_kem_pk(make_trusted_kem_sk(responder1)));
+  out(C, setup_kem_pk(make_trusted_kem_sk(responder2)));
+  out(C, setup_kem_pk(make_trusted_kem_sk(initiator1)));
+  out(C, setup_kem_pk(make_trusted_kem_sk(initiator2))).
+
+let rosenpass_main2() = 
+  REP(INITIATOR_BOUND, Oinitiator)
  | REP(RESPONDER_BOUND, Oinit_hello)
  | REP(RESPONDER_BOUND, Oinit_conf).

-let main = identity_hiding_main.
+let identity_hiding_main() = 
+  0 | reveal_pks() |  rosenpass_main2() | phase 1; secretCommunication().

-weaksecret initiator_pk.
-weaksecret responder_pk.
+let main = identity_hiding_main.
--- a/analysis/crypto/kem.mpv
+++ b/analysis/crypto/kem.mpv
@@ -9,13 +9,10 @@ type kem_sk.
 type kem_pk.

 fun kem_pub(kem_sk) : kem_pk.
-fun kem_private(kem_pk) : kem_sk[private].
 fun kem_enc(kem_pk, key) : bits.
 fun kem_dec(kem_sk, bits) : key
  reduc forall sk:kem_sk, shk:key;
-    kem_dec(sk, kem_enc(kem_pub(sk), shk)) = shk
-  otherwise forall pk:kem_pk, shk:key;
-    kem_dec(kem_private(pk), kem_enc(pk, shk)) = shk.
+    kem_dec(sk, kem_enc(kem_pub(sk), shk)) = shk.

 fun kem_pk2b(kem_pk) : bits [typeConverter].

--- a/analysis/rosenpass/oracles.mpv
+++ b/analysis/rosenpass/oracles.mpv
@@ -47,23 +47,15 @@ CK_EV(  event OskOinit_conf(key, key). )
 MTX_EV( event ICRjct(InitConf_t, key, kem_sk, kem_pk). )
 SES_EV( event ResponderSession(InitConf_t, key). )
 event ConsumeBiscuit(Atom, kem_sk, kem_pk, Atom).
-let Oinit_conf() = 
-  in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic));
+
+let Oinit_conf_inner(Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t) =
 #if RANDOMIZED_CALL_IDS
  new call:Atom;
 #else
  call <- Cinit_conf(Ssskm, Spsk, Sspkt, ic);
 #endif

-#ifdef CONSTANT_KEYS 
-  spkt <- initiator_pk;
-  spkm <- responder_pk;
-  sskm <- kem_private(spkm);
-  psk  <- setup_key(Spsk);
-  biscuit_key <- biscuit_key(sskm);
-#else
  SETUP_HANDSHAKE_STATE()
-#endif

  eski <- kem_sk0;
  epki <- kem_pk0;
@@ -82,6 +74,10 @@ let Oinit_conf() =
    0
 #endif
  ).
+  
+let Oinit_conf() = 
+  in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic));
+  Oinit_conf_inner(Ssskm, Spsk, Sspkt, ic).

 restriction biscuit_no:Atom, sskm:kem_sk, spkr:kem_pk, ad1:Atom, ad2:Atom;
  event(ConsumeBiscuit(biscuit_no, sskm, spkr, ad1)) && event(ConsumeBiscuit(biscuit_no, sskm, spkr, ad2))
@@ -95,8 +91,8 @@ CK_EV(  event OskOresp_hello(key, key, key). )
 MTX_EV( event RHRjct(RespHello_t, key, kem_sk, kem_pk). )
 MTX_EV( event ICSent(RespHello_t, InitConf_t, key, kem_sk, kem_pk). )
 SES_EV( event InitiatorSession(RespHello_t, key). )
-let Oresp_hello(HS_DECL_ARGS) =
-  in(C, Cresp_hello(RespHello(sidr, =sidi, ecti, scti, biscuit, auth)));
+let Oresp_hello(HS_DECL_ARGS, C_in:channel) =
+  in(C_in, Cresp_hello(RespHello(sidr, =sidi, ecti, scti, biscuit, auth)));
  rh <- RespHello(sidr, sidi, ecti, scti, biscuit, auth);
  /* try */ let ic = (
    ck_ini <- ck;
@@ -108,7 +104,7 @@ let Oresp_hello(HS_DECL_ARGS) =
    SES_EV( event InitiatorSession(rh, osk); )
    ic
  /* success */ ) in (
-    out(C, EnvelopeInitConf(create_mac(spkt, IC2b(ic)), ic))
+    out(C_in, Envelope(create_mac(spkt, IC2b(ic)), IC2b(ic)))
  /* fail */ ) else (
 #if MESSAGE_TRANSMISSION_EVENTS
    event RHRjct(rh, psk, sski, spkr)
@@ -126,8 +122,8 @@ MTX_EV( event IHRjct(InitHello_t, key, kem_sk, kem_pk). )
 MTX_EV( event RHSent(InitHello_t, RespHello_t, key, kem_sk, kem_pk). )
 event ConsumeSidr(SessionId, Atom).
 event ConsumeBn(Atom, kem_sk, kem_pk, Atom).
-let Oinit_hello() = 
-  in(C, Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih));
+
+let Oinit_hello_inner(sidm:SessionId, biscuit_no:Atom, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt: kem_sk_tmpl, Septi: seed_tmpl, Sspti: seed_tmpl, ih: InitHello_t, C_out:channel) = 
 #if RANDOMIZED_CALL_IDS
  new call:Atom;
 #else
@@ -136,38 +132,17 @@ let Oinit_hello() =
  // TODO: This is ugly
  let InitHello(sidi, epki, sctr, pidiC, auth) = ih in

-#ifdef CONSTANT_KEYS 
-  spkt <- initiator_pk;
-  spkm <- responder_pk;
-  sskm <- kem_private(spkm);
-  psk  <- setup_key(Spsk);
-  biscuit_key <- biscuit_key(sskm);
-#else
  SETUP_HANDSHAKE_STATE()
-#endif

  eski <- kem_sk0;

  event ConsumeBn(biscuit_no, sskm, spkt, call);
  event ConsumeSidr(sidr, call);

-#ifdef SECURE_RNG
-  new septi_trusted_prec: seed_prec;
-  new sspti_trusted_prec: seed_prec;
-
-  septi_trusted_seed <- make_trusted_seed(septi_trusted_prec);
-  sspti_trusted_seed <- make_trusted_seed(sspti_trusted_prec);
-
-  epti <- rng_key(setup_seed(septi_trusted_seed)); // RHR4
-  spti <- rng_key(setup_seed(sspti_trusted_seed)); // RHR4
-  event ConsumeSeed(Epti, setup_seed(septi_trusted_seed), call);
-  event ConsumeSeed(Spti, setup_seed(sspti_trusted_seed), call);
-#else
  epti <- rng_key(setup_seed(Septi)); // RHR4
  spti <- rng_key(setup_seed(Sspti)); // RHR5
  event ConsumeSeed(Epti, setup_seed(Septi), call);
  event ConsumeSeed(Spti, setup_seed(Sspti), call);
-#endif

  let rh = (
    INITHELLO_CONSUME()
@@ -177,7 +152,8 @@ let Oinit_hello() =
    MTX_EV( event RHSent(ih, rh, psk, sskr, spki); )
    rh
  /* success */ ) in (
-    out(C, EnvelopeRespHello(create_mac(spkt, RH2b(rh)), rh))
+    out(C_out, Envelope(create_mac(spkt, RH2b(rh)), RH2b(rh)))
+
  /* fail */ ) else (
 #if MESSAGE_TRANSMISSION_EVENTS
    event IHRjct(ih, psk, sskr, spki)
@@ -186,6 +162,10 @@ let Oinit_hello() =
 #endif
  ).

+let Oinit_hello() = 
+  in(C, Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih));
+  Oinit_hello_inner(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih, C).
+
 restriction sid:SessionId, ad1:Atom, ad2:Atom;
  event(ConsumeSidr(sid, ad1)) && event(ConsumeSidr(sid, ad2))
    ==> ad1 = ad2.
@@ -204,52 +184,33 @@ CK_EV( event OskOinitiator(key, key, kem_sk, kem_pk, key). )
 MTX_EV( event IHSent(InitHello_t, key, kem_sk, kem_pk). )
 event ConsumeSidi(SessionId, Atom).

+let Oinitiator_inner(sidi: SessionId, Ssskm: kem_sk_tmpl, Spsk: key_tmpl, Sspkt: kem_sk_tmpl, Seski: seed_tmpl, Ssptr: seed_tmpl, C_out:channel) =
+  #if RANDOMIZED_CALL_IDS
+    new call:Atom;
+  #else
+    call <- Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr);
+  #endif
+
+    SETUP_HANDSHAKE_STATE()
+
+    sidr <- sid0;
+
+    RNG_KEM_PAIR(eski, epki, Seski) // IHI3
+    sptr <- rng_key(setup_seed(Ssptr)); // IHI5
+    event ConsumeSidi(sidi, call);
+    event ConsumeSeed(Sptr, setup_seed(Ssptr), call);
+    event ConsumeSeed(Eski, setup_seed(Seski), call);
+
+    INITHELLO_PRODUCE()
+    CK_EV( event OskOinitiator_ck(ck); ) 
+    CK_EV( event OskOinitiator(ck, psk, sski, spkr, sptr); )
+    MTX_EV( event IHSent(ih, psk, sski, spkr); )
+    out(C_out, Envelope(create_mac(spkt, IH2b(ih)), IH2b(ih)));
+    Oresp_hello(HS_PASS_ARGS, C_out).
+
 let Oinitiator() =
  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
-
-#ifdef CONSTANT_KEYS 
-  spkt <- responder_pk;
-  spkm <- initiator_pk;
-  sskm <- kem_private(spkm);
-  psk  <- setup_key(Spsk);
-  biscuit_key <- biscuit_key(sskm);
-#else
-  SETUP_HANDSHAKE_STATE()
-#endif
-
-  sidr <- sid0;
-
-#ifdef SECURE_RNG
-  new ssptr_trusted_prec: seed_prec;
-  new seski_trusted_prec: seed_prec;
-
-  ssptr_trusted_seed <- make_trusted_seed(ssptr_trusted_prec);
-  seski_trusted_seed <- make_trusted_seed(seski_trusted_prec);
-
-  RNG_KEM_PAIR(eski, epki, seski_trusted_seed) // IHI3
-  sptr <- rng_key(setup_seed(ssptr_trusted_seed)); // IHI5
-  event ConsumeSidi(sidi, call);
-  event ConsumeSeed(Sptr, setup_seed(ssptr_trusted_seed), call);
-  event ConsumeSeed(Eski, setup_seed(seski_trusted_seed), call);
-#else
-  RNG_KEM_PAIR(eski, epki, Seski) // IHI3
-  sptr <- rng_key(setup_seed(Ssptr)); // IHI5
-  event ConsumeSidi(sidi, call);
-  event ConsumeSeed(Sptr, setup_seed(Ssptr), call);
-  event ConsumeSeed(Eski, setup_seed(Seski), call);
-#endif
-
-  INITHELLO_PRODUCE()
-  CK_EV( event OskOinitiator_ck(ck); ) 
-  CK_EV( event OskOinitiator(ck, psk, sski, spkr, sptr); )
-  MTX_EV( event IHSent(ih, psk, sski, spkr); )
-  out(C, EnvelopeInitHello(create_mac(spkt, IH2b(ih) ), ih));
-  Oresp_hello(HS_PASS_ARGS).
+  Oinitiator_inner(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr, C).

 restriction sid:SessionId, ad1:Atom, ad2:Atom;
  event(ConsumeSidi(sid, ad1)) && event(ConsumeSidi(sid, ad2))
--- a/analysis/rosenpass/protocol.mpv
+++ b/analysis/rosenpass/protocol.mpv
@@ -2,13 +2,10 @@
 #include "crypto/kem.mpv"
 #include "rosenpass/handshake_state.mpv"

-#define ENVELOPE(TYPE)                        \
-  type MCAT(MCAT(Envelope, TYPE), _t).        \ 
-  fun CAT(Envelope, TYPE) (                   \
-    key,                                       \
-    MCAT(TYPE, _t)                           \
-  ) : MCAT(MCAT(Envelope, TYPE), _t) [data].
-
+fun Envelope(
+  key,
+  bits
+): bits [data].
 letfun create_mac(pk:kem_pk, payload:bits) = lprf2(MAC, kem_pk2b(pk), payload).

 type InitHello_t.
@@ -20,7 +17,6 @@ fun InitHello(
  bits       // auth
 ) : InitHello_t [data].

-ENVELOPE(InitHello)
 fun IH2b(InitHello_t) : bitstring [typeConverter].

 #define INITHELLO_PRODUCE()       \
@@ -53,10 +49,9 @@ fun RespHello(
    bits       // auth
 ) : RespHello_t [data].

-ENVELOPE(RespHello)
 fun RH2b(RespHello_t) : bitstring [typeConverter].

-#define RESPHELLO_PRODUCE()                   \
+#define RESPHELLO_PRODUCE()  \
  /* not handled here */           /* RHR1 */ \
  MIX2(sid2b(sidr), sid2b(sidi))   /* RHR3 */ \
  ENCAPS_AND_MIX(ecti, epki, epti) /* RHR4 */ \
@@ -82,7 +77,6 @@ fun InitConf(
    bits       // auth
 ) : InitConf_t [data].

-ENVELOPE(InitConf)
 fun IC2b(InitConf_t) : bitstring [typeConverter].

 #define INITCONF_PRODUCE()                  \