chore: DOS protection and identity hiding symbolic models

Starting points for actually integrating these models in a
comprehensive, reliable way.

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"

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)))

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. *)

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).
+KEM_EV(event Oinit_conf_KemUse(SessionId, SessionId, Atom).)
-let Oinit_conf() = 
+#ifdef KEM_EVENTS
-  in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic));
+  restriction sidi:SessionId, sidr:SessionId, ad1:Atom, ad2:Atom;
-#if RANDOMIZED_CALL_IDS
+    event(Oinit_conf_KemUse(sidi, sidr, ad1)) && event(Oinit_conf_KemUse(sidi, sidr, ad2))
-  new call:Atom;
+      ==> ad1 = ad2.
-#else
-  call <- Cinit_conf(Ssskm, Spsk, Sspkt, ic);
 #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)));
+KEM_EV(event Oresp_hello_KemUse(SessionId, SessionId, Atom).)
-  rh <- RespHello(sidr, sidi, ecti, scti, biscuit, auth);
+#ifdef KEM_EVENTS
-  /* try */ let ic = (
+restriction sidi:SessionId, sidr:SessionId, ad1:Atom, ad2:Atom;
-    ck_ini <- ck;
+  event(Oresp_hello_KemUse(sidi, sidr, ad1)) && event(Oresp_hello_KemUse(sidi, sidr, ad2))
-    RESPHELLO_CONSUME()
+    ==> ad1 = ad2.
-    ck_ih <- ck;
+#endif
-    INITCONF_PRODUCE()
+
-    CK_EV (event OskOresp_hello(ck_ini, ck_ih, osk); ) // TODO: Queries testing that there is no duplication
+#ifdef COOKIE_EVENTS
-    MTX_EV( event ICSent(rh, ic, psk, sski, spkr); )
+COOKIE_EVENTS(Oresp_hello)
-    SES_EV( event InitiatorSession(rh, osk); )
+#endif
-    ic
+let Oresp_hello(HS_DECL_ARGS, C_in:channel, call:Atom) =
-  /* success */ ) in (
+  in(C_in, Cresp_hello(RespHello(sidr, =sidi, ecti, scti, biscuit, auth)));
-    out(C, ic)
+  in(C_in, mac2_key:key);
-  /* fail */ ) else (
+  rh <- RespHello(sidr, sidi, ecti, scti, biscuit, auth);
-#if MESSAGE_TRANSMISSION_EVENTS
+  #ifdef COOKIE_EVENTS
-    event RHRjct(rh, psk, sski, spkr)
+    msg <- RH2b(rh);
-#else
+
-    0
+    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() = 
+KEM_EV(event Oinit_hello_KemUse(SessionId, SessionId, Atom).)
-  in(C, Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih));
+
-#if RANDOMIZED_CALL_IDS
+#ifdef KEM_EVENTS
-  new call:Atom;
+restriction sidi:SessionId, sidr:SessionId, ad1:Atom, ad2:Atom;
-#else
+  event(Oinit_hello_KemUse(sidi, sidr, ad1)) && event(Oinit_hello_KemUse(sidi, sidr, ad2))
-  call <- Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih);
+    ==> 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).
+KEM_EV(event Oinitiator_inner_KemUse(SessionId, SessionId, Atom).)
-let Oinitiator() =
+
-  in(C, Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr));
+#ifdef KEM_EVENTS
-#if RANDOMIZED_CALL_IDS
+restriction sidi:SessionId, sidr:SessionId, ad1:Atom, ad2:Atom;
-  new call:Atom;
+  event(Oinitiator_inner_KemUse(sidi, sidr, ad1)) && event(Oinitiator_inner_KemUse(sidi, sidr, ad2))
-#else
+    ==> ad1 = ad2.
-  call <- Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr);
 #endif
-  SETUP_HANDSHAKE_STATE()
+event ConsumeSidi(SessionId, Atom).
-  RNG_KEM_PAIR(eski, epki, Seski) // IHI3
+
-  sidr <- sid0;
+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) =
-  sptr <- rng_key(setup_seed(Ssptr)); // IHI5
+
-  event ConsumeSidi(sidi, call);
+    SETUP_HANDSHAKE_STATE()
-  event ConsumeSeed(Sptr, setup_seed(Ssptr), call);
+    sidr <- sid0;
-  event ConsumeSeed(Eski, setup_seed(Seski), call);
+
-  INITHELLO_PRODUCE()
+    KEM_EV(event Oinitiator_inner_KemUse(sidi, sidr, call);)
-  CK_EV( event OskOinitiator_ck(ck); ) 
+
-  CK_EV( event OskOinitiator(ck, psk, sski, spkr, sptr); )
+    RNG_KEM_PAIR(eski, epki, Seski) // IHI3
-  MTX_EV( event IHSent(ih, psk, sski, spkr); )
+    sptr <- rng_key(setup_seed(Ssptr)); // IHI5
-  out(C, ih);
+    event ConsumeSidi(sidi, call);
-  Oresp_hello(HS_PASS_ARGS).
+    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].

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 */ \