feat: add inital identity hiding code to proverif

2026-02-27 14:03:11 -08:00 · 2023-11-22 20:11:04 -05:00
parent 7c83e244f9
commit 4a170b1983
4 changed files with 122 additions and 7 deletions
--- a/analysis/03_identity_hiding.entry.mpv
+++ b/analysis/03_identity_hiding.entry.mpv
@@ -0,0 +1,31 @@
+#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 "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)).
+
+#include "rosenpass/oracles.mpv"
+
+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,10 +9,13 @@ 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.
+    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.

 fun kem_pk2b(kem_pk) : bits [typeConverter].

--- a/analysis/rosenpass/oracles.mpv
+++ b/analysis/rosenpass/oracles.mpv
@@ -54,7 +54,17 @@ let Oinit_conf() =
 #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;
  let try_ = (
@@ -98,7 +108,7 @@ let Oresp_hello(HS_DECL_ARGS) =
    SES_EV( event InitiatorSession(rh, osk); )
    ic
  /* success */ ) in (
-    out(C, ic)
+    out(C, EnvelopeInitConf(create_mac(spkt, IC2b(ic)), ic))
  /* fail */ ) else (
 #if MESSAGE_TRANSMISSION_EVENTS
    event RHRjct(rh, psk, sski, spkr)
@@ -125,14 +135,40 @@ let Oinit_hello() =
 #endif
  // 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;
-  epti <- rng_key(setup_seed(Septi)); // RHR4
-  spti <- rng_key(setup_seed(Sspti)); // RHR5
+
  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()
    ck_ini <- ck;
@@ -141,7 +177,7 @@ let Oinit_hello() =
    MTX_EV( event RHSent(ih, rh, psk, sskr, spki); )
    rh
  /* success */ ) in (
-    out(C, rh)
+    out(C, EnvelopeRespHello(create_mac(spkt, RH2b(rh)), rh))
  /* fail */ ) else (
 #if MESSAGE_TRANSMISSION_EVENTS
    event IHRjct(ih, psk, sskr, spki)
@@ -167,6 +203,7 @@ CK_EV( event OskOinitiator_ck(key). )
 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
@@ -174,18 +211,44 @@ let Oinitiator() =
 #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()
-  RNG_KEM_PAIR(eski, epki, Seski) // IHI3
+#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, ih);
+  out(C, EnvelopeInitHello(create_mac(spkt, IH2b(ih) ), ih));
  Oresp_hello(HS_PASS_ARGS).

 restriction sid:SessionId, ad1:Atom, ad2:Atom;
--- a/analysis/rosenpass/protocol.mpv
+++ b/analysis/rosenpass/protocol.mpv
@@ -2,6 +2,15 @@
 #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].
+
+letfun create_mac(pk:kem_pk, payload:bits) = lprf2(MAC, kem_pk2b(pk), payload).
+
 type InitHello_t.
 fun InitHello(
  SessionId, // sidi
@@ -11,6 +20,9 @@ fun InitHello(
  bits       // auth
 ) : InitHello_t [data].

+ENVELOPE(InitHello)
+fun IH2b(InitHello_t) : bitstring [typeConverter].
+
 #define INITHELLO_PRODUCE()       \
  ck <- lprf1(CK_INIT, kem_pk2b(spkr)); /* IHI1 */ \
  /* not handled here */                /* IHI2 */ \
@@ -41,6 +53,9 @@ fun RespHello(
    bits       // auth
 ) : RespHello_t [data].

+ENVELOPE(RespHello)
+fun RH2b(RespHello_t) : bitstring [typeConverter].
+
 #define RESPHELLO_PRODUCE()                   \
  /* not handled here */           /* RHR1 */ \
  MIX2(sid2b(sidr), sid2b(sidi))   /* RHR3 */ \
@@ -67,6 +82,9 @@ fun InitConf(
    bits       // auth
 ) : InitConf_t [data].

+ENVELOPE(InitConf)
+fun IC2b(InitConf_t) : bitstring [typeConverter].
+
 #define INITCONF_PRODUCE()                  \
  MIX2(sid2b(sidi), sid2b(sidr)) /* ICI3 */ \
  ENCRYPT_AND_MIX(auth, empty)   /* ICI4 */ \