mirror of
https://github.com/rosenpass/rosenpass.git
synced 2026-01-06 18:14:51 -08:00
202 lines
12 KiB
Plaintext
202 lines
12 KiB
Plaintext
#define CHAINING_KEY_EVENTS 1
|
|
#define MESSAGE_TRANSMISSION_EVENTS 0
|
|
#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"
|
|
lemma ini:key, ih:key, rh:key, any_psk:key, any_sski:kem_sk, any_spkr:kem_pk, any_sptr:key;
|
|
event(OskOresp_hello(ini, ih, rh))
|
|
==> event(OskOinitiator(ini, any_psk, any_sski, any_spkr, any_sptr)).
|
|
|
|
@lemma "state coherence, responder: Responder accepting an InitConf message implies they also generated the associated RespHello message"
|
|
lemma ini:key, rh:key, ic:key, any_psk:key, any_sskr:kem_sk, any_spki:kem_pk, any_epki:kem_pk, any_epti:key, any_spti:key;
|
|
event(OskOinit_conf(rh, ic))
|
|
==> event(OskOinit_hello(ini, rh, any_psk, any_sskr, any_spki, any_epki, any_epti, any_spti)).
|
|
|
|
@reachable "functionality: Key exchange can be achieved"
|
|
query ini:key, ih1:key, ih2:key, rh:key;
|
|
event(OskOresp_hello(ini, ih1, rh)) && event(OskOinit_conf(ih2, rh)).
|
|
|
|
@lemma "secrecy: Adv can not learn shared secret key"
|
|
lemma kp:key_prec, skp:kem_sk_prec;
|
|
attacker(trusted_key(kp)).
|
|
|
|
@lemma "secrecy: There is no way for an attacker to learn a trusted kem secret key"
|
|
lemma skp:kem_sk_prec;
|
|
attacker(trusted_kem_sk(skp)).
|
|
|
|
@lemma "secrecy: The adversary can learn a trusted kem pk only by using the reveal oracle"
|
|
lemma skp:kem_sk_prec;
|
|
attacker(kem_pub(trusted_kem_sk(skp)))
|
|
==> event(RevealPk(kem_pub(trusted_kem_sk(skp)))).
|
|
|
|
@reachable "non-secrecy: The attacker can learn the value of a shared key" // (by using a malicious/non-trusted key)
|
|
query k:key;
|
|
attacker(prepare_key(k)) && attacker(k).
|
|
|
|
@reachable "non-secrecy: The attacker can learn the value of a kem secret key" // (by using a malicious/non-trusted key)
|
|
query sk:kem_sk;
|
|
attacker(prepare_kem_sk(sk)) && attacker(sk).
|
|
|
|
// Demonstrates how to check that a key is malicious in a lemma
|
|
|
|
@lemma "secrecy: Attacker knowledge of a shared key implies the key is not trusted"
|
|
lemma k:key, kp:key_prec;
|
|
attacker(prepare_key(k)) && attacker(k) ==> k <> trusted_key(kp).
|
|
|
|
@lemma "secrecy: Attacker knowledge of a kem sk implies the key is not trusted"
|
|
lemma k:kem_sk, kp:kem_sk_prec;
|
|
attacker(prepare_kem_sk(k)) && attacker(k) ==> k <> trusted_kem_sk(kp).
|
|
|
|
// Actual in-protocol secrecy queries
|
|
|
|
@lemma "symmetric secrecy: Secure PSK is sufficient for ck secrecy after trusted InitHello transmission from initiator perspective"
|
|
lemma ck:key, Ppsk:key_prec, any_sski:kem_sk, any_spkr:kem_pk, any_sptr:key;
|
|
let secure_psk = trusted_key(Ppsk) in
|
|
event(OskOinitiator(ck, secure_psk, any_sski, any_spkr, any_sptr)) && attacker(ck).
|
|
|
|
@lemma "asymmetric secrecy: Secure SSKR is sufficient for ck secrecy after trusted InitHello transmission from initiator perspective"
|
|
lemma ck:key, any_psk:key, any_sski:kem_sk, Psskr:kem_sk_prec, Psptr:seed_prec;
|
|
let secure_spkr = kem_pub(trusted_kem_sk(Psskr)) in
|
|
let secure_sptr = rng_key(trusted_seed(Psptr)) in // to account for a captured RNG
|
|
event(OskOinitiator(ck, any_psk, any_sski, secure_spkr, secure_sptr)) && attacker(ck).
|
|
|
|
@lemma "symmetric secrecy: Secure PSK is sufficient for ck secrecy after trusted RespHello transmission from responder perspective"
|
|
lemma ck_ini:key, ck:key, Ppsk:key_prec, any_sskr:kem_sk, any_spki:kem_pk, any_epki:kem_pk, any_epti:key, any_spti:key;
|
|
let secure_psk = trusted_key(Ppsk) in
|
|
attacker(ck)
|
|
&& event(OskOinit_hello(ck_ini, ck, secure_psk, any_sskr, any_spki, any_epki, any_epti, any_spti)).
|
|
|
|
@lemma "asymmetric secrecy: Secure SSKI is sufficient for ck secrecy after trusted InitHello transmission from responder perspective"
|
|
lemma ck_ini:key, ck:key, any_psk:key, any_sskr:kem_sk, PSsski:kem_sk_prec, any_epki:kem_pk, any_epti:key, PSspti:seed_prec;
|
|
let secure_spki = kem_pub(trusted_kem_sk(PSsski)) in
|
|
let secure_spti = rng_key(trusted_seed(PSspti)) in /* Accounting for captured RNG */
|
|
attacker(ck)
|
|
&& event(OskOinit_hello(ck_ini, ck, any_psk, any_sskr, secure_spki, any_epki, any_epti, secure_spti)).
|
|
|
|
@lemma "forward, asymmetric secrecy: Secure ESKI is sufficient for ck secrecy after trusted InitHello transmission from responder perspective"
|
|
lemma ck_ini:key, ck:key, any_psk:key, any_sskr:kem_sk, any_spki:kem_pk, Peski:kem_sk_prec, Pepti:seed_prec, any_spti:key;
|
|
let secure_epki = kem_pub(trusted_kem_sk(Peski)) in
|
|
let secure_epti = rng_key(trusted_seed(Pepti)) in /* Accounting for captured RNG */
|
|
attacker(ck)
|
|
&& event(OskOinit_hello(ck_ini, ck, any_psk, any_sskr, any_spki, secure_epki, secure_epti, any_spti)).
|
|
|
|
// TODO: Do not mention OskOinitiator
|
|
@lemma "symmetric secrecy: Secure PSK is sufficient for ck secrecy after trusted InitConf transmission from initiator perspective"
|
|
// (Follows directly from the same property on Oinitiator)
|
|
lemma ini:key, ih:key, rh:key, Ppsk:key_prec, any_sski:kem_sk, any_spkr:kem_pk, any_sptr:key;
|
|
let secure_psk = trusted_key(Ppsk) in
|
|
attacker(rh)
|
|
&& event(OskOinitiator(ini, secure_psk, any_sski, any_spkr, any_sptr))
|
|
&& event(OskOresp_hello(ini, ih, rh)).
|
|
|
|
// TODO: Do not mention OskOinitiator
|
|
@lemma "asymmetric secrecy: Secure SSKR is sufficient for ck secrecy after trusted RespHello transmission from initiator perspective"
|
|
// (Follows directly from the same property on Oinitiator)
|
|
lemma ini:key, ih:key, rh:key, any_psk:key, any_sski:kem_sk, Psskr:kem_sk_prec, Psptr:seed_prec;
|
|
let secure_spkr = kem_pub(trusted_kem_sk(Psskr)) in
|
|
let secure_sptr = rng_key(trusted_seed(Psptr)) in // to account for a captured RNG
|
|
attacker(rh)
|
|
&& event(OskOinitiator(ini, any_psk, any_sski, secure_spkr, secure_sptr))
|
|
&& event(OskOresp_hello(ini, ih, rh)).
|
|
|
|
@lemma "passive asymmetric secrecy: Secure SSKI is sufficient for ck secrecy after trusted RespHello transmission from initiator perspective"
|
|
// (Follows directly from the same property on Oinitiator)
|
|
lemma ini:key, ih:key, rh:key, any_psk:key, any_psk2:key, Psski:kem_sk_prec,
|
|
any_sskr:kem_sk, any_spki:kem_pk, any_epki:kem_pk, any_spkr:kem_pk,
|
|
any_sptr:key, any_epti:key, Pspti:seed_prec;
|
|
let secure_sski = trusted_kem_sk(Psski) in
|
|
let secure_spti = rng_key(trusted_seed(Pspti)) in // to account for a captured RNG
|
|
// That spki must be must bee derived from secure_sski follows from the same chaining key
|
|
// being put out, since spki is mixed into the chaining key. Specifying it speeds up the
|
|
// validation though. TODO: Turn this into a lemma?
|
|
// TODO: Do we event need SPKI in the initiator event?
|
|
#if SIMPLE_MODEL
|
|
let ih_spki = kem_pub(secure_sski) in
|
|
#else
|
|
let ih_spki = any_spki in
|
|
#endif
|
|
attacker(rh)
|
|
&& event(OskOinitiator(ini, any_psk, secure_sski, any_spkr, any_sptr))
|
|
&& event(OskOinit_hello(ini, ih, any_psk2, any_sskr, ih_spki, any_epki, any_epti, secure_spti))
|
|
&& event(OskOresp_hello(ini, ih, rh)).
|
|
|
|
@lemma "forward asymmetric secrecy: Secure SSKI is sufficient for ck secrecy after trusted RespHello transmission from initiator perspective"
|
|
// (Follows directly from the same property on Oinitiator)
|
|
lemma ini:key, ih:key, rh:key, any_psk:key, any_psk2:key, Peski:kem_sk_prec,
|
|
any_sskr:kem_sk, any_sski:kem_sk, any_spki:kem_pk, any_epki:kem_pk, any_spkr:kem_pk,
|
|
any_sptr:key, Pepti:seed_prec, any_spti:key;
|
|
let secure_epki = kem_pub(trusted_kem_sk(Peski)) in
|
|
let secure_epti = rng_key(trusted_seed(Pepti)) in // to account for a captured RNG
|
|
attacker(rh)
|
|
&& event(OskOinitiator(ini, any_psk, any_sski, any_spkr, any_sptr))
|
|
&& event(OskOinit_hello(ini, ih, any_psk2, any_sskr, any_spki, secure_epki, secure_epti, any_spti))
|
|
&& event(OskOresp_hello(ini, ih, rh)).
|
|
|
|
// TODO: Add continuity queries: InitConf acceptance implies that there was a InitHello acceptance and so on
|
|
|
|
@lemma "symmetric secrecy: Secure PSK is sufficient for ck secrecy after trusted InitConf acceptance from responder perspective"
|
|
lemma ini:key, rh:key, ic:key, Ppsk:key_prec, any_sskr:kem_sk, any_spki:kem_pk, any_epki:kem_pk, any_epti:key, any_spti:key;
|
|
let secure_psk = trusted_key(Ppsk) in
|
|
attacker(ic)
|
|
&& event(OskOinit_hello(ini, rh, secure_psk, any_sskr, any_spki, any_epki, any_epti, any_spti))
|
|
&& event(OskOinit_conf(rh, ic)).
|
|
|
|
@lemma "asymmetric secrecy: Secure SSKI is sufficient for ck secrecy after InitConf acceptance from responder perspective"
|
|
lemma ini:key, rh:key, ic:key, any_psk:key, any_sskr:kem_sk, PSsski:kem_sk_prec, any_epki:kem_pk, any_epti:key, PSspti:seed_prec;
|
|
let secure_spki = kem_pub(trusted_kem_sk(PSsski)) in
|
|
let secure_spti = rng_key(trusted_seed(PSspti)) in /* Accounting for captured RNG */
|
|
attacker(ic)
|
|
&& event(OskOinit_hello(ini, rh, any_psk, any_sskr, secure_spki, any_epki, any_epti, secure_spti))
|
|
&& event(OskOinit_conf(rh, ic)).
|
|
|
|
@lemma "forward, asymmetric secrecy: Secure ESKI is sufficient for ck secrecy after InitConf acceptance from responder perspective"
|
|
lemma ini:key, rh:key, ic:key, any_psk:key, any_sskr:kem_sk, any_spki:kem_pk, Peski:kem_sk_prec, Pepti:seed_prec, any_spti:key;
|
|
let secure_epki = kem_pub(trusted_kem_sk(Peski)) in
|
|
let secure_epti = rng_key(trusted_seed(Pepti)) in /* Accounting for captured RNG */
|
|
attacker(ic)
|
|
&& event(OskOinit_hello(ini, rh, any_psk, any_sskr, any_spki, secure_epki, secure_epti, any_spti))
|
|
&& event(OskOinit_conf(rh, ic)).
|
|
|
|
@lemma "passive asymmetric secrecy: Secure SSKR is sufficient for ck secrecy after InitConf acceptance from responder perspective"
|
|
lemma ini:key, rh:key, ic:key, any_psk1:key, any_psk2:key, any_sski:kem_sk, any_sskr:kem_sk,
|
|
any_spki:kem_pk, any_epki:kem_pk, Psskr:kem_sk_prec, Psptr:seed_prec, any_epti:key, any_spti:key;
|
|
let secure_spkr = kem_pub(trusted_kem_sk(Psskr)) in
|
|
let secure_sptr = rng_key(trusted_seed(Psptr)) in /* Accounting for captured RNG */
|
|
attacker(ic)
|
|
&& event(OskOinitiator(ini, any_psk1, any_sski, secure_spkr, secure_sptr))
|
|
&& event(OskOinit_hello(ini, rh, any_psk2, any_sskr, any_spki, any_epki, any_epti, any_spti))
|
|
&& event(OskOinit_conf(rh, ic)).
|
|
|
|
// TODO: Anonymity queries (under which circumstances can adv identify the participants?)
|
|
// TODO: Model CPAKEM, etc
|