From f39a43a8219a2a3edfb80384717c65a529a6bf9a Mon Sep 17 00:00:00 2001 From: Karolin Varner Date: Wed, 13 Aug 2025 17:59:27 +0200 Subject: [PATCH] fix(proverif): Remove broken protocol analysis code The identity hiding and DOS protection models where never actually functional. Here we just remove them so the CI and manual runs of analysis.sh stop giving spurious errors. --- .../03_identity_hiding_initiator.entry.mpv | 25 ---- .../03_identity_hiding_responder.entry.mpv | 96 ------------- analysis/03_identity_hiding_test.entry.mpv | 29 ---- analysis/04_dos_protection.entry.mpv | 136 ------------------ 4 files changed, 286 deletions(-) delete mode 100644 analysis/03_identity_hiding_initiator.entry.mpv delete mode 100644 analysis/03_identity_hiding_responder.entry.mpv delete mode 100644 analysis/03_identity_hiding_test.entry.mpv delete mode 100644 analysis/04_dos_protection.entry.mpv 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)). -