diff --git a/analysis/03_identity_hiding.entry.mpv b/analysis/03_identity_hiding.entry.mpv
index d18d425..56dff17 100644
--- 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.
diff --git a/analysis/crypto/kem.mpv b/analysis/crypto/kem.mpv
index 168263a..edfbe1d 100644
--- 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].
 
diff --git a/analysis/rosenpass/oracles.mpv b/analysis/rosenpass/oracles.mpv
index 0825f7a..d1c7f44 100644
--- 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;
@@ -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, 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))
@@ -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_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
+    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_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));
-#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))
diff --git a/analysis/rosenpass/protocol.mpv b/analysis/rosenpass/protocol.mpv
index 9874cf4..a900981 100644
--- 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()                  \