diff --git a/analysis/03_identity_hiding_initiator.entry.mpv b/analysis/03_identity_hiding_initiator.entry.mpv deleted file mode 100644 index 2d63043..0000000 --- a/analysis/03_identity_hiding_initiator.entry.mpv +++ /dev/null @@ -1,25 +0,0 @@ -#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]. diff --git a/analysis/03_identity_hiding_responder.entry.mpv b/analysis/03_identity_hiding_responder.entry.mpv deleted file mode 100644 index 5908a72..0000000 --- a/analysis/03_identity_hiding_responder.entry.mpv +++ /dev/null @@ -1,96 +0,0 @@ -#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]. diff --git a/analysis/03_identity_hiding_test.entry.mpv b/analysis/03_identity_hiding_test.entry.mpv deleted file mode 100644 index 1c7afc5..0000000 --- a/analysis/03_identity_hiding_test.entry.mpv +++ /dev/null @@ -1,29 +0,0 @@ -#define INITIATOR_TEST 1 -#define CUSTOM_MAIN 1 - -#include "rosenpass/03_identity_hiding.mpv" - -let Oinitiator_bad_actor_inner(sk_tmp:kem_sk_prec) = - - in(C, Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr)); - - #if RANDOMIZED_CALL_IDS - new call:Atom; - #else - call <- Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr); - #endif - - in(C, last_cookie:key); - tmpl <- make_trusted_kem_sk(sk_tmp); - out(C, setup_kem_sk(tmpl)); - Oinitiator_inner(sidi, Ssskm, Spsk, tmpl, Seski, Ssptr, last_cookie, C, call). - -let Oinitiator_bad_actor() = - Oinitiator_bad_actor_inner(responder1) | Oinitiator_bad_actor_inner(responder2) | Oinitiator_bad_actor_inner(initiator1) | Oinitiator_bad_actor_inner(initiator2). - - -let identity_hiding_main2() = - 0 | Oinitiator_bad_actor() | rosenpass_main2() | participants_communication() | phase 1; secretCommunication(). - - -let main = identity_hiding_main2. diff --git a/analysis/04_dos_protection.entry.mpv b/analysis/04_dos_protection.entry.mpv deleted file mode 100644 index e436577..0000000 --- a/analysis/04_dos_protection.entry.mpv +++ /dev/null @@ -1,136 +0,0 @@ -#define CHAINING_KEY_EVENTS 1 -#define MESSAGE_TRANSMISSION_EVENTS 0 -#define SESSION_START_EVENTS 0 -#define RANDOMIZED_CALL_IDS 0 -#define COOKIE_EVENTS 1 -#define KEM_EVENTS 1 - -#include "config.mpv" -#include "prelude/basic.mpv" -#include "crypto/key.mpv" -#include "crypto/kem.mpv" -#include "rosenpass/handshake_state.mpv" - -/* The cookie data structure is implemented based on the WireGuard protocol. - * The ip and port is based purely on the public key and the implementation of the private cookie key is intended to mirror the biscuit key. - * The code tests the response to a possible DOS attack by setting up alternative branches for the protocol - * processes: Oinit_conf, Oinit_hello and resp_hello to simulate what happens when the responder or initiator is overloaded. - * When under heavy load a valid cookie is required. When such a cookie is not present a cookie message is sent as a response. - * Queries then test to make sure that expensive KEM operations are only conducted after a cookie has been successfully validated. - */ - -type CookieMsg_t. -fun CookieMsg( - SessionId, // sender - bits, // nonce - bits // cookie -) : CookieMsg_t [data]. - -#define COOKIE_EVENTS(eventLbl) \ - COOKIE_EV(event MCAT(eventLbl, _UnderLoadEV) (SessionId, SessionId, Atom).) \ - COOKIE_EV(event MCAT(eventLbl, _CookieValidated) (SessionId, SessionId, Atom).) \ - COOKIE_EV(event MCAT(eventLbl, _CookieSent) (SessionId, SessionId, Atom, CookieMsg_t).) - -fun cookie_key(kem_sk) : key [private]. -fun ip_and_port(kem_pk):bits. -letfun create_mac2_key(sskm:kem_sk, spkt:kem_pk) = prf(cookie_key(sskm), ip_and_port(spkt)). -letfun create_cookie(sskm:kem_sk, spkm:kem_pk, spkt:kem_pk, nonce:bits, msg:bits) = xaead_enc(lprf2(COOKIE, kem_pk2b(spkm), nonce), - k2b(create_mac2_key(sskm, spkm)), msg). - -#define COOKIE_PROCESS(eventLbl, innerFunc) \ - new nonce:bits; \ - in(C, Ccookie(mac1, mac2)); \ - COOKIE_EV(event MCAT(eventLbl, _UnderLoadEV) (sidi, sidr, call);) \ - msgB <- Envelope(mac1, msg); \ - mac2_key <- create_mac2_key(sskm, spkt); \ - if k2b(create_mac2(mac2_key, msgB)) = mac2 then \ - COOKIE_EV(event MCAT(eventLbl, _CookieValidated) (sidi, sidr, call);) \ - innerFunc \ - else \ - cookie <- create_cookie(sskm, spkm, spkt, nonce, msg); \ - cookie_msg <- CookieMsg(sidi, nonce, cookie); \ - COOKIE_EV(event MCAT(eventLbl, _CookieSent) (sidi, sidr, call, cookie_msg);) \ - out(C, cookie_msg). \ - -#include "rosenpass/oracles.mpv" - -#include "rosenpass/responder.macro" -COOKIE_EVENTS(Oinit_conf) -let Oinit_conf_underLoad() = - in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic)); - in(C, last_cookie:bits); - - msg <- IC2b(ic); - let InitConf(sidi, sidr, biscuit, auth) = ic in - - new call:Atom; - - SETUP_HANDSHAKE_STATE() - - COOKIE_PROCESS(Oinit_conf, Oinit_conf_inner(Ssskm, Spsk, Sspkt, ic, call)) - -#include "rosenpass/responder.macro" -COOKIE_EVENTS(Oinit_hello) -let Oinit_hello_underLoad() = - - in(C, Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih)); - in(C, Oinit_hello_last_cookie:key); - new call:Atom; - - msg <- IH2b(ih); - let InitHello(sidi, epki, sctr, pidic, auth) = ih in - SETUP_HANDSHAKE_STATE() - - COOKIE_PROCESS(Oinit_hello, Oinit_hello_inner(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih, Oinit_hello_last_cookie, C, call)) - -let rosenpass_dos_main() = 0 - | !Oreveal_kem_pk - | REP(INITIATOR_BOUND, Oinitiator) - | REP(RESPONDER_BOUND, Oinit_hello) - | REP(RESPONDER_BOUND, Oinit_conf) - | REP(RESPONDER_BOUND, Oinit_hello_underLoad) - | REP(RESPONDER_BOUND, Oinit_conf_underLoad). - -let main = rosenpass_dos_main. - -select cookie:CookieMsg_t; attacker(cookie)/6220[hypothesis]. -nounif v:key; attacker(prepare_key( v ))/6217[hypothesis]. -nounif v:seed; attacker(prepare_seed( v ))/6216[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: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]. - -@reachable "DOS protection: cookie sent" -query sidi:SessionId, sidr:SessionId, call:Atom, cookieMsg:CookieMsg_t; - event (Oinit_hello_CookieSent(sidi, sidr, call, cookieMsg)). - -@lemma "DOS protection: Oinit_hello kem use when under load implies validated cookie" -lemma sidi:SessionId, sidr:SessionId, call:Atom; -event(Oinit_hello_UnderLoadEV(sidi, sidr, call)) - && event(Oinit_hello_KemUse(sidi, sidr, call)) - ==> event(Oinit_hello_CookieValidated(sidi, sidr, call)). - -@lemma "DOS protection: Oinit_conf kem use when under load implies validated cookie" -lemma sidi:SessionId, sidr:SessionId, call:Atom; -event(Oinit_conf_UnderLoadEV(sidi, sidr, call)) - && event(Oinit_conf_KemUse(sidi, sidr, call)) - ==> event(Oinit_conf_CookieValidated(sidi, sidr, call)). - -@lemma "DOS protection: Oresp_hello kem use when under load implies validated cookie" -lemma sidi:SessionId, sidr:SessionId, call:Atom; -event(Oresp_hello_UnderLoadEV(sidi, sidr, call)) - && event(Oresp_hello_KemUse(sidi, sidr, call)) - ==> event(Oresp_hello_CookieValidated(sidi, sidr, call)). -