diff --git a/analysis/01_secrecy.entry.mpv b/analysis/01_secrecy.entry.mpv
index 7386339..6be684f 100644
--- a/analysis/01_secrecy.entry.mpv
+++ b/analysis/01_secrecy.entry.mpv
@@ -3,12 +3,33 @@
 #define SESSION_START_EVENTS 0
 #define RANDOMIZED_CALL_IDS 0
 
+
 #include "config.mpv"
 #include "prelude/basic.mpv"
 #include "crypto/key.mpv"
 #include "crypto/kem.mpv"
+
 #include "rosenpass/oracles.mpv"
 
+nounif v:seed_prec;   attacker(prepare_seed(trusted_seed( v )))/6217[hypothesis].
+nounif v:seed;        attacker(prepare_seed( v ))/6216[hypothesis].
+nounif v:seed;        attacker(rng_kem_sk( v ))/6215[hypothesis].
+nounif v:seed;        attacker(rng_key( v ))/6214[hypothesis].
+nounif v:key_prec;    attacker(prepare_key(trusted_key( v )))/6213[hypothesis].
+nounif v:kem_sk_prec; attacker(prepare_kem_sk(trusted_kem_sk( v )))/6212[hypothesis].
+nounif v:key;         attacker(prepare_key( v ))/6211[hypothesis].
+nounif v:kem_sk;      attacker(prepare_kem_sk( v ))/6210[hypothesis].
+nounif Spk:kem_sk_tmpl;
+  attacker(Creveal_kem_pk(Spk))/6110[conclusion].
+nounif sid:SessionId, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Seski:seed_tmpl, Ssptr:seed_tmpl;
+  attacker(Cinitiator( *sid, *Ssskm, *Spsk, *Sspkt, *Seski, *Ssptr ))/6109[conclusion].
+nounif sid:SessionId, biscuit_no:Atom, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Septi:seed_tmpl, Sspti:seed_tmpl, ih:InitHello_t;
+  attacker(Cinit_hello( *sid, *biscuit_no, *Ssskm, *Spsk, *Sspkt, *Septi, *Sspti, *ih ))/6108[conclusion].
+nounif rh:RespHello_t;
+  attacker(Cresp_hello( *rh ))/6107[conclusion].
+nounif Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t;
+  attacker(Cinit_conf( *Ssskm, *Spsk, *Sspkt, *ic ))/6106[conclusion].
+
 let main = rosenpass_main.
 
 @lemma "state coherence, initiator: Initiator accepting a RespHello message implies they also generated the associated InitHello message"
diff --git a/analysis/02_availability.entry.mpv b/analysis/02_availability.entry.mpv
index 6d05e9a..1d0807c 100644
--- a/analysis/02_availability.entry.mpv
+++ b/analysis/02_availability.entry.mpv
@@ -10,6 +10,26 @@
 
 let main = rosenpass_main.
 
+nounif v:seed_prec;   attacker(prepare_seed(trusted_seed( v )))/6217[hypothesis].
+nounif v:seed;        attacker(prepare_seed( v ))/6216[hypothesis].
+nounif v:seed;        attacker(rng_kem_sk( v ))/6215[hypothesis].
+nounif v:seed;        attacker(rng_key( v ))/6214[hypothesis].
+nounif v:key_prec;    attacker(prepare_key(trusted_key( v )))/6213[hypothesis].
+nounif v:kem_sk_prec; attacker(prepare_kem_sk(trusted_kem_sk( v )))/6212[hypothesis].
+nounif v:key;         attacker(prepare_key( v ))/6211[hypothesis].
+nounif v:kem_sk;      attacker(prepare_kem_sk( v ))/6210[hypothesis].
+nounif Spk:kem_sk_tmpl;
+  attacker(Creveal_kem_pk(Spk))/6110[conclusion].
+nounif sid:SessionId, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Seski:seed_tmpl, Ssptr:seed_tmpl;
+  attacker(Cinitiator( *sid, *Ssskm, *Spsk, *Sspkt, *Seski, *Ssptr ))/6109[conclusion].
+nounif sid:SessionId, biscuit_no:Atom, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Septi:seed_tmpl, Sspti:seed_tmpl, ih:InitHello_t;
+  attacker(Cinit_hello( *sid, *biscuit_no, *Ssskm, *Spsk, *Sspkt, *Septi, *Sspti, *ih ))/6108[conclusion].
+nounif rh:RespHello_t;
+  attacker(Cresp_hello( *rh ))/6107[conclusion].
+nounif Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t;
+  attacker(Cinit_conf( *Ssskm, *Spsk, *Sspkt, *ic ))/6106[conclusion].
+
+
 @lemma "non-interruptability: Adv cannot prevent a genuine InitHello message from being accepted"
 lemma ih:InitHello_t, psk:key, sski:kem_sk, sskr:kem_sk;
   event(IHRjct(ih, psk, sskr, kem_pub(sski)))
diff --git a/analysis/config.mpv b/analysis/config.mpv
index 5fed8df..4f7deea 100644
--- a/analysis/config.mpv
+++ b/analysis/config.mpv
@@ -88,6 +88,18 @@ set verboseCompleted=VERBOSE.
 #define SES_EV(...)
 #endif
 
+#if COOKIE_EVENTS
+#define COOKIE_EV(...) __VA_ARGS__
+#else
+#define COOKIE_EV(...)
+#endif
+
+#if KEM_EVENTS
+#define KEM_EV(...) __VA_ARGS__
+#else
+#define KEM_EV(...)
+#endif
+
 
 (* TODO: Authentication timing properties *)
 (* TODO: Proof that every adversary submitted package is equivalent to one generated by the proper algorithm using different coins. This probably requires introducing an oracle that extracts the coins used and explicitly adding the notion of coins used for Packet->Packet steps and an inductive RNG notion. *)
diff --git a/analysis/rosenpass/oracles.mpv b/analysis/rosenpass/oracles.mpv
index d21e6b2..17421c9 100644
--- a/analysis/rosenpass/oracles.mpv
+++ b/analysis/rosenpass/oracles.mpv
@@ -41,23 +41,32 @@ restriction s:seed, p1:Atom, p2:Atom, ad1:Atom, ad2:Atom;
   event(ConsumeSeed(p1, s, ad1)) && event(ConsumeSeed(p2, s, ad2))
     ==> p1 = p2 && ad1 = ad2.
 
+letfun create_mac2(k:key, msg:bits) = prf(k,msg).
+
 #include "rosenpass/responder.macro"
 fun Cinit_conf(kem_sk_tmpl, key_tmpl, kem_pk_tmpl, InitConf_t) : Atom [data].
 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));
-#if RANDOMIZED_CALL_IDS
-  new call:Atom;
-#else
-  call <- Cinit_conf(Ssskm, Spsk, Sspkt, ic);
+KEM_EV(event Oinit_conf_KemUse(SessionId, SessionId, Atom).)
+#ifdef KEM_EVENTS
+  restriction sidi:SessionId, sidr:SessionId, ad1:Atom, ad2:Atom;
+    event(Oinit_conf_KemUse(sidi, sidr, ad1)) && event(Oinit_conf_KemUse(sidi, sidr, ad2))
+      ==> ad1 = ad2.
 #endif
+event ConsumeBiscuit(Atom, kem_sk, kem_pk, Atom).
+
+fun Ccookie(key, bits) : Atom[data].
+
+let Oinit_conf_inner(Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t, call:Atom) =
+
   SETUP_HANDSHAKE_STATE()
+
   eski <- kem_sk0;
   epki <- kem_pk0;
   let try_ = (
+    let InitConf(sidi, sidr, biscuit, auth) = ic in 
+    KEM_EV(event Oinit_conf_KemUse(sidi, sidr, call);)
     INITCONF_CONSUME()
     event ConsumeBiscuit(biscuit_no, sskm, spkt, call);
     CK_EV(  event OskOinit_conf(ck_rh, osk); )
@@ -72,11 +81,21 @@ let Oinit_conf() =
     0
 #endif
   ).
+  
+let Oinit_conf() = 
+
+  in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic));
+  #if RANDOMIZED_CALL_IDS
+    new call:Atom;
+  #else
+    call <- Cinit_conf(Ssskm, Spsk, Sspkt, ic);
+  #endif
+
+  Oinit_conf_inner(Ssskm, Spsk, Sspkt, ic, call).
 
 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.
-
 // TODO: Restriction biscuit no invalidation
 
 #include "rosenpass/initiator.macro"
@@ -85,27 +104,56 @@ 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)));
-  rh <- RespHello(sidr, sidi, ecti, scti, biscuit, auth);
-  /* try */ let ic = (
-    ck_ini <- ck;
-    RESPHELLO_CONSUME()
-    ck_ih <- ck;
-    INITCONF_PRODUCE()
-    CK_EV (event OskOresp_hello(ck_ini, ck_ih, osk); ) // TODO: Queries testing that there is no duplication
-    MTX_EV( event ICSent(rh, ic, psk, sski, spkr); )
-    SES_EV( event InitiatorSession(rh, osk); )
-    ic
-  /* success */ ) in (
-    out(C, ic)
-  /* fail */ ) else (
-#if MESSAGE_TRANSMISSION_EVENTS
-    event RHRjct(rh, psk, sski, spkr)
-#else
-    0
+
+KEM_EV(event Oresp_hello_KemUse(SessionId, SessionId, Atom).)
+#ifdef KEM_EVENTS
+restriction sidi:SessionId, sidr:SessionId, ad1:Atom, ad2:Atom;
+  event(Oresp_hello_KemUse(sidi, sidr, ad1)) && event(Oresp_hello_KemUse(sidi, sidr, ad2))
+    ==> ad1 = ad2.
+#endif
+
+#ifdef COOKIE_EVENTS
+COOKIE_EVENTS(Oresp_hello)
+#endif
+let Oresp_hello(HS_DECL_ARGS, C_in:channel, call:Atom) =
+  in(C_in, Cresp_hello(RespHello(sidr, =sidi, ecti, scti, biscuit, auth)));
+  in(C_in, mac2_key:key);
+  rh <- RespHello(sidr, sidi, ecti, scti, biscuit, auth);
+  #ifdef COOKIE_EVENTS
+    msg <- RH2b(rh);
+
+    COOKIE_PROCESS(Oresp_hello,
+  #endif
+    /* try */ let ic = (
+      ck_ini <- ck;
+      KEM_EV(event Oresp_hello_KemUse(sidi, sidr, call);)
+      RESPHELLO_CONSUME()
+      ck_ih <- ck;
+      INITCONF_PRODUCE()
+      CK_EV (event OskOresp_hello(ck_ini, ck_ih, osk); ) // TODO: Queries testing that there is no duplication
+      MTX_EV( event ICSent(rh, ic, psk, sski, spkr); )
+      SES_EV( event InitiatorSession(rh, osk); )
+      ic
+    /* success */ ) in (
+      icbits <- IC2b(ic);
+      mac <- create_mac(spkt, icbits);
+      mac2 <- create_mac2(mac2_key, mac_envelope2b(mac));
+      out(C_in, ic);
+      out(C_in, mac);
+      out(C_in, mac2)
+
+    /* fail */ ) else (
+  #if MESSAGE_TRANSMISSION_EVENTS
+      event RHRjct(rh, psk, sski, spkr)
+  #else
+      0
+  #endif
+    )
+#ifdef COOKIE_EVENTS
+  )
+#else
+  .
 #endif
-  ).
 
 // TODO: Restriction: Biscuit no invalidation
 
@@ -116,24 +164,33 @@ 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));
-#if RANDOMIZED_CALL_IDS
-  new call:Atom;
-#else
-  call <- Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih);
+KEM_EV(event Oinit_hello_KemUse(SessionId, SessionId, Atom).)
+
+#ifdef KEM_EVENTS
+restriction sidi:SessionId, sidr:SessionId, ad1:Atom, ad2:Atom;
+  event(Oinit_hello_KemUse(sidi, sidr, ad1)) && event(Oinit_hello_KemUse(sidi, sidr, ad2))
+    ==> ad1 = ad2.
 #endif
+
+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, mac2_key:key, C_out:channel, call:Atom) = 
   // TODO: This is ugly
   let InitHello(sidi, epki, sctr, pidiC, auth) = ih in
+
   SETUP_HANDSHAKE_STATE()
+
   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);
+
+  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);
+  // out(C_out, spkt);
+
   let rh = (
+    KEM_EV(event Oinit_hello_KemUse(sidi, sidr, call);)
     INITHELLO_CONSUME()
     ck_ini <- ck;
     RESPHELLO_PRODUCE()
@@ -141,7 +198,14 @@ let Oinit_hello() =
     MTX_EV( event RHSent(ih, rh, psk, sskr, spki); )
     rh
   /* success */ ) in (
-    out(C, rh)
+    rhbits <- RH2b(rh);
+    mac <- create_mac(spkt, rhbits);
+    
+    out(C_out, rh);
+    out(C_out, mac);
+    mac2 <- create_mac2(mac2_key, mac_envelope2b(mac));
+    out(C_out, mac2)
+
   /* fail */ ) else (
 #if MESSAGE_TRANSMISSION_EVENTS
     event IHRjct(ih, psk, sskr, spki)
@@ -150,6 +214,18 @@ let Oinit_hello() =
 #endif
   ).
 
+let Oinit_hello() = 
+  in(C, Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih));
+  in(C, mac2_key:key);
+
+  #if RANDOMIZED_CALL_IDS
+    new call:Atom;
+  #else
+    call <- Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih);
+  #endif
+
+  Oinit_hello_inner(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih, mac2_key, C, call).
+
 restriction sid:SessionId, ad1:Atom, ad2:Atom;
   event(ConsumeSidr(sid, ad1)) && event(ConsumeSidr(sid, ad2))
     ==> ad1 = ad2.
@@ -166,27 +242,55 @@ fun Cinitiator(SessionId, kem_sk_tmpl, key_tmpl, kem_pk_tmpl, seed_tmpl, seed_tm
 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
-  new call:Atom;
-#else
-  call <- Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr);
+KEM_EV(event Oinitiator_inner_KemUse(SessionId, SessionId, Atom).)
+
+#ifdef KEM_EVENTS
+restriction sidi:SessionId, sidr:SessionId, ad1:Atom, ad2:Atom;
+  event(Oinitiator_inner_KemUse(sidi, sidr, ad1)) && event(Oinitiator_inner_KemUse(sidi, sidr, ad2))
+    ==> ad1 = ad2.
 #endif
-  SETUP_HANDSHAKE_STATE()
-  RNG_KEM_PAIR(eski, epki, Seski) // IHI3
-  sidr <- sid0;
-  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, ih);
-  Oresp_hello(HS_PASS_ARGS).
+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, last_cookie:key, C_out:channel, call:Atom) =
+
+    SETUP_HANDSHAKE_STATE()
+    sidr <- sid0;
+
+    KEM_EV(event Oinitiator_inner_KemUse(sidi, sidr, call);)
+
+    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, ih);
+    ihbits <- IH2b(ih);
+    mac <- create_mac(spkt, ihbits);
+    out(C_out, mac);
+    mac2 <- create_mac2(last_cookie, mac_envelope2b(mac));
+    out(C_out, mac2);
+
+    Oresp_hello(HS_PASS_ARGS, C_out, call).
+
+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
+
+  in(C, last_cookie:key);
+  Oinitiator_inner(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr, last_cookie, C, call).
+
 
 restriction sid:SessionId, ad1:Atom, ad2:Atom;
   event(ConsumeSidi(sid, ad1)) && event(ConsumeSidi(sid, ad2))
@@ -207,21 +311,3 @@ let rosenpass_main() = 0
   | REP(RESPONDER_BOUND, Oinit_hello)
   | REP(RESPONDER_BOUND, Oinit_conf).
 
-nounif v:seed_prec;   attacker(prepare_seed(trusted_seed( v )))/6217[hypothesis].
-nounif v:seed;        attacker(prepare_seed( v ))/6216[hypothesis].
-nounif v:seed;        attacker(rng_kem_sk( v ))/6215[hypothesis].
-nounif v:seed;        attacker(rng_key( v ))/6214[hypothesis].
-nounif v:key_prec;    attacker(prepare_key(trusted_key( v )))/6213[hypothesis].
-nounif v:kem_sk_prec; attacker(prepare_kem_sk(trusted_kem_sk( v )))/6212[hypothesis].
-nounif v:key;         attacker(prepare_key( v ))/6211[hypothesis].
-nounif v:kem_sk;      attacker(prepare_kem_sk( v ))/6210[hypothesis].
-nounif Spk:kem_sk_tmpl;
-  attacker(Creveal_kem_pk(Spk))/6110[conclusion].
-nounif sid:SessionId, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Seski:seed_tmpl, Ssptr:seed_tmpl;
-  attacker(Cinitiator( *sid, *Ssskm, *Spsk, *Sspkt, *Seski, *Ssptr ))/6109[conclusion].
-nounif sid:SessionId, biscuit_no:Atom, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Septi:seed_tmpl, Sspti:seed_tmpl, ih:InitHello_t;
-  attacker(Cinit_hello( *sid, *biscuit_no, *Ssskm, *Spsk, *Sspkt, *Septi, *Sspti, *ih ))/6108[conclusion].
-nounif rh:RespHello_t;
-  attacker(Cresp_hello( *rh ))/6107[conclusion].
-nounif Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t;
-  attacker(Cinit_conf( *Ssskm, *Spsk, *Sspkt, *ic ))/6106[conclusion].
diff --git a/analysis/rosenpass/protocol.mpv b/analysis/rosenpass/protocol.mpv
index 658b05f..7bf2f1f 100644
--- a/analysis/rosenpass/protocol.mpv
+++ b/analysis/rosenpass/protocol.mpv
@@ -2,6 +2,26 @@
 #include "crypto/kem.mpv"
 #include "rosenpass/handshake_state.mpv"
 
+fun Envelope(
+  key,
+  bits
+): bits [data].
+
+type mac_envelope_t.
+fun mac_envelope(
+  key,
+  bits
+) : mac_envelope_t.
+
+fun mac_envelope2b(mac_envelope_t) : bits [typeConverter].
+
+letfun create_mac(pk:kem_pk, payload:bits) = mac_envelope(lprf2(MAC, kem_pk2b(pk), payload), payload).
+
+fun mac_envelope_pk_test(mac_envelope_t, kem_pk) : bool
+  reduc forall pk:kem_pk, b:bits;
+    mac_envelope_pk_test(mac_envelope(prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pk2b(pk)),
+        b), b), pk) = true.
+
 type InitHello_t.
 fun InitHello(
   SessionId, // sidi
@@ -11,6 +31,8 @@ fun InitHello(
   bits       // auth
 ) : InitHello_t [data].
 
+fun IH2b(InitHello_t) : bitstring [typeConverter].
+
 #define INITHELLO_PRODUCE()       \
   ck <- lprf1(CK_INIT, kem_pk2b(spkr)); /* IHI1 */ \
   /* not handled here */                /* IHI2 */ \
@@ -41,7 +63,9 @@ fun RespHello(
     bits       // auth
 ) : RespHello_t [data].
 
-#define RESPHELLO_PRODUCE()                   \
+fun RH2b(RespHello_t) : bitstring [typeConverter].
+
+#define RESPHELLO_PRODUCE()  \
   /* not handled here */           /* RHR1 */ \
   MIX2(sid2b(sidr), sid2b(sidi))   /* RHR3 */ \
   ENCAPS_AND_MIX(ecti, epki, epti) /* RHR4 */ \
@@ -67,13 +91,14 @@ fun InitConf(
     bits       // auth
 ) : InitConf_t [data].
 
+fun IC2b(InitConf_t) : bitstring [typeConverter].
+
 #define INITCONF_PRODUCE()                  \
   MIX2(sid2b(sidi), sid2b(sidr)) /* ICI3 */ \
   ENCRYPT_AND_MIX(auth, empty)   /* ICI4 */ \
   ic <- InitConf(sidi, sidr, biscuit, auth);
 
 #define INITCONF_CONSUME()                        \
-  let InitConf(sidi, sidr, biscuit, auth) = ic in \
   LOAD_BISCUIT(biscuit_no, biscuit)   /* ICR1 */    \
   ENCRYPT_AND_MIX(rh_auth, empty)     /* ICIR */    \
   ck_rh <- ck;                        /* ---- */ /* TODO: Move into oracles.mpv */ \