#define INITIATOR_TEST 1

#include "rosenpass/03_identity_hiding.mpv"

// nounif a:Atom, s:seed, a2:Atom;
// 	ConsumeSeed(a, s, a2) / 6300[conclusion].

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].