gitea-mirror/rosenpass
1
0
Fork 0
mirror of https://github.com/rosenpass/rosenpass.git synced 2026-02-27 22:13:12 -08:00
Code Issues Packages Projects Releases Wiki Activity

fixed issues with identity hiding proverif code

Browse Source
This commit is contained in:
James Brownlee
2023-12-14 21:02:39 -05:00
parent 2c4ab16eb7
commit df8990f4f8
2 changed files with 34 additions and 65 deletions
Download Patch File Download Diff File Expand all files Collapse all files

85
analysis/03_identity_hiding.entry.mpv
View File

@@ -17,72 +17,37 @@
new MCAT(name, _secret_seed):seed_prec; \ new MCAT(name, _secret_seed):seed_prec; \
name <- make_trusted_seed(MCAT(name, _secret_seed)); \ name <- make_trusted_seed(MCAT(name, _secret_seed)); \
free C2:channel.
free D:channel [private]. free D:channel [private].
free secure_biscuit_no:Atom [private]. free secure_biscuit_no:Atom [private].
free secure_sidi,secure_sidr:SessionId [private]. free secure_sidi,secure_sidr:SessionId [private].
free secure_psk:key [private]. free secure_psk:key [private].
free secure_septi_trusted_prec: seed_prec [private]. free initiator1, initiator2:kem_sk_prec.
free secure_sspti_trusted_prec: seed_prec [private]. free responder1, responder2:kem_sk_prec.
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) = 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(seski_trusted_seed)
NEW_TRUSTED_SEED(ssptr_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) = let secure_resp_hello(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, sidr:SessionId, sidi:SessionId, biscuit_no:Atom, psk:key_tmpl) =
in(C_in, Envelope(k, IH2b(InitHello(=sidi, epki, sctr, pidiC, auth)))); in(D, Envelope(k, IH2b(InitHello(=sidi, epki, sctr, pidiC, auth))));
ih <- InitHello(sidi, epki, sctr, pidiC, auth); ih <- InitHello(sidi, epki, sctr, pidiC, auth);
NEW_TRUSTED_SEED(septi_trusted_seed) NEW_TRUSTED_SEED(septi_trusted_seed)
NEW_TRUSTED_SEED(sspti_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) = let secure_init_conf(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, psk:key_tmpl, sidi:SessionId, sidr:SessionId) =
in(C_in, Envelope(k3, IC2b(InitConf(=sidi, =sidr, biscuit, auth3)))); in(D, Envelope(k3, IC2b(InitConf(=sidi, =sidr, biscuit, auth3))));
ic <- InitConf(sidi,sidr,biscuit, auth3); ic <- InitConf(sidi,sidr,biscuit, auth3);
NEW_TRUSTED_SEED(seski_trusted_seed) NEW_TRUSTED_SEED(seski_trusted_seed)
NEW_TRUSTED_SEED(ssptr_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_communication(initiator: kem_sk_tmpl, responder:kem_sk_tmpl) =
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_key <- prepare_key(secure_psk);
(!secure_init_hello2(initiator, secure_sidi, secure_key, responder, C)) (!secure_init_hello(initiator, secure_sidi, secure_key, responder))
| !secure_resp_hello2(initiator, responder, secure_sidr, secure_sidi, secure_biscuit_no, secure_key, C) | !secure_resp_hello(initiator, responder, secure_sidr, secure_sidi, secure_biscuit_no, secure_key)
| !(secure_init_conf2(initiator, responder, secure_key, secure_sidi, secure_sidr, C)). | !(secure_init_conf(initiator, responder, secure_key, secure_sidi, secure_sidr)).
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) = let pipeChannel(D:channel, C:channel) =
in(D, b:bits); in(D, b:bits);
@@ -93,13 +58,13 @@ fun kem_private(kem_pk): kem_sk
kem_private(kem_pub(sk_tmpl)) = sk_tmpl[private]. kem_private(kem_pub(sk_tmpl)) = sk_tmpl[private].
let secretCommunication() = let secretCommunication() =
// initiator_pk <- choice[setup_kem_pk(make_trusted_kem_sk(initiator1)), setup_kem_pk(make_trusted_kem_sk(initiator2))]; 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(kem_private(initiator_pk));
responder_seed <- prepare_kem_sk(trusted_kem_sk(responder1));
initiator_seed <- prepare_kem_sk(trusted_kem_sk(initiator1)); // 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_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)); // responder_seed <- prepare_kem_sk(kem_private(responder_pk));
secure_communication(initiator_seed, responder_seed, D) | !pipeChannel(D, C2). secure_communication(initiator_seed, responder_seed) | !pipeChannel(D, C).
let reveal_pks() = let reveal_pks() =
out(C, setup_kem_pk(make_trusted_kem_sk(responder1))); 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(initiator1)));
out(C, setup_kem_pk(make_trusted_kem_sk(initiator2))). out(C, setup_kem_pk(make_trusted_kem_sk(initiator2))).
let identity_hiding_main() = let rosenpass_main2() =
0 | reveal_pks() | secure_particpant_communication() | phase 1; secretCommunication(). 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. let main = identity_hiding_main.

14
analysis/rosenpass/oracles.mpv
View File

@@ -48,7 +48,7 @@ MTX_EV( event ICRjct(InitConf_t, key, kem_sk, kem_pk). )
SES_EV( event ResponderSession(InitConf_t, key). ) SES_EV( event ResponderSession(InitConf_t, key). )
event ConsumeBiscuit(Atom, kem_sk, kem_pk, Atom). 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 #if RANDOMIZED_CALL_IDS
new call:Atom; new call:Atom;
#else #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() = let Oinit_conf() =
in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic)); 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; 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)) 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 ConsumeSidr(SessionId, Atom).
event ConsumeBn(Atom, kem_sk, kem_pk, 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 #if RANDOMIZED_CALL_IDS
new call:Atom; new call:Atom;
#else #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); ) MTX_EV( event RHSent(ih, rh, psk, sskr, spki); )
rh rh
/* success */ ) in ( /* 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 ( /* fail */ ) else (
#if MESSAGE_TRANSMISSION_EVENTS #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). ) MTX_EV( event IHSent(InitHello_t, key, kem_sk, kem_pk). )
event ConsumeSidi(SessionId, Atom). 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 #if RANDOMIZED_CALL_IDS
new call:Atom; new call:Atom;
#else #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(ck); )
CK_EV( event OskOinitiator(ck, psk, sski, spkr, sptr); ) CK_EV( event OskOinitiator(ck, psk, sski, spkr, sptr); )
MTX_EV( event IHSent(ih, psk, sski, spkr); ) MTX_EV( event IHSent(ih, psk, sski, spkr); )
out(C_in, Envelope(create_mac(spkt, IH2b(ih)), IH2b(ih))); out(C_out, Envelope(create_mac(spkt, IH2b(ih)), IH2b(ih)));
Oresp_hello(HS_PASS_ARGS, C). Oresp_hello(HS_PASS_ARGS, C_out).
let Oinitiator() = let Oinitiator() =
in(C, Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr)); in(C, Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr));