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.

2026-02-28 06:23:08 -08:00 · 2023-11-25 20:49:32 -05:00
parent 8027ccbf38
commit 0cdd06031b
4 changed files with 142 additions and 109 deletions
--- a/analysis/03_identity_hiding.entry.mpv
+++ b/analysis/03_identity_hiding.entry.mpv
@@ -4,28 +4,109 @@
 #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 C2:channel.
+free D:channel [private].
+free secure_biscuit_no:Atom [private].
+free secure_sidi,secure_sidr:SessionId [private].
+free secure_psk:key [private].
+free secure_septi_trusted_prec: seed_prec [private].
+free secure_sspti_trusted_prec: seed_prec [private].
+free secure_seski_trusted_prec: seed_prec [private].
+free secure_ssptr_trusted_prec: seed_prec [private].
+free initiator1, initiator2:kem_sk_prec[private].
+free responder1, responder2:kem_sk_prec[private].
+
+let secure_init_hello2(initiator: kem_sk_tmpl, sidi : SessionId, psk: key_tmpl, responder: kem_sk_tmpl, C:channel) =
+  NEW_TRUSTED_SEED(seski_trusted_seed)
+  NEW_TRUSTED_SEED(ssptr_trusted_seed)
+  Oinitiator_inner(sidi, initiator, psk, responder, seski_trusted_seed, ssptr_trusted_seed, C).
+
+let secure_resp_hello2(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, sidr:SessionId, sidi:SessionId, biscuit_no:Atom, psk:key_tmpl, C:channel) =
+  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, C).
+
+let secure_init_conf2(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, psk:key_tmpl, sidi:SessionId, sidr:SessionId, C:channel) =
+  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, C).
+
+fun Csecure_init_hello(SessionId, key_tmpl, kem_sk_tmpl): Atom[data].
+let secure_init_hello(initiator: kem_sk_tmpl) =
+  NEW_TRUSTED_SEED(seski_trusted_seed)
+  NEW_TRUSTED_SEED(ssptr_trusted_seed)
+  in(C, Csecure_init_hello(sidi, psk, responder));
+  Oinitiator_inner(sidi, initiator, psk, responder, seski_trusted_seed, ssptr_trusted_seed, C).
+
+fun Csecure_resp_hello(SessionId, SessionId, Atom, key_tmpl, kem_sk_tmpl, InitHello_t): Atom[data].
+let secure_resp_hello(initiator: kem_sk_tmpl) =
+  NEW_TRUSTED_SEED(septi_trusted_seed)
+  NEW_TRUSTED_SEED(sspti_trusted_seed)
+  in(C, Csecure_resp_hello(sidr, sidi, biscuit_no, psk, responder, ih));
+  Oinit_hello_inner(sidr, biscuit_no, responder, psk, initiator, septi_trusted_seed, sspti_trusted_seed, ih, C).
+
+fun Csecure_init_conf(key_tmpl, kem_sk_tmpl, InitConf_t): Atom[data].
+let secure_init_conf(initiator: kem_sk_tmpl) =
+  NEW_TRUSTED_SEED(seski_trusted_seed)
+  NEW_TRUSTED_SEED(ssptr_trusted_seed)
+  in(C, Csecure_init_conf(psk, responder, ic));
+  Oinit_conf_inner(initiator, psk, responder, ic, C).
+
+let secure_communication(initiator: kem_sk_tmpl, responder:kem_sk_tmpl, C:channel) =
+  secure_key <- prepare_key(secure_psk);
+  (!secure_init_hello2(initiator, secure_sidi, secure_key, responder, C))
+  | !secure_resp_hello2(initiator, responder, secure_sidr, secure_sidi, secure_biscuit_no, secure_key, C)
+  | !(secure_init_conf2(initiator, responder, secure_key, secure_sidi, secure_sidr, C)).
+
+let run_secure_protocols(participant:kem_sk_tmpl) =
+  !(secure_init_hello(participant)) 
+  | !(secure_resp_hello(participant))
+  | !(secure_init_conf(participant)).
+
+let secure_particpant_communication() = 0
+  | !run_secure_protocols(make_trusted_kem_sk(responder1)) | !run_secure_protocols(make_trusted_kem_sk(responder2)) 
+  | !run_secure_protocols(make_trusted_kem_sk(initiator1)) | !run_secure_protocols(make_trusted_kem_sk(initiator2)).
+
+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() =
+  responder_pk <- choice[setup_kem_pk(make_trusted_kem_sk(responder1)), setup_kem_pk(make_trusted_kem_sk(responder2))];
+  kem_seed <- prepare_kem_sk(kem_private(responder_pk));
+  kem_pk <- setup_kem_pk(kem_seed);
+  initiator_seed <- prepare_kem_sk(trusted_kem_sk(initiator1));
+  secure_communication(initiator_seed, kem_seed, D) | !pipeChannel(D, C2).
+
+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 identity_hiding_main() = 
+  0 | reveal_pks() | secure_particpant_communication() | phase 1; secretCommunication().

-let identity_hiding_main() = 0
-  | REP(INITIATOR_BOUND, Oinitiator)
-  | REP(RESPONDER_BOUND, Oinit_hello)
-  | REP(RESPONDER_BOUND, Oinit_conf).

 let main = identity_hiding_main.
-
-weaksecret initiator_pk.
-weaksecret responder_pk.
--- 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, C_in:channel) =
 #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;
@@ -83,6 +75,10 @@ let Oinit_conf() =
 #endif
  ).
  
+let Oinit_conf() = 
+  in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic));
+  Oinit_conf_inner(Ssskm, Spsk, Sspkt, ic, C).
+
 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))
    ==> ad1 = 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_in: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_in, 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() =
-  in(C, Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr));
-#if RANDOMIZED_CALL_IDS
+let Oinitiator_inner(sidi: SessionId, Ssskm: kem_sk_tmpl, Spsk: key_tmpl, Sspkt: kem_sk_tmpl, Seski: seed_tmpl, Ssptr: seed_tmpl, C_in:channel) =
+  #if RANDOMIZED_CALL_IDS
    new call:Atom;
-#else
+  #else
    call <- Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr);
-#endif
+  #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).
+    out(C_in, Envelope(create_mac(spkt, IH2b(ih)), IH2b(ih)));
+    Oresp_hello(HS_PASS_ARGS, C).
+
+let Oinitiator() =
+  in(C, Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr));
+  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,7 +49,6 @@ fun RespHello(
    bits       // auth
 ) : RespHello_t [data].

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

 #define RESPHELLO_PRODUCE()  \
@@ -82,7 +77,6 @@ fun InitConf(
    bits       // auth
 ) : InitConf_t [data].

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

 #define INITCONF_PRODUCE()                  \