mirror of
https://github.com/rosenpass/rosenpass.git
synced 2025-12-30 14:42:29 -08:00
70 lines
3.5 KiB
Plaintext
70 lines
3.5 KiB
Plaintext
#define CHAINING_KEY_EVENTS 0
|
|
#define MESSAGE_TRANSMISSION_EVENTS 1
|
|
#define SESSION_START_EVENTS 1
|
|
|
|
#include "config.mpv"
|
|
#include "prelude/basic.mpv"
|
|
#include "crypto/key.mpv"
|
|
#include "crypto/kem.mpv"
|
|
#include "rosenpass/oracles.mpv"
|
|
|
|
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)))
|
|
&& event(IHSent(ih, psk, sski, kem_pub(sskr))).
|
|
|
|
@lemma "non-interruptability: Adv cannot prevent a genuine RespHello message from being accepted"
|
|
lemma ih:InitHello_t, rh:RespHello_t, psk:key, sski:kem_sk, sskr:kem_sk;
|
|
event(RHRjct(rh, psk, sski, kem_pub(sskr)))
|
|
&& event(IHSent(ih, psk, sski, kem_pub(sskr)))
|
|
&& event(RHSent(ih, rh, psk, sskr, kem_pub(sski))).
|
|
|
|
@lemma "non-interruptability: Adv cannot prevent a genuine InitConf message from being accepted"
|
|
lemma ih:InitHello_t, rh:RespHello_t, ic:InitConf_t, psk:key, sski:kem_sk, sskr:kem_sk;
|
|
event(ICRjct(ic, psk, sskr, kem_pub(sski)))
|
|
&& event(IHSent(ih, psk, sski, kem_pub(sskr)))
|
|
&& event(RHSent(ih, rh, psk, sskr, kem_pub(sski)))
|
|
&& event(ICSent(rh, ic, psk, sski, kem_pub(sskr))).
|
|
|
|
@query "non-interruptability: Adv cannot use the same RespHello package to start a session twice"
|
|
query rh:RespHello_t, ck1:key, ck2:key, t1:time, t2:time;
|
|
event(InitiatorSession(rh, ck1))@t1 && event(InitiatorSession(rh, ck1))@t2
|
|
==> t1 = t2.
|
|
|
|
@query "non-interruptability: Adv cannot use the same InitConf package to start a session twice"
|
|
query ic:InitConf_t, ck1:key, ck2:key, t1:time, t2:time;
|
|
event(ResponderSession(ic, ck1))@t1 && event(ResponderSession(ic, ck1))@t2
|
|
==> t1 = t2.
|
|
|
|
@query "non-interruptability: Adv cannot start a responder session with the same key twice"
|
|
query rh1:RespHello_t, rh2:RespHello_t, ck:key, t1:time, t2:time;
|
|
event(InitiatorSession(rh1, ck))@t1 && event(InitiatorSession(rh2, ck))@t2
|
|
==> t1 = t2.
|
|
|
|
@query "non-interruptability: Adv cannot start a responder session with the same key twice"
|
|
query ic1:InitConf_t, ic2:InitConf_t, ck:key, t1:time, t2:time;
|
|
event(ResponderSession(ic1, ck))@t1 && event(ResponderSession(ic2, ck))@t2
|
|
==> t1 = t2.
|