mirror of
https://github.com/rosenpass/rosenpass.git
synced 2025-12-05 20:40:02 -08:00
chore: Rollback symbolic models to original state
The later edits where unfortunately incomplete. They lacked modeling of multi-session, multi-user settings and they generally rendered the models less trustworthy from my perspective. These edits are still interesting as a starting point for analyzing identity hiding and stealth, but they are not high-quality enough to be present in main.
This commit is contained in:
Karolin Varner
@@ -3,33 +3,12 @@
|
||||
#define SESSION_START_EVENTS 0
|
||||
#define RANDOMIZED_CALL_IDS 0
|
||||
|
||||
|
||||
#include "config.mpv"
|
||||
#include "prelude/basic.mpv"
|
||||
#include "crypto/key.mpv"
|
||||
#include "crypto/kem.mpv"
|
||||
|
||||
#include "rosenpass/oracles.mpv"
|
||||
|
||||
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].
|
||||
|
||||
let main = rosenpass_main.
|
||||
|
||||
@lemma "state coherence, initiator: Initiator accepting a RespHello message implies they also generated the associated InitHello message"
|
||||
|
||||
@@ -10,26 +10,6 @@
|
||||
|
||||
let main = rosenpass_main.
|
||||
|
||||
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].
|
||||
|
||||
|
||||
@lemma "non-interruptability: Adv cannot prevent a genuine InitHello message from being accepted"
|
||||
lemma ih:InitHello_t, psk:key, sski:kem_sk, sskr:kem_sk;
|
||||
event(IHRjct(ih, psk, sskr, kem_pub(sski)))
|
||||
|
||||
@@ -88,18 +88,6 @@ set verboseCompleted=VERBOSE.
|
||||
#define SES_EV(...)
|
||||
#endif
|
||||
|
||||
#if COOKIE_EVENTS
|
||||
#define COOKIE_EV(...) __VA_ARGS__
|
||||
#else
|
||||
#define COOKIE_EV(...)
|
||||
#endif
|
||||
|
||||
#if KEM_EVENTS
|
||||
#define KEM_EV(...) __VA_ARGS__
|
||||
#else
|
||||
#define KEM_EV(...)
|
||||
#endif
|
||||
|
||||
|
||||
(* TODO: Authentication timing properties *)
|
||||
(* TODO: Proof that every adversary submitted package is equivalent to one generated by the proper algorithm using different coins. This probably requires introducing an oracle that extracts the coins used and explicitly adding the notion of coins used for Packet->Packet steps and an inductive RNG notion. *)
|
||||
|
||||
@@ -41,32 +41,23 @@ restriction s:seed, p1:Atom, p2:Atom, ad1:Atom, ad2:Atom;
|
||||
event(ConsumeSeed(p1, s, ad1)) && event(ConsumeSeed(p2, s, ad2))
|
||||
==> p1 = p2 && ad1 = ad2.
|
||||
|
||||
letfun create_mac2(k:key, msg:bits) = prf(k,msg).
|
||||
|
||||
#include "rosenpass/responder.macro"
|
||||
fun Cinit_conf(kem_sk_tmpl, key_tmpl, kem_pk_tmpl, InitConf_t) : Atom [data].
|
||||
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). )
|
||||
KEM_EV(event Oinit_conf_KemUse(SessionId, SessionId, Atom).)
|
||||
#ifdef KEM_EVENTS
|
||||
restriction sidi:SessionId, sidr:SessionId, ad1:Atom, ad2:Atom;
|
||||
event(Oinit_conf_KemUse(sidi, sidr, ad1)) && event(Oinit_conf_KemUse(sidi, sidr, ad2))
|
||||
==> ad1 = ad2.
|
||||
#endif
|
||||
event ConsumeBiscuit(Atom, kem_sk, kem_pk, Atom).
|
||||
|
||||
fun Ccookie(key, bits) : Atom[data].
|
||||
|
||||
let Oinit_conf_inner(Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t, call:Atom) =
|
||||
|
||||
let Oinit_conf() =
|
||||
in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic));
|
||||
#if RANDOMIZED_CALL_IDS
|
||||
new call:Atom;
|
||||
#else
|
||||
call <- Cinit_conf(Ssskm, Spsk, Sspkt, ic);
|
||||
#endif
|
||||
SETUP_HANDSHAKE_STATE()
|
||||
|
||||
eski <- kem_sk0;
|
||||
epki <- kem_pk0;
|
||||
let try_ = (
|
||||
let InitConf(sidi, sidr, biscuit, auth) = ic in
|
||||
KEM_EV(event Oinit_conf_KemUse(sidi, sidr, call);)
|
||||
INITCONF_CONSUME()
|
||||
event ConsumeBiscuit(biscuit_no, sskm, spkt, call);
|
||||
CK_EV( event OskOinit_conf(ck_rh, osk); )
|
||||
@@ -81,21 +72,11 @@ let Oinit_conf_inner(Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:Ini
|
||||
0
|
||||
#endif
|
||||
).
|
||||
|
||||
let Oinit_conf() =
|
||||
|
||||
in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic));
|
||||
#if RANDOMIZED_CALL_IDS
|
||||
new call:Atom;
|
||||
#else
|
||||
call <- Cinit_conf(Ssskm, Spsk, Sspkt, ic);
|
||||
#endif
|
||||
|
||||
Oinit_conf_inner(Ssskm, Spsk, Sspkt, ic, call).
|
||||
|
||||
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))
|
||||
==> ad1 = ad2.
|
||||
|
||||
// TODO: Restriction biscuit no invalidation
|
||||
|
||||
#include "rosenpass/initiator.macro"
|
||||
@@ -104,56 +85,27 @@ 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). )
|
||||
|
||||
KEM_EV(event Oresp_hello_KemUse(SessionId, SessionId, Atom).)
|
||||
#ifdef KEM_EVENTS
|
||||
restriction sidi:SessionId, sidr:SessionId, ad1:Atom, ad2:Atom;
|
||||
event(Oresp_hello_KemUse(sidi, sidr, ad1)) && event(Oresp_hello_KemUse(sidi, sidr, ad2))
|
||||
==> ad1 = ad2.
|
||||
#endif
|
||||
|
||||
#ifdef COOKIE_EVENTS
|
||||
COOKIE_EVENTS(Oresp_hello)
|
||||
#endif
|
||||
let Oresp_hello(HS_DECL_ARGS, C_in:channel, call:Atom) =
|
||||
in(C_in, Cresp_hello(RespHello(sidr, =sidi, ecti, scti, biscuit, auth)));
|
||||
in(C_in, mac2_key:key);
|
||||
let Oresp_hello(HS_DECL_ARGS) =
|
||||
in(C, Cresp_hello(RespHello(sidr, =sidi, ecti, scti, biscuit, auth)));
|
||||
rh <- RespHello(sidr, sidi, ecti, scti, biscuit, auth);
|
||||
#ifdef COOKIE_EVENTS
|
||||
msg <- RH2b(rh);
|
||||
|
||||
COOKIE_PROCESS(Oresp_hello,
|
||||
#endif
|
||||
/* try */ let ic = (
|
||||
ck_ini <- ck;
|
||||
KEM_EV(event Oresp_hello_KemUse(sidi, sidr, call);)
|
||||
RESPHELLO_CONSUME()
|
||||
ck_ih <- ck;
|
||||
INITCONF_PRODUCE()
|
||||
CK_EV (event OskOresp_hello(ck_ini, ck_ih, osk); ) // TODO: Queries testing that there is no duplication
|
||||
MTX_EV( event ICSent(rh, ic, psk, sski, spkr); )
|
||||
SES_EV( event InitiatorSession(rh, osk); )
|
||||
ic
|
||||
/* success */ ) in (
|
||||
icbits <- IC2b(ic);
|
||||
mac <- create_mac(spkt, icbits);
|
||||
mac2 <- create_mac2(mac2_key, mac_envelope2b(mac));
|
||||
out(C_in, ic);
|
||||
out(C_in, mac);
|
||||
out(C_in, mac2)
|
||||
|
||||
/* fail */ ) else (
|
||||
#if MESSAGE_TRANSMISSION_EVENTS
|
||||
event RHRjct(rh, psk, sski, spkr)
|
||||
#else
|
||||
0
|
||||
#endif
|
||||
)
|
||||
#ifdef COOKIE_EVENTS
|
||||
)
|
||||
/* try */ let ic = (
|
||||
ck_ini <- ck;
|
||||
RESPHELLO_CONSUME()
|
||||
ck_ih <- ck;
|
||||
INITCONF_PRODUCE()
|
||||
CK_EV (event OskOresp_hello(ck_ini, ck_ih, osk); ) // TODO: Queries testing that there is no duplication
|
||||
MTX_EV( event ICSent(rh, ic, psk, sski, spkr); )
|
||||
SES_EV( event InitiatorSession(rh, osk); )
|
||||
ic
|
||||
/* success */ ) in (
|
||||
out(C, ic)
|
||||
/* fail */ ) else (
|
||||
#if MESSAGE_TRANSMISSION_EVENTS
|
||||
event RHRjct(rh, psk, sski, spkr)
|
||||
#else
|
||||
.
|
||||
0
|
||||
#endif
|
||||
).
|
||||
|
||||
// TODO: Restriction: Biscuit no invalidation
|
||||
|
||||
@@ -164,33 +116,24 @@ 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).
|
||||
KEM_EV(event Oinit_hello_KemUse(SessionId, SessionId, Atom).)
|
||||
|
||||
#ifdef KEM_EVENTS
|
||||
restriction sidi:SessionId, sidr:SessionId, ad1:Atom, ad2:Atom;
|
||||
event(Oinit_hello_KemUse(sidi, sidr, ad1)) && event(Oinit_hello_KemUse(sidi, sidr, ad2))
|
||||
==> ad1 = ad2.
|
||||
let Oinit_hello() =
|
||||
in(C, Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih));
|
||||
#if RANDOMIZED_CALL_IDS
|
||||
new call:Atom;
|
||||
#else
|
||||
call <- Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih);
|
||||
#endif
|
||||
|
||||
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, mac2_key:key, C_out:channel, call:Atom) =
|
||||
// TODO: This is ugly
|
||||
let InitHello(sidi, epki, sctr, pidiC, auth) = ih in
|
||||
|
||||
SETUP_HANDSHAKE_STATE()
|
||||
|
||||
eski <- kem_sk0;
|
||||
|
||||
event ConsumeBn(biscuit_no, sskm, spkt, call);
|
||||
event ConsumeSidr(sidr, call);
|
||||
|
||||
epti <- rng_key(setup_seed(Septi)); // RHR4
|
||||
spti <- rng_key(setup_seed(Sspti)); // RHR5
|
||||
event ConsumeBn(biscuit_no, sskm, spkt, call);
|
||||
event ConsumeSidr(sidr, call);
|
||||
event ConsumeSeed(Epti, setup_seed(Septi), call);
|
||||
event ConsumeSeed(Spti, setup_seed(Sspti), call);
|
||||
// out(C_out, spkt);
|
||||
|
||||
let rh = (
|
||||
KEM_EV(event Oinit_hello_KemUse(sidi, sidr, call);)
|
||||
INITHELLO_CONSUME()
|
||||
ck_ini <- ck;
|
||||
RESPHELLO_PRODUCE()
|
||||
@@ -198,14 +141,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 (
|
||||
rhbits <- RH2b(rh);
|
||||
mac <- create_mac(spkt, rhbits);
|
||||
|
||||
out(C_out, rh);
|
||||
out(C_out, mac);
|
||||
mac2 <- create_mac2(mac2_key, mac_envelope2b(mac));
|
||||
out(C_out, mac2)
|
||||
|
||||
out(C, rh)
|
||||
/* fail */ ) else (
|
||||
#if MESSAGE_TRANSMISSION_EVENTS
|
||||
event IHRjct(ih, psk, sskr, spki)
|
||||
@@ -214,18 +150,6 @@ let Oinit_hello_inner(sidm:SessionId, biscuit_no:Atom, Ssskm:kem_sk_tmpl, Spsk:k
|
||||
#endif
|
||||
).
|
||||
|
||||
let Oinit_hello() =
|
||||
in(C, Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih));
|
||||
in(C, mac2_key:key);
|
||||
|
||||
#if RANDOMIZED_CALL_IDS
|
||||
new call:Atom;
|
||||
#else
|
||||
call <- Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih);
|
||||
#endif
|
||||
|
||||
Oinit_hello_inner(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih, mac2_key, C, call).
|
||||
|
||||
restriction sid:SessionId, ad1:Atom, ad2:Atom;
|
||||
event(ConsumeSidr(sid, ad1)) && event(ConsumeSidr(sid, ad2))
|
||||
==> ad1 = ad2.
|
||||
@@ -242,55 +166,27 @@ fun Cinitiator(SessionId, kem_sk_tmpl, key_tmpl, kem_pk_tmpl, seed_tmpl, seed_tm
|
||||
CK_EV( event OskOinitiator_ck(key). )
|
||||
CK_EV( event OskOinitiator(key, key, kem_sk, kem_pk, key). )
|
||||
MTX_EV( event IHSent(InitHello_t, key, kem_sk, kem_pk). )
|
||||
KEM_EV(event Oinitiator_inner_KemUse(SessionId, SessionId, Atom).)
|
||||
|
||||
#ifdef KEM_EVENTS
|
||||
restriction sidi:SessionId, sidr:SessionId, ad1:Atom, ad2:Atom;
|
||||
event(Oinitiator_inner_KemUse(sidi, sidr, ad1)) && event(Oinitiator_inner_KemUse(sidi, sidr, ad2))
|
||||
==> ad1 = ad2.
|
||||
#endif
|
||||
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, last_cookie:key, C_out:channel, call:Atom) =
|
||||
|
||||
SETUP_HANDSHAKE_STATE()
|
||||
sidr <- sid0;
|
||||
|
||||
KEM_EV(event Oinitiator_inner_KemUse(sidi, sidr, call);)
|
||||
|
||||
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_out, ih);
|
||||
ihbits <- IH2b(ih);
|
||||
mac <- create_mac(spkt, ihbits);
|
||||
out(C_out, mac);
|
||||
mac2 <- create_mac2(last_cookie, mac_envelope2b(mac));
|
||||
out(C_out, mac2);
|
||||
|
||||
Oresp_hello(HS_PASS_ARGS, C_out, call).
|
||||
|
||||
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
|
||||
|
||||
in(C, last_cookie:key);
|
||||
Oinitiator_inner(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr, last_cookie, C, call).
|
||||
|
||||
#if RANDOMIZED_CALL_IDS
|
||||
new call:Atom;
|
||||
#else
|
||||
call <- Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr);
|
||||
#endif
|
||||
SETUP_HANDSHAKE_STATE()
|
||||
RNG_KEM_PAIR(eski, epki, Seski) // IHI3
|
||||
sidr <- sid0;
|
||||
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, ih);
|
||||
Oresp_hello(HS_PASS_ARGS).
|
||||
|
||||
restriction sid:SessionId, ad1:Atom, ad2:Atom;
|
||||
event(ConsumeSidi(sid, ad1)) && event(ConsumeSidi(sid, ad2))
|
||||
@@ -311,3 +207,21 @@ let rosenpass_main() = 0
|
||||
| REP(RESPONDER_BOUND, Oinit_hello)
|
||||
| REP(RESPONDER_BOUND, Oinit_conf).
|
||||
|
||||
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].
|
||||
|
||||
@@ -2,26 +2,6 @@
|
||||
#include "crypto/kem.mpv"
|
||||
#include "rosenpass/handshake_state.mpv"
|
||||
|
||||
fun Envelope(
|
||||
key,
|
||||
bits
|
||||
): bits [data].
|
||||
|
||||
type mac_envelope_t.
|
||||
fun mac_envelope(
|
||||
key,
|
||||
bits
|
||||
) : mac_envelope_t.
|
||||
|
||||
fun mac_envelope2b(mac_envelope_t) : bits [typeConverter].
|
||||
|
||||
letfun create_mac(pk:kem_pk, payload:bits) = mac_envelope(lprf2(MAC, kem_pk2b(pk), payload), payload).
|
||||
|
||||
fun mac_envelope_pk_test(mac_envelope_t, kem_pk) : bool
|
||||
reduc forall pk:kem_pk, b:bits;
|
||||
mac_envelope_pk_test(mac_envelope(prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pk2b(pk)),
|
||||
b), b), pk) = true.
|
||||
|
||||
type InitHello_t.
|
||||
fun InitHello(
|
||||
SessionId, // sidi
|
||||
@@ -31,8 +11,6 @@ fun InitHello(
|
||||
bits // auth
|
||||
) : InitHello_t [data].
|
||||
|
||||
fun IH2b(InitHello_t) : bitstring [typeConverter].
|
||||
|
||||
#define INITHELLO_PRODUCE() \
|
||||
ck <- lprf1(CK_INIT, kem_pk2b(spkr)); /* IHI1 */ \
|
||||
/* not handled here */ /* IHI2 */ \
|
||||
@@ -63,9 +41,7 @@ fun RespHello(
|
||||
bits // auth
|
||||
) : RespHello_t [data].
|
||||
|
||||
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 */ \
|
||||
@@ -91,14 +67,13 @@ fun InitConf(
|
||||
bits // auth
|
||||
) : InitConf_t [data].
|
||||
|
||||
fun IC2b(InitConf_t) : bitstring [typeConverter].
|
||||
|
||||
#define INITCONF_PRODUCE() \
|
||||
MIX2(sid2b(sidi), sid2b(sidr)) /* ICI3 */ \
|
||||
ENCRYPT_AND_MIX(auth, empty) /* ICI4 */ \
|
||||
ic <- InitConf(sidi, sidr, biscuit, auth);
|
||||
|
||||
#define INITCONF_CONSUME() \
|
||||
let InitConf(sidi, sidr, biscuit, auth) = ic in \
|
||||
LOAD_BISCUIT(biscuit_no, biscuit) /* ICR1 */ \
|
||||
ENCRYPT_AND_MIX(rh_auth, empty) /* ICIR */ \
|
||||
ck_rh <- ck; /* ---- */ /* TODO: Move into oracles.mpv */ \
|
||||
|
||||
Reference in New Issue
Block a user