#define RESPONDER_TEST 1

#include "rosenpass/03_identity_hiding.mpv"

// select k:kem_pk,ih: InitHello_t;         attacker(prf(prf(prf(prf(key0, PROTOCOL), MAC), kem_pk2b(k) ), IH2b(ih))) phase 1/6300[hypothesis].

// select epki:kem_pk, sctr:bits, pidiC:bits, auth:bits, epki2:kem_pk, sctr2:bits, pidiC2:bits, auth2:bits;
// 	mess(D, prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pk2b(kem_pub(trusted_kem_sk(responder1)))),
// 			IH2b(InitHello(secure_sidi, *epki, *sctr, *pidiC, *auth)))
// 		) [hypothesis, conclusion].

// select epki:kem_pk, sctr:bits, pidiC:bits, auth:bits, epki2:kem_pk, sctr2:bits, pidiC2:bits, auth2:bits;
// attacker(choice[prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pk2b(kem_pub(trusted_kem_sk(responder1)))),
// 		IH2b(InitHello(secure_sidi, *epki, *sctr, *pidiC, *auth))),

// 		prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pk2b(kem_pub(trusted_kem_sk(responder2)))),
// 				IH2b(InitHello(secure_sidi, *epki2, *sctr2, *pidiC2, *auth2)))]
// 	) [hypothesis, conclusion].

// select 
// attacker(prf(prf(key0,PROTOCOL),MAC)) [hypothesis, conclusion].

// select 
// attacker(prf(key0,PROTOCOL)) [conclusion].

// select  
// attacker(key0) [conclusion].

// select  
// attacker(PROTOCOL) [conclusion].

// select 
// attacker(kem_pub(trusted_kem_sk(responder1))) /9999 [hypothesis, conclusion].

// select 
// attacker(kem_pub(trusted_kem_sk(responder2))) /9999 [hypothesis, conclusion].

// nounif ih:InitHello_t;
// 	attacker(ih) / 9999 [hypothesis].

// nounif rh:RespHello_t;
// 	attacker(rh) / 9999 [hypothesis].

// nounif ic:InitConf_t;
// 	attacker(ic) / 9999 [hypothesis].

// nounif k:key;
// attacker(ck_hs_enc( *k )) [hypothesis, conclusion].

// nounif k:key;
// attacker(ck_hs_enc( *k )) phase 1   [hypothesis, conclusion].

// nounif k:key, b:bits;
// attacker(ck_mix( *k , *b ))   [hypothesis, conclusion].

// nounif k:key, b:bits;
// attacker(ck_mix( *k , *b ))phase 1   [hypothesis, conclusion].

// // select k:kem_pk, epki2:kem_pk, sctr2:bits, pidiC2:bits, auth2:bits, epki:kem_pk, sctr:bits, pidiC:bits, auth:bits;
// // attacker(choice[Envelope(prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pub(trusted_kem_sk(responder1))),
// // 	InitHello(secure_sidi, *epki2, *sctr2, *pidiC2, *auth2)
// // 	), InitHello(secure_sidi, *epki2, *sctr2, *pidiC2, *auth2))
// // 	Envelope(prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pub(trusted_kem_sk(responder2))),
// // 		InitHello(secure_sidi, *epki, *sctr, *pidiC, *auth)),
// // 		InitHello(secure_sidi, *epki, *sctr, *pidiC, *auth))
// // 	]) / 9999[hypothesis, conclusion].

// nounif k:key, b1:bits, b2:bits;
// 	attacker(xaead_enc( *k, *b1, *b2)) / 9999[hypothesis,conclusion].

// nounif pk:kem_pk, k:key; 
// 	attacker(kem_enc( *pk , *k )) / 9999[hypothesis,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 ))/9999[hypothesis, conclusion].
// nounif Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t;
//   attacker(Cinit_conf( *Ssskm, *Spsk, *Sspkt, *ic ))/9999[hypothesis, 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 )) /9999 [hypothesis, 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;
//   mess(C, Cinit_hello( *sid, *biscuit_no, *Ssskm, *Spsk, *Sspkt, *Septi, *Sspti, *ih ))/9999[hypothesis, conclusion].
// nounif Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t;
//   mess(C, Cinit_conf( *Ssskm, *Spsk, *Sspkt, *ic ))/9999[hypothesis, conclusion].
// nounif sid:SessionId, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Seski:seed_tmpl, Ssptr:seed_tmpl;
//   mess(C, Cinitiator( *sid, *Ssskm, *Spsk, *Sspkt, *Seski, *Ssptr )) /9999 [hypothesis, conclusion].
// nounif rh:RespHello_t;
//   attacker(Cresp_hello( *rh ))[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].