chore: DOS protection and identity hiding symbolic models

Starting points for actually integrating these models in a comprehensive, reliable way.
2025-12-12 07:40:30 -08:00 · 2024-06-07 21:04:14 +02:00
parent 5f8b00d045
commit 64c2cf60fe
5 changed files with 241 additions and 77 deletions
--- 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"
--- 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)))
--- 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. *)
--- 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].
--- 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 */ \