diff --git a/Cargo.lock b/Cargo.lock
index 408d357..caa73f8 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2568,9 +2568,9 @@ checksum = "a8f112729512f8e442d81f95a8a7ddf2b7c6b8a1a6f509a95864142b30cab2d3"
[[package]]
name = "stacker"
-version = "0.1.19"
+version = "0.1.21"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d9156ebd5870ef293bfb43f91c7a74528d363ec0d424afe24160ed5a4343d08a"
+checksum = "cddb07e32ddb770749da91081d8d0ac3a16f1a569a18b20348cd371f5dead06b"
dependencies = [
"cc",
"cfg-if",
diff --git a/Cargo.toml b/Cargo.toml
index ae45898..c8fd636 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -88,7 +88,7 @@ assert_tv = { version = "0.6.4" }
base64 = { version = "0.22.1" }
serial_test = "3.2.0"
tempfile = "3"
-stacker = "0.1.17"
+stacker = "0.1.21"
libfuzzer-sys = "0.4"
test_bin = "0.4.0"
criterion = "0.5.1"
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)).
-
diff --git a/analysis/rosenpass/03_identity_hiding.mpv b/analysis/rosenpass/03_identity_hiding.mpv
index 112ed6c..dc4901c 100644
--- a/analysis/rosenpass/03_identity_hiding.mpv
+++ b/analysis/rosenpass/03_identity_hiding.mpv
@@ -58,7 +58,7 @@ let secure_init_hello(initiator: kem_sk_tmpl, sidi : SessionId, psk: key_tmpl, r
new epkit:kem_pk; // epki
new sctrt:bits; // sctr
- new pidiCt:bits; // pidiC
+ new pidi_ct:bits; // pidi_ct
new autht:bits; // auth
NEW_TRUSTED_SEED(seski_trusted_seed)
@@ -70,9 +70,9 @@ let secure_init_hello(initiator: kem_sk_tmpl, sidi : SessionId, psk: key_tmpl, r
let secure_resp_hello(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, sidi:SessionId, sidr:SessionId, biscuit_no:Atom, psk:key_tmpl) =
- in(D, InitHello(=secure_sidi, epki, sctr, pidiC, auth));
+ in(D, InitHello(=secure_sidi, epki, sctr, pidi_ct, auth));
- ih <- InitHello(sidi, epki, sctr, pidiC, auth);
+ ih <- InitHello(sidi, epki, sctr, pidi_ct, auth);
NEW_TRUSTED_SEED(septi_trusted_seed)
NEW_TRUSTED_SEED(sspti_trusted_seed)
new last_cookie:key;
diff --git a/analysis/rosenpass/cookie.mpv b/analysis/rosenpass/cookie.mpv
index d28fdef..94cce02 100644
--- a/analysis/rosenpass/cookie.mpv
+++ b/analysis/rosenpass/cookie.mpv
@@ -19,7 +19,7 @@ fun CookieMsg(
COOKIE_EV(event MCAT(eventLbl, _UnderLoadEV) (spkm, spkt, last_cookie);) \
msgB <- Envelope(mac1, RH2b(rh)); \
mac2_key <- create_mac2_key(sskm, spkt) \
- let RespHello(sidi, sidr, ecti, scti, biscuit, auth) = rh in \
+ let RespHello(sidi, sidr, ecti, scti, biscuit_ct, auth) = rh in \
if Envelope(mac2_key, msgB) = mac2 then \
COOKIE_EV(event MCAT(eventLbl, _CookieValidated) (spkm, last_cookie);) \
innerFunc \
diff --git a/analysis/rosenpass/handshake_state.mpv b/analysis/rosenpass/handshake_state.mpv
index c114d8b..6a6bb29 100644
--- a/analysis/rosenpass/handshake_state.mpv
+++ b/analysis/rosenpass/handshake_state.mpv
@@ -143,10 +143,10 @@ letfun ENCRYPT_AND_MIX(ct, pt) \
// TODO: Migrate kems to use binary ciphertexts directly
#define ENCAPS_AND_MIX(ct, pk, shk) \
ct <- kem_enc(pk, shk); \
- MIX3(kem_pk2b(pk), ct, k2b(shk))
+ MIX3(kem_pk2b(pk), k2b(shk), ct)
#define DECAPS_AND_MIX(sk, pk, ct) \
DUMMY(shk) <- kem_dec(sk, ct); \
- MIX3(kem_pk2b(pk), ct, k2b(DUMMY(shk)))
+ MIX3(kem_pk2b(pk), k2b(DUMMY(shk)), ct)
// biscuits
diff --git a/analysis/rosenpass/oracles.mpv b/analysis/rosenpass/oracles.mpv
index d21e6b2..0d8a32d 100644
--- a/analysis/rosenpass/oracles.mpv
+++ b/analysis/rosenpass/oracles.mpv
@@ -86,8 +86,8 @@ 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)));
- rh <- RespHello(sidr, sidi, ecti, scti, biscuit, auth);
+ in(C, Cresp_hello(RespHello(sidr, =sidi, ecti, scti, biscuit_ct, auth)));
+ rh <- RespHello(sidr, sidi, ecti, scti, biscuit_ct, auth);
/* try */ let ic = (
ck_ini <- ck;
RESPHELLO_CONSUME()
@@ -124,7 +124,7 @@ let Oinit_hello() =
call <- Cinit_hello(sidr, biscuit_no, Ssskm, Spsk, Sspkt, Septi, Sspti, ih);
#endif
// TODO: This is ugly
- let InitHello(sidi, epki, sctr, pidiC, auth) = ih in
+ let InitHello(sidi, epki, sctr, pidi_ct, auth) = ih in
SETUP_HANDSHAKE_STATE()
eski <- kem_sk0;
epti <- rng_key(setup_seed(Septi)); // RHR4
diff --git a/analysis/rosenpass/protocol.mpv b/analysis/rosenpass/protocol.mpv
index 658b05f..bb82055 100644
--- a/analysis/rosenpass/protocol.mpv
+++ b/analysis/rosenpass/protocol.mpv
@@ -7,7 +7,7 @@ fun InitHello(
SessionId, // sidi
kem_pk, // epki
bits, // sctr
- bits, // pidiC
+ bits, // pidi_ct
bits // auth
) : InitHello_t [data].
@@ -17,16 +17,16 @@ fun InitHello(
/* not handled here */ /* IHI3 */ \
MIX2(sid2b(sidi), kem_pk2b(epki)) /* IHI4 */ \
ENCAPS_AND_MIX(sctr, spkr, sptr) /* IHI5 */ \
- ENCRYPT_AND_MIX(pidiC, pidi) /* IHI6 */ \
+ ENCRYPT_AND_MIX(pidi_ct, pidi) /* IHI6 */ \
MIX2(kem_pk2b(spki), k2b(psk)) /* IHI7 */ \
ENCRYPT_AND_MIX(auth, empty) /* IHI8 */ \
- ih <- InitHello(sidi, epki, sctr, pidiC, auth);
+ ih <- InitHello(sidi, epki, sctr, pidi_ct, auth);
#define INITHELLO_CONSUME() \
ck <- lprf1(CK_INIT, kem_pk2b(spkr)); /* IHR1 */ \
MIX2(sid2b(sidi), kem_pk2b(epki)) /* IHR4 */ \
DECAPS_AND_MIX(sskr, spkr, sctr) /* IHR5 */ \
- DECRYPT_AND_MIX(pid, pidiC) /* IHR6 */ \
+ DECRYPT_AND_MIX(pid, pidi_ct) /* IHR6 */ \
LOOKUP_SENDER(pid) /* IHR6 */ \
MIX2(kem_pk2b(spki), k2b(psk)) /* IHR7 */ \
DECRYPT_AND_MIX(DUMMY(empty), auth)
@@ -46,17 +46,17 @@ fun RespHello(
MIX2(sid2b(sidr), sid2b(sidi)) /* RHR3 */ \
ENCAPS_AND_MIX(ecti, epki, epti) /* RHR4 */ \
ENCAPS_AND_MIX(scti, spki, spti) /* RHR5 */ \
- STORE_BISCUIT(biscuit) /* RHR6 */ \
+ STORE_BISCUIT(biscuit_ct) /* RHR6 */ \
ENCRYPT_AND_MIX(auth, empty) /* RHR7 */ \
- rh <- RespHello(sidr, sidi, ecti, scti, biscuit, auth);
+ rh <- RespHello(sidr, sidi, ecti, scti, biscuit_ct, auth);
#define RESPHELLO_CONSUME() \
- let RespHello(sidr, sidi, ecti, scti, biscuit, auth) = rh in \
+ let RespHello(sidr, sidi, ecti, scti, biscuit_ct, auth) = rh in \
/* not handled here */ /* RHI2 */ \
MIX2(sid2b(sidr), sid2b(sidi)) /* RHI3 */ \
DECAPS_AND_MIX(eski, epki, ecti) /* RHI4 */ \
DECAPS_AND_MIX(sski, spki, scti) /* RHI5 */ \
- MIX(biscuit) /* RHI6 */ \
+ MIX(biscuit_ct) /* RHI6 */ \
DECRYPT_AND_MIX(DUMMY(empty), auth) /* RHI7 */
type InitConf_t.
@@ -70,11 +70,11 @@ fun InitConf(
#define INITCONF_PRODUCE() \
MIX2(sid2b(sidi), sid2b(sidr)) /* ICI3 */ \
ENCRYPT_AND_MIX(auth, empty) /* ICI4 */ \
- ic <- InitConf(sidi, sidr, biscuit, auth);
+ ic <- InitConf(sidi, sidr, biscuit_ct, auth);
#define INITCONF_CONSUME() \
- let InitConf(sidi, sidr, biscuit, auth) = ic in \
- LOAD_BISCUIT(biscuit_no, biscuit) /* ICR1 */ \
+ let InitConf(sidi, sidr, biscuit_ct, auth) = ic in \
+ LOAD_BISCUIT(biscuit_no, biscuit_ct)/* ICR1 */ \
ENCRYPT_AND_MIX(rh_auth, empty) /* ICIR */ \
ck_rh <- ck; /* ---- */ /* TODO: Move into oracles.mpv */ \
MIX2(sid2b(sidi), sid2b(sidr)) /* ICR3 */ \
diff --git a/papers/graphics/rosenpass-wp-hashing-tree-rgb.pdf b/papers/graphics/rosenpass-wp-hashing-tree-rgb.pdf
deleted file mode 100644
index 4d5708c..0000000
Binary files a/papers/graphics/rosenpass-wp-hashing-tree-rgb.pdf and /dev/null differ
diff --git a/papers/graphics/rosenpass-wp-hashing-tree-rgb.svg b/papers/graphics/rosenpass-wp-hashing-tree-rgb.svg
deleted file mode 100644
index 7228f23..0000000
--- a/papers/graphics/rosenpass-wp-hashing-tree-rgb.svg
+++ /dev/null
@@ -1,2341 +0,0 @@
-
-
-
diff --git a/papers/graphics/rosenpass-wp-hashing-tree.afdesign b/papers/graphics/rosenpass-wp-hashing-tree.afdesign
index e520ce1..d8482fe 100644
Binary files a/papers/graphics/rosenpass-wp-hashing-tree.afdesign and b/papers/graphics/rosenpass-wp-hashing-tree.afdesign differ
diff --git a/papers/graphics/rosenpass-wp-hashing-tree.pdf b/papers/graphics/rosenpass-wp-hashing-tree.pdf
index bc1f09a..3a1fa3a 100644
Binary files a/papers/graphics/rosenpass-wp-hashing-tree.pdf and b/papers/graphics/rosenpass-wp-hashing-tree.pdf differ
diff --git a/papers/graphics/rosenpass-wp-hashing-tree.png b/papers/graphics/rosenpass-wp-hashing-tree.png
index f57bde5..eeed426 100644
Binary files a/papers/graphics/rosenpass-wp-hashing-tree.png and b/papers/graphics/rosenpass-wp-hashing-tree.png differ
diff --git a/papers/graphics/rosenpass-wp-hashing-tree.svg b/papers/graphics/rosenpass-wp-hashing-tree.svg
index b6dafc5..55180c8 100644
--- a/papers/graphics/rosenpass-wp-hashing-tree.svg
+++ b/papers/graphics/rosenpass-wp-hashing-tree.svg
@@ -1,17 +1,17 @@
diff --git a/papers/graphics/rosenpass-wp-key-exchange-protocol-rgb.pdf b/papers/graphics/rosenpass-wp-key-exchange-protocol-rgb.pdf
deleted file mode 100644
index 2caa9e4..0000000
Binary files a/papers/graphics/rosenpass-wp-key-exchange-protocol-rgb.pdf and /dev/null differ
diff --git a/papers/graphics/rosenpass-wp-key-exchange-protocol-rgb.svg b/papers/graphics/rosenpass-wp-key-exchange-protocol-rgb.svg
deleted file mode 100644
index 4e3ed23..0000000
--- a/papers/graphics/rosenpass-wp-key-exchange-protocol-rgb.svg
+++ /dev/null
@@ -1,191 +0,0 @@
-
-
-
diff --git a/papers/graphics/rosenpass-wp-key-exchange-protocol.afdesign b/papers/graphics/rosenpass-wp-key-exchange-protocol.afdesign
new file mode 100644
index 0000000..db70ca8
Binary files /dev/null and b/papers/graphics/rosenpass-wp-key-exchange-protocol.afdesign differ
diff --git a/papers/graphics/rosenpass-wp-key-exchange-protocol.pdf b/papers/graphics/rosenpass-wp-key-exchange-protocol.pdf
index f087c31..49d0642 100644
Binary files a/papers/graphics/rosenpass-wp-key-exchange-protocol.pdf and b/papers/graphics/rosenpass-wp-key-exchange-protocol.pdf differ
diff --git a/papers/graphics/rosenpass-wp-key-exchange-protocol.png b/papers/graphics/rosenpass-wp-key-exchange-protocol.png
index 6c5b3af..0c79732 100644
Binary files a/papers/graphics/rosenpass-wp-key-exchange-protocol.png and b/papers/graphics/rosenpass-wp-key-exchange-protocol.png differ
diff --git a/papers/graphics/rosenpass-wp-key-exchange-protocol.svg b/papers/graphics/rosenpass-wp-key-exchange-protocol.svg
index 3a3d271..1ec21d6 100644
--- a/papers/graphics/rosenpass-wp-key-exchange-protocol.svg
+++ b/papers/graphics/rosenpass-wp-key-exchange-protocol.svg
@@ -1,15 +1,12 @@