diff --git a/analysis/03_identity_hiding.entry.mpv b/analysis/03_identity_hiding.entry.mpv index 0d8f3f0..93c9389 100644 --- a/analysis/03_identity_hiding.entry.mpv +++ b/analysis/03_identity_hiding.entry.mpv @@ -17,72 +17,37 @@ new MCAT(name, _secret_seed):seed_prec; \ name <- make_trusted_seed(MCAT(name, _secret_seed)); \ -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]. +free initiator1, initiator2:kem_sk_prec. +free responder1, responder2:kem_sk_prec. -let secure_init_hello2(initiator: kem_sk_tmpl, sidi : SessionId, psk: key_tmpl, responder: kem_sk_tmpl, C:channel) = +let secure_init_hello(initiator: kem_sk_tmpl, sidi : SessionId, psk: key_tmpl, responder: kem_sk_tmpl) = 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). + Oinitiator_inner(sidi, initiator, psk, responder, seski_trusted_seed, ssptr_trusted_seed, D). -let secure_resp_hello2(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, sidr:SessionId, sidi:SessionId, biscuit_no:Atom, psk:key_tmpl, C_in:channel) = - in(C_in, Envelope(k, IH2b(InitHello(=sidi, epki, sctr, pidiC, auth)))); +let secure_resp_hello(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, sidr:SessionId, sidi:SessionId, biscuit_no:Atom, psk:key_tmpl) = + 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). + Oinit_hello_inner(sidr, biscuit_no, responder, psk, initiator, septi_trusted_seed, sspti_trusted_seed, ih, D). -let secure_init_conf2(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, psk:key_tmpl, sidi:SessionId, sidr:SessionId, C_in:channel) = - in(C_in, Envelope(k3, IC2b(InitConf(=sidi, =sidr, biscuit, auth3)))); +let secure_init_conf(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, psk:key_tmpl, sidi:SessionId, sidr:SessionId) = + 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). + Oinit_conf_inner(initiator, psk, responder, ic). -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) = +let secure_communication(initiator: kem_sk_tmpl, responder:kem_sk_tmpl) = 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)). + (!secure_init_hello(initiator, secure_sidi, secure_key, responder)) + | !secure_resp_hello(initiator, responder, secure_sidr, secure_sidi, secure_biscuit_no, secure_key) + | !(secure_init_conf(initiator, responder, secure_key, secure_sidi, secure_sidr)). let pipeChannel(D:channel, C:channel) = in(D, b:bits); @@ -93,13 +58,13 @@ fun kem_private(kem_pk): kem_sk kem_private(kem_pub(sk_tmpl)) = sk_tmpl[private]. let secretCommunication() = - // initiator_pk <- choice[setup_kem_pk(make_trusted_kem_sk(initiator1)), setup_kem_pk(make_trusted_kem_sk(initiator2))]; - // initiator_seed <- prepare_kem_sk(kem_private(initiator_pk)); - - initiator_seed <- prepare_kem_sk(trusted_kem_sk(initiator1)); - responder_pk <- choice[setup_kem_pk(make_trusted_kem_sk(responder1)), setup_kem_pk(make_trusted_kem_sk(responder2))]; - responder_seed <- prepare_kem_sk(kem_private(responder_pk)); - secure_communication(initiator_seed, responder_seed, D) | !pipeChannel(D, C2). + initiator_pk <- choice[setup_kem_pk(make_trusted_kem_sk(initiator1)), setup_kem_pk(make_trusted_kem_sk(initiator2))]; + initiator_seed <- prepare_kem_sk(kem_private(initiator_pk)); + responder_seed <- prepare_kem_sk(trusted_kem_sk(responder1)); + // initiator_seed <- prepare_kem_sk(trusted_kem_sk(initiator1)); + // responder_pk <- choice[setup_kem_pk(make_trusted_kem_sk(responder1)), setup_kem_pk(make_trusted_kem_sk(responder2))]; + // responder_seed <- prepare_kem_sk(kem_private(responder_pk)); + secure_communication(initiator_seed, responder_seed) | !pipeChannel(D, C). let reveal_pks() = out(C, setup_kem_pk(make_trusted_kem_sk(responder1))); @@ -107,8 +72,12 @@ let reveal_pks() = 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 rosenpass_main2() = + REP(INITIATOR_BOUND, Oinitiator) + | REP(RESPONDER_BOUND, Oinit_hello) + | REP(RESPONDER_BOUND, Oinit_conf). +let identity_hiding_main() = + 0 | reveal_pks() | rosenpass_main2() | phase 1; secretCommunication(). let main = identity_hiding_main. diff --git a/analysis/rosenpass/oracles.mpv b/analysis/rosenpass/oracles.mpv index d1c7f44..9212ac7 100644 --- a/analysis/rosenpass/oracles.mpv +++ b/analysis/rosenpass/oracles.mpv @@ -48,7 +48,7 @@ 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_inner(Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t, C_in:channel) = +let Oinit_conf_inner(Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t) = #if RANDOMIZED_CALL_IDS new call:Atom; #else @@ -77,7 +77,7 @@ let Oinit_conf_inner(Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:Ini let Oinit_conf() = in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic)); - Oinit_conf_inner(Ssskm, Spsk, Sspkt, ic, C). + Oinit_conf_inner(Ssskm, Spsk, Sspkt, ic). 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)) @@ -123,7 +123,7 @@ 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_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) = +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_out:channel) = #if RANDOMIZED_CALL_IDS new call:Atom; #else @@ -152,7 +152,7 @@ let Oinit_hello_inner(sidm:SessionId, biscuit_no:Atom, Ssskm:kem_sk_tmpl, Spsk:k MTX_EV( event RHSent(ih, rh, psk, sskr, spki); ) rh /* success */ ) in ( - out(C_in, Envelope(create_mac(spkt, RH2b(rh)), RH2b(rh))) + out(C_out, Envelope(create_mac(spkt, RH2b(rh)), RH2b(rh))) /* fail */ ) else ( #if MESSAGE_TRANSMISSION_EVENTS @@ -184,7 +184,7 @@ 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) = +let Oinitiator_inner(sidi: SessionId, Ssskm: kem_sk_tmpl, Spsk: key_tmpl, Sspkt: kem_sk_tmpl, Seski: seed_tmpl, Ssptr: seed_tmpl, C_out:channel) = #if RANDOMIZED_CALL_IDS new call:Atom; #else @@ -205,8 +205,8 @@ let Oinitiator_inner(sidi: SessionId, Ssskm: kem_sk_tmpl, Spsk: key_tmpl, Sspkt: 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). + out(C_out, Envelope(create_mac(spkt, IH2b(ih)), IH2b(ih))); + Oresp_hello(HS_PASS_ARGS, C_out). let Oinitiator() = in(C, Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr));