From 0cdd06031b4f4b0662705d578041d5bf93146c44 Mon Sep 17 00:00:00 2001 From: James Brownlee Date: Sat, 25 Nov 2023 20:49:32 -0500 Subject: [PATCH] Changed identity hiding test to work as a two stage process where participants with fresh secure secret keys communicate with each other and other compromised participants. Then the attacker is asked to identify the difference between two of the secure participants as on of them acts as a responder. --- analysis/03_identity_hiding.entry.mpv | 107 +++++++++++++++++++--- analysis/crypto/kem.mpv | 5 +- analysis/rosenpass/oracles.mpv | 123 +++++++++----------------- analysis/rosenpass/protocol.mpv | 16 ++-- 4 files changed, 142 insertions(+), 109 deletions(-) diff --git a/analysis/03_identity_hiding.entry.mpv b/analysis/03_identity_hiding.entry.mpv index d18d425..56dff17 100644 --- a/analysis/03_identity_hiding.entry.mpv +++ b/analysis/03_identity_hiding.entry.mpv @@ -4,28 +4,109 @@ #define MESSAGE_TRANSMISSION_EVENTS 1 #define SESSION_START_EVENTS 0 #define RANDOMIZED_CALL_IDS 0 -#define CONSTANT_KEYS 1 -#define SECURE_RNG 1 #undef FULL_MODEL #undef SIMPLE_MODEL #define SIMPLE_MODEL 1 #include "prelude/basic.mpv" #include "crypto/key.mpv" +#include "rosenpass/oracles.mpv" #include "crypto/kem.mpv" -//free initiator_sk1, initiator_sk2, responder_sk: kem_sk [private]. -free initiator_pk, responder_pk: kem_pk[private]. -// noninterf initiator_pk among(kem_pub(initiator_sk1), kem_pub(initiator_sk2)). +#define NEW_TRUSTED_SEED(name) \ + new MCAT(name, _secret_seed):seed_prec; \ + name <- make_trusted_seed(MCAT(name, _secret_seed)); \ -#include "rosenpass/oracles.mpv" +free C2:channel. +free D:channel [private]. +free secure_biscuit_no:Atom [private]. +free secure_sidi,secure_sidr:SessionId [private]. +free secure_psk:key [private]. +free secure_septi_trusted_prec: seed_prec [private]. +free secure_sspti_trusted_prec: seed_prec [private]. +free secure_seski_trusted_prec: seed_prec [private]. +free secure_ssptr_trusted_prec: seed_prec [private]. +free initiator1, initiator2:kem_sk_prec[private]. +free responder1, responder2:kem_sk_prec[private]. + +let secure_init_hello2(initiator: kem_sk_tmpl, sidi : SessionId, psk: key_tmpl, responder: kem_sk_tmpl, C:channel) = + NEW_TRUSTED_SEED(seski_trusted_seed) + NEW_TRUSTED_SEED(ssptr_trusted_seed) + Oinitiator_inner(sidi, initiator, psk, responder, seski_trusted_seed, ssptr_trusted_seed, C). + +let secure_resp_hello2(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, sidr:SessionId, sidi:SessionId, biscuit_no:Atom, psk:key_tmpl, C:channel) = + in(D, Envelope(k, IH2b(InitHello(=sidi, epki, sctr, pidiC, auth)))); + ih <- InitHello(sidi, epki, sctr, pidiC, auth); + NEW_TRUSTED_SEED(septi_trusted_seed) + NEW_TRUSTED_SEED(sspti_trusted_seed) + Oinit_hello_inner(sidr, biscuit_no, responder, psk, initiator, septi_trusted_seed, sspti_trusted_seed, ih, C). + +let secure_init_conf2(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, psk:key_tmpl, sidi:SessionId, sidr:SessionId, C:channel) = + in(D, Envelope(k3, IC2b(InitConf(=sidi, =sidr, biscuit, auth3)))); + ic <- InitConf(sidi,sidr,biscuit, auth3); + NEW_TRUSTED_SEED(seski_trusted_seed) + NEW_TRUSTED_SEED(ssptr_trusted_seed) + Oinit_conf_inner(initiator, psk, responder, ic, C). + +fun Csecure_init_hello(SessionId, key_tmpl, kem_sk_tmpl): Atom[data]. +let secure_init_hello(initiator: kem_sk_tmpl) = + NEW_TRUSTED_SEED(seski_trusted_seed) + NEW_TRUSTED_SEED(ssptr_trusted_seed) + in(C, Csecure_init_hello(sidi, psk, responder)); + Oinitiator_inner(sidi, initiator, psk, responder, seski_trusted_seed, ssptr_trusted_seed, C). + +fun Csecure_resp_hello(SessionId, SessionId, Atom, key_tmpl, kem_sk_tmpl, InitHello_t): Atom[data]. +let secure_resp_hello(initiator: kem_sk_tmpl) = + NEW_TRUSTED_SEED(septi_trusted_seed) + NEW_TRUSTED_SEED(sspti_trusted_seed) + in(C, Csecure_resp_hello(sidr, sidi, biscuit_no, psk, responder, ih)); + Oinit_hello_inner(sidr, biscuit_no, responder, psk, initiator, septi_trusted_seed, sspti_trusted_seed, ih, C). + +fun Csecure_init_conf(key_tmpl, kem_sk_tmpl, InitConf_t): Atom[data]. +let secure_init_conf(initiator: kem_sk_tmpl) = + NEW_TRUSTED_SEED(seski_trusted_seed) + NEW_TRUSTED_SEED(ssptr_trusted_seed) + in(C, Csecure_init_conf(psk, responder, ic)); + Oinit_conf_inner(initiator, psk, responder, ic, C). + +let secure_communication(initiator: kem_sk_tmpl, responder:kem_sk_tmpl, C:channel) = + secure_key <- prepare_key(secure_psk); + (!secure_init_hello2(initiator, secure_sidi, secure_key, responder, C)) + | !secure_resp_hello2(initiator, responder, secure_sidr, secure_sidi, secure_biscuit_no, secure_key, C) + | !(secure_init_conf2(initiator, responder, secure_key, secure_sidi, secure_sidr, C)). + +let run_secure_protocols(participant:kem_sk_tmpl) = + !(secure_init_hello(participant)) + | !(secure_resp_hello(participant)) + | !(secure_init_conf(participant)). + +let secure_particpant_communication() = 0 + | !run_secure_protocols(make_trusted_kem_sk(responder1)) | !run_secure_protocols(make_trusted_kem_sk(responder2)) + | !run_secure_protocols(make_trusted_kem_sk(initiator1)) | !run_secure_protocols(make_trusted_kem_sk(initiator2)). + +let pipeChannel(D:channel, C:channel) = + in(D, b:bits); + out(C, b). + +fun kem_private(kem_pk): kem_sk + reduc forall sk_tmpl:kem_sk; + kem_private(kem_pub(sk_tmpl)) = sk_tmpl[private]. + +let secretCommunication() = + responder_pk <- choice[setup_kem_pk(make_trusted_kem_sk(responder1)), setup_kem_pk(make_trusted_kem_sk(responder2))]; + kem_seed <- prepare_kem_sk(kem_private(responder_pk)); + kem_pk <- setup_kem_pk(kem_seed); + initiator_seed <- prepare_kem_sk(trusted_kem_sk(initiator1)); + secure_communication(initiator_seed, kem_seed, D) | !pipeChannel(D, C2). + +let reveal_pks() = + out(C, setup_kem_pk(make_trusted_kem_sk(responder1))); + out(C, setup_kem_pk(make_trusted_kem_sk(responder2))); + out(C, setup_kem_pk(make_trusted_kem_sk(initiator1))); + out(C, setup_kem_pk(make_trusted_kem_sk(initiator2))). + +let identity_hiding_main() = + 0 | reveal_pks() | secure_particpant_communication() | phase 1; secretCommunication(). -let identity_hiding_main() = 0 - | REP(INITIATOR_BOUND, Oinitiator) - | REP(RESPONDER_BOUND, Oinit_hello) - | REP(RESPONDER_BOUND, Oinit_conf). let main = identity_hiding_main. - -weaksecret initiator_pk. -weaksecret responder_pk. diff --git a/analysis/crypto/kem.mpv b/analysis/crypto/kem.mpv index 168263a..edfbe1d 100644 --- a/analysis/crypto/kem.mpv +++ b/analysis/crypto/kem.mpv @@ -9,13 +9,10 @@ type kem_sk. type kem_pk. fun kem_pub(kem_sk) : kem_pk. -fun kem_private(kem_pk) : kem_sk[private]. fun kem_enc(kem_pk, key) : bits. fun kem_dec(kem_sk, bits) : key reduc forall sk:kem_sk, shk:key; - kem_dec(sk, kem_enc(kem_pub(sk), shk)) = shk - otherwise forall pk:kem_pk, shk:key; - kem_dec(kem_private(pk), kem_enc(pk, shk)) = shk. + kem_dec(sk, kem_enc(kem_pub(sk), shk)) = shk. fun kem_pk2b(kem_pk) : bits [typeConverter]. diff --git a/analysis/rosenpass/oracles.mpv b/analysis/rosenpass/oracles.mpv index 0825f7a..d1c7f44 100644 --- a/analysis/rosenpass/oracles.mpv +++ b/analysis/rosenpass/oracles.mpv @@ -47,23 +47,15 @@ CK_EV( event OskOinit_conf(key, key). ) MTX_EV( event ICRjct(InitConf_t, key, kem_sk, kem_pk). ) SES_EV( event ResponderSession(InitConf_t, key). ) event ConsumeBiscuit(Atom, kem_sk, kem_pk, Atom). -let Oinit_conf() = - in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic)); + +let Oinit_conf_inner(Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t, C_in:channel) = #if RANDOMIZED_CALL_IDS new call:Atom; #else call <- Cinit_conf(Ssskm, Spsk, Sspkt, ic); #endif -#ifdef CONSTANT_KEYS - spkt <- initiator_pk; - spkm <- responder_pk; - sskm <- kem_private(spkm); - psk <- setup_key(Spsk); - biscuit_key <- biscuit_key(sskm); -#else SETUP_HANDSHAKE_STATE() -#endif eski <- kem_sk0; epki <- kem_pk0; @@ -82,6 +74,10 @@ let Oinit_conf() = 0 #endif ). + +let Oinit_conf() = + in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic)); + Oinit_conf_inner(Ssskm, Spsk, Sspkt, ic, C). restriction biscuit_no:Atom, sskm:kem_sk, spkr:kem_pk, ad1:Atom, ad2:Atom; event(ConsumeBiscuit(biscuit_no, sskm, spkr, ad1)) && event(ConsumeBiscuit(biscuit_no, sskm, spkr, ad2)) @@ -95,8 +91,8 @@ CK_EV( event OskOresp_hello(key, key, key). ) MTX_EV( event RHRjct(RespHello_t, key, kem_sk, kem_pk). ) MTX_EV( event ICSent(RespHello_t, InitConf_t, key, kem_sk, kem_pk). ) SES_EV( event InitiatorSession(RespHello_t, key). ) -let Oresp_hello(HS_DECL_ARGS) = - in(C, Cresp_hello(RespHello(sidr, =sidi, ecti, scti, biscuit, auth))); +let Oresp_hello(HS_DECL_ARGS, C_in:channel) = + in(C_in, Cresp_hello(RespHello(sidr, =sidi, ecti, scti, biscuit, auth))); rh <- RespHello(sidr, sidi, ecti, scti, biscuit, auth); /* try */ let ic = ( ck_ini <- ck; @@ -108,7 +104,7 @@ let Oresp_hello(HS_DECL_ARGS) = SES_EV( event InitiatorSession(rh, osk); ) ic /* success */ ) in ( - out(C, EnvelopeInitConf(create_mac(spkt, IC2b(ic)), ic)) + out(C_in, Envelope(create_mac(spkt, IC2b(ic)), IC2b(ic))) /* fail */ ) else ( #if MESSAGE_TRANSMISSION_EVENTS event RHRjct(rh, psk, sski, spkr) @@ -126,8 +122,8 @@ MTX_EV( event IHRjct(InitHello_t, key, kem_sk, kem_pk). ) MTX_EV( event RHSent(InitHello_t, RespHello_t, key, kem_sk, kem_pk). ) event ConsumeSidr(SessionId, Atom). event ConsumeBn(Atom, kem_sk, kem_pk, Atom). -let Oinit_hello() = - in(C, Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih)); + +let Oinit_hello_inner(sidm:SessionId, biscuit_no:Atom, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt: kem_sk_tmpl, Septi: seed_tmpl, Sspti: seed_tmpl, ih: InitHello_t, C_in:channel) = #if RANDOMIZED_CALL_IDS new call:Atom; #else @@ -136,38 +132,17 @@ let Oinit_hello() = // TODO: This is ugly let InitHello(sidi, epki, sctr, pidiC, auth) = ih in -#ifdef CONSTANT_KEYS - spkt <- initiator_pk; - spkm <- responder_pk; - sskm <- kem_private(spkm); - psk <- setup_key(Spsk); - biscuit_key <- biscuit_key(sskm); -#else SETUP_HANDSHAKE_STATE() -#endif eski <- kem_sk0; event ConsumeBn(biscuit_no, sskm, spkt, call); event ConsumeSidr(sidr, call); -#ifdef SECURE_RNG - new septi_trusted_prec: seed_prec; - new sspti_trusted_prec: seed_prec; - - septi_trusted_seed <- make_trusted_seed(septi_trusted_prec); - sspti_trusted_seed <- make_trusted_seed(sspti_trusted_prec); - - epti <- rng_key(setup_seed(septi_trusted_seed)); // RHR4 - spti <- rng_key(setup_seed(sspti_trusted_seed)); // RHR4 - event ConsumeSeed(Epti, setup_seed(septi_trusted_seed), call); - event ConsumeSeed(Spti, setup_seed(sspti_trusted_seed), call); -#else epti <- rng_key(setup_seed(Septi)); // RHR4 spti <- rng_key(setup_seed(Sspti)); // RHR5 event ConsumeSeed(Epti, setup_seed(Septi), call); event ConsumeSeed(Spti, setup_seed(Sspti), call); -#endif let rh = ( INITHELLO_CONSUME() @@ -177,7 +152,8 @@ let Oinit_hello() = MTX_EV( event RHSent(ih, rh, psk, sskr, spki); ) rh /* success */ ) in ( - out(C, EnvelopeRespHello(create_mac(spkt, RH2b(rh)), rh)) + out(C_in, Envelope(create_mac(spkt, RH2b(rh)), RH2b(rh))) + /* fail */ ) else ( #if MESSAGE_TRANSMISSION_EVENTS event IHRjct(ih, psk, sskr, spki) @@ -186,6 +162,10 @@ let Oinit_hello() = #endif ). +let Oinit_hello() = + in(C, Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih)); + Oinit_hello_inner(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih, C). + restriction sid:SessionId, ad1:Atom, ad2:Atom; event(ConsumeSidr(sid, ad1)) && event(ConsumeSidr(sid, ad2)) ==> ad1 = ad2. @@ -204,52 +184,33 @@ CK_EV( event OskOinitiator(key, key, kem_sk, kem_pk, key). ) MTX_EV( event IHSent(InitHello_t, key, kem_sk, kem_pk). ) event ConsumeSidi(SessionId, Atom). +let Oinitiator_inner(sidi: SessionId, Ssskm: kem_sk_tmpl, Spsk: key_tmpl, Sspkt: kem_sk_tmpl, Seski: seed_tmpl, Ssptr: seed_tmpl, C_in:channel) = + #if RANDOMIZED_CALL_IDS + new call:Atom; + #else + call <- Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr); + #endif + + SETUP_HANDSHAKE_STATE() + + sidr <- sid0; + + RNG_KEM_PAIR(eski, epki, Seski) // IHI3 + sptr <- rng_key(setup_seed(Ssptr)); // IHI5 + event ConsumeSidi(sidi, call); + event ConsumeSeed(Sptr, setup_seed(Ssptr), call); + event ConsumeSeed(Eski, setup_seed(Seski), call); + + INITHELLO_PRODUCE() + CK_EV( event OskOinitiator_ck(ck); ) + CK_EV( event OskOinitiator(ck, psk, sski, spkr, sptr); ) + MTX_EV( event IHSent(ih, psk, sski, spkr); ) + out(C_in, Envelope(create_mac(spkt, IH2b(ih)), IH2b(ih))); + Oresp_hello(HS_PASS_ARGS, C). + let Oinitiator() = 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 - -#ifdef CONSTANT_KEYS - spkt <- responder_pk; - spkm <- initiator_pk; - sskm <- kem_private(spkm); - psk <- setup_key(Spsk); - biscuit_key <- biscuit_key(sskm); -#else - SETUP_HANDSHAKE_STATE() -#endif - - sidr <- sid0; - -#ifdef SECURE_RNG - new ssptr_trusted_prec: seed_prec; - new seski_trusted_prec: seed_prec; - - ssptr_trusted_seed <- make_trusted_seed(ssptr_trusted_prec); - seski_trusted_seed <- make_trusted_seed(seski_trusted_prec); - - RNG_KEM_PAIR(eski, epki, seski_trusted_seed) // IHI3 - sptr <- rng_key(setup_seed(ssptr_trusted_seed)); // IHI5 - event ConsumeSidi(sidi, call); - event ConsumeSeed(Sptr, setup_seed(ssptr_trusted_seed), call); - event ConsumeSeed(Eski, setup_seed(seski_trusted_seed), call); -#else - RNG_KEM_PAIR(eski, epki, Seski) // IHI3 - sptr <- rng_key(setup_seed(Ssptr)); // IHI5 - event ConsumeSidi(sidi, call); - event ConsumeSeed(Sptr, setup_seed(Ssptr), call); - event ConsumeSeed(Eski, setup_seed(Seski), call); -#endif - - INITHELLO_PRODUCE() - CK_EV( event OskOinitiator_ck(ck); ) - CK_EV( event OskOinitiator(ck, psk, sski, spkr, sptr); ) - MTX_EV( event IHSent(ih, psk, sski, spkr); ) - out(C, EnvelopeInitHello(create_mac(spkt, IH2b(ih) ), ih)); - Oresp_hello(HS_PASS_ARGS). + Oinitiator_inner(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr, C). restriction sid:SessionId, ad1:Atom, ad2:Atom; event(ConsumeSidi(sid, ad1)) && event(ConsumeSidi(sid, ad2)) diff --git a/analysis/rosenpass/protocol.mpv b/analysis/rosenpass/protocol.mpv index 9874cf4..a900981 100644 --- a/analysis/rosenpass/protocol.mpv +++ b/analysis/rosenpass/protocol.mpv @@ -2,13 +2,10 @@ #include "crypto/kem.mpv" #include "rosenpass/handshake_state.mpv" -#define ENVELOPE(TYPE) \ - type MCAT(MCAT(Envelope, TYPE), _t). \ - fun CAT(Envelope, TYPE) ( \ - key, \ - MCAT(TYPE, _t) \ - ) : MCAT(MCAT(Envelope, TYPE), _t) [data]. - +fun Envelope( + key, + bits +): bits [data]. letfun create_mac(pk:kem_pk, payload:bits) = lprf2(MAC, kem_pk2b(pk), payload). type InitHello_t. @@ -20,7 +17,6 @@ fun InitHello( bits // auth ) : InitHello_t [data]. -ENVELOPE(InitHello) fun IH2b(InitHello_t) : bitstring [typeConverter]. #define INITHELLO_PRODUCE() \ @@ -53,10 +49,9 @@ fun RespHello( bits // auth ) : RespHello_t [data]. -ENVELOPE(RespHello) fun RH2b(RespHello_t) : bitstring [typeConverter]. -#define RESPHELLO_PRODUCE() \ +#define RESPHELLO_PRODUCE() \ /* not handled here */ /* RHR1 */ \ MIX2(sid2b(sidr), sid2b(sidi)) /* RHR3 */ \ ENCAPS_AND_MIX(ecti, epki, epti) /* RHR4 */ \ @@ -82,7 +77,6 @@ fun InitConf( bits // auth ) : InitConf_t [data]. -ENVELOPE(InitConf) fun IC2b(InitConf_t) : bitstring [typeConverter]. #define INITCONF_PRODUCE() \