mirror of
https://github.com/rosenpass/rosenpass.git
synced 2025-12-12 07:40:30 -08:00
8c469af6b1
seperate files for responder and initiator tests test file that shows other participants leaking info has an effect general code clean up performance improvement: initiator and responder tests now run in ~10s
97 lines
4.6 KiB
Plaintext
97 lines
4.6 KiB
Plaintext
#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].
|