From 9e8f43f9a0c739fc32d8c6a83de500856a905300 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Tue, 14 Jul 2026 15:05:34 +0200 Subject: [PATCH 1/6] =?UTF-8?q?Add=20hax=E2=86=92ProVerif=20symbolic=20sec?= =?UTF-8?q?urity=20analysis=20for=20protocol-minimal?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Symbolic (Dolev-Yao) verification of the SecureDrop protocol via the hax ProVerif backend. 13/13 properties verified across three layers: - Message: submission/reply confidentiality + sender/journalist authentication - Enrollment: FPF->Newsroom->Journalist trust chain, rogue journalist refuted (with a load-bearing soundness demo that the newsroom-signature check matters) - Fetch: wrong-recipient secrecy + recipient anonymity (observational equivalence) Drives the ACTUAL extracted Rust (encrypt, decrypt_with_sender, auth_enc/dec, metadata enc/dec, sign/verify); the 3-party DH fetch clue is hand-modeled with a documented, idealized algebra (see VERIFICATION.md limitations). All annotations are cfg(hax_backend_proverif)-gated, so cargo build, cargo test, and the F* pipeline (proofs/fstar/) are unaffected. Engine-free CI lane (.github/workflows/proverif.yml) + `make proverif-check` run against a committed, sha-pinned model snapshot; `make proverif-extract` re-derives it. See proofs/proverif/VERIFICATION.md (status + trust assumptions) and PLAN.md. Co-Authored-By: Claude Opus 4.8 (1M context) --- .github/workflows/proverif.yml | 38 ++ securedrop-protocol/Cargo.toml | 5 +- securedrop-protocol/protocol-minimal/Makefile | 9 + .../protocol-minimal/proofs/proverif/PLAN.md | 393 ++++++++++++++ .../proofs/proverif/VERIFICATION.md | 226 ++++++++ .../proofs/proverif/extraction/.gitignore | 2 + .../proofs/proverif/extraction/lib.pvl | 319 +++++++++++ .../proofs/proverif/extraction/lib.pvl.sha256 | 1 + .../proverif/extraction/missingdecl.pvl | 18 + .../proofs/proverif/handwritten/sd_crypto.pvl | 48 ++ .../proofs/proverif/handwritten/sd_model.pvl | 58 ++ .../protocol-minimal/proofs/proverif/hax.py | 353 ++++++++++++ .../proofs/proverif/lib/PROVENANCE.md | 24 + .../proofs/proverif/lib/cryptolib.pvl | 124 +++++ .../proofs/proverif/lib/primitives.pvl | 503 ++++++++++++++++++ .../proofs/proverif/queries/enrollment.pv | 84 +++ .../proverif/queries/enrollment_soundness.pv | 63 +++ .../proofs/proverif/queries/fetch.pv | 79 +++ .../proofs/proverif/queries/fetch_unlink.pv | 44 ++ .../proofs/proverif/queries/reply.pv | 69 +++ .../proofs/proverif/queries/submission.pv | 70 +++ .../protocol-minimal/src/ciphertext.rs | 4 + .../protocol-minimal/src/keys.rs | 3 + .../protocol-minimal/src/message.rs | 22 + .../protocol-minimal/src/metadata.rs | 15 + .../protocol-minimal/src/primitives/x25519.rs | 20 + .../protocol-minimal/src/sign.rs | 18 + 27 files changed, 2611 insertions(+), 1 deletion(-) create mode 100644 .github/workflows/proverif.yml create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/PLAN.md create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/extraction/.gitignore create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl.sha256 create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/extraction/missingdecl.pvl create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/handwritten/sd_crypto.pvl create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/handwritten/sd_model.pvl create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/hax.py create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/lib/PROVENANCE.md create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/lib/cryptolib.pvl create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/lib/primitives.pvl create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/queries/enrollment.pv create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/queries/enrollment_soundness.pv create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/queries/fetch.pv create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/queries/fetch_unlink.pv create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/queries/reply.pv create mode 100644 securedrop-protocol/protocol-minimal/proofs/proverif/queries/submission.pv diff --git a/.github/workflows/proverif.yml b/.github/workflows/proverif.yml new file mode 100644 index 00000000..2e4821e4 --- /dev/null +++ b/.github/workflows/proverif.yml @@ -0,0 +1,38 @@ +name: proverif + +# Engine-free symbolic-analysis lane: runs ProVerif against the COMMITTED +# extraction snapshot (proofs/proverif/extraction/lib.pvl) plus the vendored +# support libraries. It does NOT build the hax ProVerif backend, so it stays fast +# and portable — only a `proverif` binary is needed. Re-extraction (which needs the +# hax-proverif opam switch) is a manual step: `make proverif-extract`. + +on: [push, pull_request] + +permissions: + contents: read + +jobs: + proverif: + name: ProVerif symbolic model (engine-free) + runs-on: ubuntu-latest + steps: + - name: Check out + uses: actions/checkout@a81bbbf8298c0fa03ea29cdc473d45769f953675 # v4.1.1 + with: + persist-credentials: false + + - name: Set up OCaml (for ProVerif) + uses: ocaml/setup-ocaml@v3 + with: + ocaml-compiler: "5.3" + + - name: Install ProVerif + run: opam install -y proverif + + - name: Verify committed model snapshot (engine-free) + run: opam exec -- python3 proofs/proverif/hax.py reconstruct-proverif + working-directory: securedrop-protocol/protocol-minimal + + - name: Check ProVerif verdicts against committed EXPECTPV + run: opam exec -- make proverif-check + working-directory: securedrop-protocol/protocol-minimal diff --git a/securedrop-protocol/Cargo.toml b/securedrop-protocol/Cargo.toml index cc7fccb4..e652ff5a 100644 --- a/securedrop-protocol/Cargo.toml +++ b/securedrop-protocol/Cargo.toml @@ -19,4 +19,7 @@ authors = ["SecureDrop Team "] license = "GPL-3.0" [workspace.lints.rust] -unexpected_cfgs = { level = "warn", check-cfg = ["cfg(hax)"] } +# `cfg(hax_backend_proverif)` is set only by hax during `cargo hax into proverif` +# (it gates the ProVerif-specific annotations). Normal builds, `cargo test`, and +# `into fstar` never set it, so those lanes strip the gated annotations entirely. +unexpected_cfgs = { level = "warn", check-cfg = ["cfg(hax)", "cfg(hax_backend_proverif)"] } diff --git a/securedrop-protocol/protocol-minimal/Makefile b/securedrop-protocol/protocol-minimal/Makefile index 964ec745..bf7d17c4 100644 --- a/securedrop-protocol/protocol-minimal/Makefile +++ b/securedrop-protocol/protocol-minimal/Makefile @@ -52,6 +52,15 @@ verify: # Internal/CI: Type-check and verify extracted proofs. # Verify: $(MAKE) -C $(PROOF_DIR) ADMIT_MODULES="$(HAX_ADMITS)" all-keep-going +.PHONY: proverif-check +proverif-check: ## Verify the ProVerif (symbolic) model against committed verdicts (engine-free; needs `proverif`). + python3 proofs/proverif/hax.py reconstruct-proverif + python3 proofs/proverif/hax.py check-proverif + +.PHONY: proverif-extract +proverif-extract: ## Re-extract the ProVerif model from Rust (needs the hax-proverif opam switch). + python3 proofs/proverif/hax.py extract-proverif + .PHONY: hax-lib-version hax-lib-version: # Internal: Query Cargo for the hax-lib version. @cargo pkgid hax-lib 2>/dev/null | sed 's/.*@//' diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/PLAN.md b/securedrop-protocol/protocol-minimal/proofs/proverif/PLAN.md new file mode 100644 index 00000000..450eca4b --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/PLAN.md @@ -0,0 +1,393 @@ +# Plan — symbolic (ProVerif) analysis of `securedrop-protocol-minimal` via the hax ProVerif backend + +Status: proposal / not yet executed. Mirrors the SPQR + Mandrake flagship setups +(`~/SparsePostQuantumRatchet/hax.py`, `~/mandrake/hax.py`) on the hax ProVerif +"Backend A" (rust-engine, `cargo hax into proverif`, opam switch `hax-proverif`). + +-------------------------------------------------------------------------------- +## 0. Executive summary — how this works and why it's low-risk + +- The hax ProVerif backend lifts **plain Rust functions** into ProVerif `letfun`s + (one `letfun` per fn, structs → `[data]` constructors). There is **no protocol + DSL to adopt**: the `hax-lib-protocol` state-machine macros exist but the backend + only *parses* them, it does not render processes/events/queries. Every flagship + (PSK, SPQR, Bertie, Mandrake) writes the protocol as ordinary Rust and hand-writes + the ProVerif harness (events, queries, roles, honest run) in `.pv` files that call + the generated letfuns. +- All ProVerif annotations are gated on **`cfg(hax_backend_proverif)`** (set only by + hax during `into proverif`) and the dev `hax-lib` (which carries those macros) is + injected at extraction time via `cargo --config` — **not** a committed + `[patch.crates-io]`. Consequence: `cargo build`, `cargo test`, and the **existing + F\* pipeline are completely untouched.** Normal builds never see the annotations. +- The crate is already well-posed for this: `message.rs`/`metadata.rs`/`sign.rs` + (the SD-APKE / SD-PKE / Ed25519 core) are **loop-free**, and most role/key-setup + functions (`Source::new`, `Journalist::new`, `from_master_key`, …) are already + `#[hax_lib::opaque]`, so the backend won't recurse into their rng/Vec/loop bodies + — we model key setup in the harness instead. + +Pipeline (identical shape to PSK/SPQR/Mandrake): + +``` +cargo hax into -i '' proverif # -> proofs/proverif/extraction/{lib.pvl, missingdecl.pvl, lib.pvl.map} +proverif -lib primitives -lib cryptolib -lib sd_crypto \ + -lib missingdecl -lib lib queries/.pv +``` + +-------------------------------------------------------------------------------- +## 1. Toolchain (already present locally — verify only) + +| Component | Where | Check | +|---|---|---| +| ProVerif 2.05 | `/usr/local/bin/proverif` | `proverif --help \| head -1` | +| hax ProVerif backend | opam switch **`hax-proverif`** (`cargo hax into proverif` present, backend rev `637fc91499`) | `eval $(opam env --switch=hax-proverif); cargo hax into --help \| grep proverif` | +| dev `hax-lib` w/ proverif macros | `~/hax-proverif-backend/hax-lib` (v0.3.7 + `cfg(hax_backend_proverif)` macros) | `ls ~/hax-proverif-backend/hax-lib/proof-libs/proverif/{primitives,cryptolib}.pvl` | +| shared symbolic libs | `~/hax-proverif-backend/hax-lib/proof-libs/proverif/{primitives.pvl, cryptolib.pvl}` | — | + +Set once per shell used for extraction: +```sh +export HAX_PROVERIF_DIR=~/hax-proverif-backend # for primitives.pvl + dev hax-lib path +eval "$(opam env --switch=hax-proverif)" # cargo-hax + hax-rust-engine + hax-engine (ocaml) +``` +No new installs required. (If ProVerif crashes on stats output, apply +`~/hax-proverif-backend/examples/proverif-psk/pv_div_by_zero_fix.diff`.) + +-------------------------------------------------------------------------------- +## 2. Repo scaffolding (new, all under `protocol-minimal/`) + +``` +proofs/proverif/ + PLAN.md # this file + hax.py (NEW) # driver: extract-proverif / reconstruct-proverif / verify-proverif / check-proverif + handwritten/ + sd_crypto.pvl (NEW) # SecureDrop-specific symbolic crypto: SD-APKE (HPKE-AuthPsk) + SD-PKE (HPKE-Base/X-Wing) + queries/ (NEW) # one hand-written .pv per property, each with an (* EXPECTPV … END *) block + submission_secrecy.pv + reply_secrecy.pv + sender_auth.pv + enrollment_auth.pv + sanity.pv + TIMINGS.md + extraction/ (generated) + lib.pvl # pure hax output — committed as a snapshot (reconstruct path), never hand-edited + lib.pvl.sha256 # byte-identity pin + lib.pvl.map # source map (gitignore) + missingdecl.pvl # DIAGNOSTIC — goal: empty (gitignore) +``` + +Reuse verbatim from `~/hax-proverif-backend/hax-lib/proof-libs/proverif/`: +`primitives.pvl` (preamble: channel `c`, tuples, `Some/None/True/False`, `nat_lit`, +`bitstring_err`) and `cryptolib.pvl` (`crypto__aead_enc/dec`, `crypto__kdf`, +`crypto__hkdf_*`, `crypto__dh_pub/shared` + commutativity, `crypto__kem_pk/encaps/decaps`, +`crypto__vk_of/sign/sig_verify`, `crypto__mac*`, `crypto__serialize*`). Referenced by +`-lib` path; not copied. + +`Cargo.toml` edits (crate-local, inert for normal builds): +```toml +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(hax_backend_proverif)'] } +``` +The dev `hax-lib` is **not** added to `[dependencies]`; `hax.py` injects it at +extraction via `cargo --config patch.crates-io."hax-lib".path=$HAX_PROVERIF_DIR/hax-lib` +(+ `hax-lib-macros`, `hax-lib-macros-types`), backing up/restoring `Cargo.lock` around +the run (SPQR pattern). This keeps the committed manifest on crates.io `hax-lib 0.3.7` +so the F\* lane and CI stay portable. + +-------------------------------------------------------------------------------- +## 3. Make the crate ProVerif-extractable (source annotations) + +All annotations are `#[cfg_attr(hax_backend_proverif, hax_lib::…)]` — invisible to +`cargo build`/`test`/`into fstar`. + +### 3a. Crypto boundary — redirect leaves to the symbolic model (`replace_body` / `pv_extern`) + +Annotate at the **SecureDrop-semantic wrapper level** (functions/methods that return +owned values), *not* the raw libcrux `&mut`-out-param level. `replace_body` is allowed +on `impl` methods (SPQR does exactly this). + +| Rust item (crate = `securedrop_protocol_minimal`) | ProVerif redirect | +|---|---| +| `sign::SigningKey::sign(msg) -> Signature` | `crypto__sign(self, msg)` (self = sk) | +| `sign::VerifyingKey::verify(msg, sig) -> Result<(),_>` | `let (=rust_primitives__hax__Tuple0__Tuple0) = crypto__sig_verify(self, msg, sig) in rust_primitives__hax__Tuple0__Tuple0 else bitstring_err()` | +| `sign::tagged_preimage::(msg)` | `crypto__serialize(rust_primitives__hax__Tuple2__Tuple2(D::tag, msg))` (domain-sep tag; see 3d) | +| `primitives::x25519::dh_shared_secret(pk, sk)` | `crypto__dh_shared(sk, pk)` | +| `primitives::x25519::dh_public_key_from_scalar(sk)` / `generate_dh_keypair` | `crypto__dh_pub(sk)` / `new k; (k, crypto__dh_pub(k))` | +| `message::auth_enc(rng, skS, pkR, m, ad, info)` | `sd_apke__authenc(skS, pkR, m, ad, info)` (see §4) | +| `message::auth_dec(skR, pkS, ct, ad, info)` | `sd_apke__authdec(skR, pkS, ct, ad, info)` (partial-inverse `reduc`) | +| `metadata::encrypt(pkR, m) / decrypt(skR, ct)` | `sd_pke__enc(pkR, m)` / `sd_pke__dec(skR, ct)` | +| `primitives::mlkem::*` / `xwing::*` (if reached) | `crypto__kem_encaps/decaps/pk` | + +Redirecting at `auth_enc`/`auth_dec`/`metadata::{encrypt,decrypt}` means the internal +ML-KEM-encaps + HPKE-seal composition is modeled atomically by the `sd_apke`/`sd_pke` +symbolic primitives — the standard symbolic treatment of HPKE. (Phase-2 refinement: +add thin annotatable `provider::hpke::{seal,open}` free-fn wrappers and redirect those +instead, exposing the ML-KEM ⊕ DH-AKEM composition to ProVerif.) + +### 3b. Opaque wire/key types + +`#[cfg_attr(hax_backend_proverif, hax_lib::opaque)]` on the byte-blob structs so they +collapse to atomic `bitstring` (no field-accessor `reduc`s): `Signature`, +`VerifyingKey`, `SigningKey`, `MessageCiphertext`, `MetadataCiphertext`, +`MessagePublicKey`, `MessagePrivateKey`, `MetadataPublicKey/PrivateKey`, `Envelope`, +`Plaintext`, `KeyBundlePublic`, `SignedLongtermPubKeyBytes`, `Enrollment`, +`JournalistLongTermView`, `WelcomeBundle`. (Several already carry `hax_lib::exclude` +on their serde impls — keep those.) + +### 3c. Loops / `Vec` / iterators (backend rejects them) + +Only three call-sites loop; handle each by modeling the honest single-item case: +- `encrypt_decrypt::decrypt_with_sender` — `for &bundle in receiver.keybundles()` trial + decrypt. → `replace_body` to the single-bundle expression, **or** factor a + `decrypt_one(bundle, env)` helper (loop-free) and iterate with `!` replication in the + harness. Phase-1: single keybundle. +- `api::handle_welcome` — `for journalist in welcome.journalists` verify. → extract the + loop-free `verify_long_term` and drive the roster with `!` in the harness. +- `encrypt_decrypt::{compute_fetch_challenges, solve_fetch_challenges}` — fetch-privacy + loops. **Out of phase-1 scope** (fetch/unlinkability is phase-2); exclude via `-i`. + +### 3d. Domain-separated signatures + +`sign::sign/verify` prepend `len(tag)||tag||msg`. Model the four `DomainTag`s +(`j-sig-ltk`, `j-sig-eph`, `nr-sig`, `fpf-sig-nr`) as distinct nullary ProVerif consts +and sign over `crypto__serialize((tag, msg))` (3a). This makes cross-domain confusion +unprovable in the symbolic model, matching the type-level `Signature` separation. + +### 3e. The `-i` target filter (method-precise, SPQR/Mandrake style) + +Start from "exclude all", re-select the protocol roots (their transitive closure pulls +in the crypto leaves, which the redirects cap), keep concrete-crypto/serde/loop trees +out. Draft (tune during M1 against `missingdecl.pvl`): + +``` +-** ++securedrop_protocol_minimal::message::auth_enc ++securedrop_protocol_minimal::message::auth_dec ++securedrop_protocol_minimal::metadata::encrypt ++securedrop_protocol_minimal::metadata::decrypt ++securedrop_protocol_minimal::encrypt_decrypt::encrypt ++securedrop_protocol_minimal::encrypt_decrypt::decrypt_with_sender ++securedrop_protocol_minimal::sign::**::sign ++securedrop_protocol_minimal::sign::**::verify ++securedrop_protocol_minimal::api::**::verify_long_term ++securedrop_protocol_minimal::api::**::verify_ephemeral ++securedrop_protocol_minimal::keys::** +securedrop_protocol_minimal::wire::**::* (types only; prune if they drag serde) +-securedrop_protocol_minimal::storage::** -securedrop_protocol_minimal::server::** +-securedrop_protocol_minimal::**::compute_fetch_challenges +-securedrop_protocol_minimal::**::solve_fetch_challenges +-libcrux_**::** -hpke_rs::** -uuid::** -bip39::** -serde::** -hex::** (concrete crypto / non-protocol) +``` + +-------------------------------------------------------------------------------- +## 4. SecureDrop symbolic crypto extension (`handwritten/sd_crypto.pvl`) + +`cryptolib.pvl` already covers AEAD, KDF/HKDF, DH (+commutativity), KEM, Ed25519 +(EUF-CMA), MAC, serialization. Add only the two SecureDrop composite primitives: + +``` +(* SD-APKE = HPKE(AuthPsk): confidentiality + IMPLICIT SENDER AUTH. + authdec yields the plaintext only for a ct produced by the matching + sender sk_S and recipient pk_R (binds both identities + ad + info). *) +fun sd_apke__authenc(bitstring, bitstring, bitstring, bitstring, bitstring): bitstring. + (* skS, pkR, m, ad, info -> ct *) +reduc forall skS, skR, m, ad, info; + sd_apke__authdec(skR, crypto__dh_pub(skS), + sd_apke__authenc(skS, crypto__dh_pub(skR), m, ad, info), ad, info) = m. + +(* SD-PKE = HPKE(Base) over X-Wing: confidentiality only (metadata). *) +fun sd_pke__enc(bitstring, bitstring): bitstring. (* pkR, m -> ct *) +reduc forall skR, m; + sd_pke__dec(skR, sd_pke__enc(crypto__dh_pub(skR), m)) = m. +``` + +(`crypto__dh_pub` doubles as "public key of sk" for the symbolic identity binding; a +phase-2 decomposition can split DH-AKEM vs ML-KEM PSK if a hybrid-downgrade property is +wanted. Add any per-format serialization tags here too.) These may instead be authored +inline in Rust via `#[hax_lib::proverif::before("…")]` on `auth_enc`/`metadata::encrypt` +(Mandrake style) — pick one home for the model; a standalone `.pvl` keeps it auditable. + +-------------------------------------------------------------------------------- +## 5. Harness — events, queries, roles, honest run (`queries/*.pv`) + +Each query file: `nounif` saturation control (for the crypto-heavy ones) + `event` +decls + `free … [private]` secrets + `query …` + `let` role processes calling the +generated letfuns + `process` honest run + a trailing `(* EXPECTPV … END *)` block. + +Trust model encoded: FPF vk is a public trust anchor; the DY attacker controls the +network and can register rogue journalists; honest source + ≥1 honest journalist. + +Events (declared in the harness, raised inside role processes): +`FpfSignedNewsroom(nr_vk)`, `NewsroomSignedJournalist(j_vk)`, +`SourceSubmitted(msg, j_pk)`, `JournalistReceived(msg, src_pk)`, +`JournalistReplied(reply, src_pk)`, `SourceReceivedReply(reply)`, +`ClientAcceptedJournalist(j_vk)`. + +| # | Property | Query (shape) | Expected | +|---|---|---|---| +| 1 | **Submission confidentiality** | `query attacker(SECRET_SUBMISSION).` | `true` (secret) | +| 2 | **Reply confidentiality** | `query attacker(SECRET_REPLY).` | `true` | +| 3 | **Sender authentication** (SD-APKE implicit) | `event(JournalistReceived(m, s)) ==> event(SourceSubmitted(m, s))` (aim injective) | `true` | +| 4 | **Enrollment trust-chain auth** | `event(ClientAcceptedJournalist(jvk)) ==> event(NewsroomSignedJournalist(jvk))` | `true` (no rogue journalist) | +| 5 | **Sanity / reachability** | `query e:…; event(JournalistReceived(...))` and `event(SourceReceivedReply(...))` | `false` (i.e. reachable — honest run completes) | +| — | *(phase-2)* metadata/sender anonymity of `ct^PKE`; fetch-clue `(X,Z)` recipient unlinkability | observational-equivalence / `choice` | stretch | + +Role sketch (calls generated letfuns; `=securedrop_protocol_minimal`): +``` +let Newsroom(nr_sk, j_vk) = + (* newsroom signs journalist vk *) event NewsroomSignedJournalist(j_vk); + out(c, __sign__…__sign(nr_sk, j_vk)). (* NewsroomOnJournalist sig *) +let Journalist(j_sk, j_apke_sk, j_pke_sk, …) = … receive via __encrypt_decrypt__decrypt_with_sender … reply via __encrypt_decrypt__encrypt … +let Source(src_keys, welcome) = + (* verify chain *) let (=Tuple0) = __api__…__verify_long_term(view, nr_vk) in + event ClientAcceptedJournalist(jvk); + event SourceSubmitted(SECRET_SUBMISSION, j_pk); + out(c, __encrypt_decrypt__encrypt(src_sk, pt, j_pub)). +process new fpf_sk; new nr_sk; ( Newsroom(...) | !Journalist(...) | !Source(...) | attacker-registration ) +``` + +EXPECTPV blocks are generated once by `hax.py check-proverif update`, then asserted. + +-------------------------------------------------------------------------------- +## 6. Driver `proofs/proverif/hax.py` (adapt Mandrake's; SPQR's is the alt template) + +Subcommands (ported ~verbatim; the EXPECTPV machinery, RSS/timing sampler, and target +tiers are reusable as-is): +- `extract-proverif` — `cargo hax into -i '' proverif` with the `cargo --config` + dev-`hax-lib` injection + `Cargo.lock` backup/restore; copy `extraction/lib.pvl`(+`missingdecl.pvl`); + load-check the composed libs against `process 0`; pin `lib.pvl.sha256`. +- `reconstruct-proverif` — reassemble/validate from the committed `extraction/` snapshot + with **no** `cargo hax` (engine-free CI lane). +- `verify-proverif [q…]` — run ProVerif, print `RESULT` lines + wall-clock. +- `check-proverif [update]` — run each `queries/*.pv`, positional diff of `RESULT` lines + vs its `(* EXPECTPV … END *)`; `n/n match [OK|FAIL]`; nonzero exit on mismatch; + `update` regenerates the blocks. + +Fixed `-lib` load order (declare-before-use): +``` +proverif -lib $HAX_PROVERIF_DIR/hax-lib/proof-libs/proverif/primitives.pvl \ + -lib $HAX_PROVERIF_DIR/hax-lib/proof-libs/proverif/cryptolib.pvl \ + -lib handwritten/sd_crypto.pvl \ + -lib extraction/missingdecl.pvl \ + -lib extraction/lib.pvl \ + queries/.pv +``` +Engine discovery: prefer the `hax-proverif` opam switch; honor `HAX_PROVERIF_DIR`. + +-------------------------------------------------------------------------------- +## 7. Milestones (execution order) + +- **M0 — smoke test the toolchain (no crate changes). ✅ DONE.** PSK example verdicts reproduce via the exact `-lib` pipeline. +- **M1 — first extraction of the crypto core. ✅ DONE (2026-07-14).** Added §3a redirects + + §3b opaque to `message.rs` (`auth_enc`/`auth_dec` → `sd_apke__authenc/authdec`), + `metadata.rs` (`encrypt`/`decrypt` → `sd_pke__enc/dec`), `sign.rs` (`sign`/`verify` → + `crypto__sign/sig_verify`); added the `cfg(hax_backend_proverif)` check-cfg to the + workspace; wrote `hax.py` (extract/verify/check-proverif) and `handwritten/sd_crypto.pvl`. + **`missingdecl.pvl` is empty** (all hpke/mlkem/libcrux leaves redirected). The composed + model loads in ProVerif and `submission_secrecy.pv` passes (`attacker(SECRET) is true`). + Non-regression: `cargo build` succeeds; `proofs/fstar/` byte-identical (untouched). + Change footprint: +55 lines across 3 src files + Cargo.toml, all cfg-gated. + **Learnings:** (a) use `opam exec --switch hax-proverif --` to put the OCaml `hax-engine` + on PATH (parsing `opam env` missed its single-quoted output); (b) redirected `letfun`s + KEEP dropped params in their signature — `auth_enc` is `auth_enc(rng, sk, pk, m, ad, info)` + (6 args), so harness/queries must pass a dummy `rng` first. +- **M2 — submission confidentiality + sender auth end-to-end. ✅ DONE (2026-07-14).** + Chose **Approach A (extract the real `encrypt`)** — confirmed `encrypt_decrypt::encrypt` + extracts faithfully (trait methods monomorphize to abstract accessors; the + `decrypt_with_sender` loop even auto-unrolls). Redirected the x25519 DH ops + (`generate_dh_keypair` → `new sk; (sk, crypto__dh_pub(sk))`, `dh_shared_secret` → + `crypto__dh_shared`, DH types opaque + `into_bytes` identity) for the fetch hint; + wrote `handwritten/sd_model.pvl` giving the 5 abstract UserSecret/UserPublic accessors + meaning over honest `sd_secret`/`sd_public` user terms (the SPQR `model.pvl` pattern); + taught `hax.py` to filter `missingdecl.pvl` against handwritten definitions. + `queries/submission.pv` drives the extracted `encrypt` + a primitive-level journalist + receive. **All 3 properties green** (`check-proverif`: 3/3): + 1. `not attacker(SECRET_SUBMISSION) is true` — confidentiality + 3. `JournalistReceived(m,s) ==> SourceSubmitted(m,s) is true` — sender auth + 5. `not event(JournalistReceived) is false` — sanity (non-vacuous) + `missingdecl.pvl` clean; `cargo build` + `proofs/fstar/` untouched. Footprint: +75 src lines. +- **M3 — enrollment trust chain. ✅ DONE (2026-07-14).** The `api::verify_long_term` + blanket-impl doesn't extract (same reason F* excludes `api::**`), so the client + verification is modeled in the harness driving the REAL extracted `sign`/`verify`. + Domain separation (fpf-sig-nr / nr-sig / j-sig-ltk) is modeled by signing/verifying + the tagged message `(TAG, msg)` (mirrors `sign.rs` `tagged_preimage`). `enrollment.pv` + proves **rogue journalist refuted** (`ClientAcceptedJournalist(jvk) ==> + NewsroomSignedJournalist(jvk) is true`) + sanity; `enrollment_soundness.pv` proves the + nr-sig check is load-bearing (a broken client that skips it accepts a rogue — + `... is false`, guarding against a vacuous proof). **Full suite 6/6 green.** No source + changes (pure harness). Reply-path secrecy (property 2) deferred to a follow-up. +- **M4 — CI + snapshots. ✅ DONE (2026-07-14).** Vendored `primitives.pvl`/`cryptolib.pvl` + into `proofs/proverif/lib/` (self-contained + frozen against upstream drift); pinned the + `extraction/lib.pvl` snapshot via `lib.pvl.sha256`; added `hax.py reconstruct-proverif` + (engine-free digest check, drift-detecting) and made `proverif_libs()` prefer the vendored + copies + `proverif` invocation switch-independent. Makefile targets `proverif-check` + (engine-free reconstruct+check) / `proverif-extract`; CI workflow + `.github/workflows/proverif.yml` (installs `proverif` via opam, runs the engine-free lane). + `.gitignore` for `*.pvl.map`. **Verified: `make proverif-check` runs 6/6 green with + `HAX_PROVERIF_DIR` unset** (true CI simulation); drift detection confirmed load-bearing. + +### Follow-ups (post-M4) +- **(a) Reply path. ✅ DONE (2026-07-14).** `queries/reply.pv` drives the extracted + `encrypt` with roles swapped (journalist=sender, source=recipient). Reply confidentiality + + journalist authentication (`SourceReceivedReply(m,j) ==> JournalistReplied(m,j)`) + + sanity all green. **Suite now 9/9.** +- **(c) Fetch-privacy / recipient unlinkability. ✅ DONE (2026-07-14).** `queries/fetch.pv` + (correctness: intended recipient recovers the id; wrong-recipient + eavesdropper secrecy) + and `queries/fetch_unlink.pv` (**recipient anonymity** via ProVerif observational + equivalence — the untrusted server can't tell A from B). **Suite now 13/13.** See + FETCH-NOTES below for the modeling departure. +- **Full `decrypt_with_sender` extraction. ✅ DONE (2026-07-14).** Both receive directions + (submission + reply) now drive the REAL extracted `decrypt_with_sender` — its trial-decrypt + over the key-bundle list, metadata-based sender-key recovery, and `auth_dec` — instead of a + primitive-level harness model. Needed: identity `MessagePublicKey::from_bytes` + + `Plaintext::{to_bytes,from_bytes}` (opaque round-trip); opaque `MessageKeyBundle`/ + `MessageKeyPair`/`MetadataKeyPair` so their bundle machinery lives entirely in `sd_model` + (breaks a lib↔model load-order cycle — ProVerif is single-pass); a receiver model + (`sd_journalist`/`sd_bundle` + `keybundles`/`fetch_keypair` accessors); and a generalized + `missingdecl` filter (also drops names defined by the vendored libs, e.g. reduc-defined + `Tuple2__0/1`). `missingdecl` stays clean; suite still **13/13**. The backend auto-unrolls + the trial-decrypt loop (fixed bound 3; a single-bundle journalist uses the first iteration). +- HPKE-AuthPsk decomposition; migrate `replace_body`→`pv_model` when the tracing backend lands. + +### FETCH-NOTES (the one modeling departure) +Every other property drives the **extracted** Rust. The fetch mechanism is a **3-party DH +clue** (`X=g^x`, `Z=pk_R^x`; server `pmgdh=X^eph`, `mk=Z^eph`; recipient `mk=pmgdh^r_sk`), +i.e. `mk = g^(x·r_sk·eph)`. Two reasons it is modeled by hand rather than extracted: +(1) hax's `crypto__dh_shared` is a 2-party KDF-style op and cannot express the nested +exponentiation; (2) ProVerif does **not terminate** on the general exp-commutativity +equation here. So `fetch*.pv` use dedicated clue constructors (`gen/cluex/cluez/srvp/srvk`) +whose single correctness `reduc` (`reck(srvp(cluex(x),eph), r_sk) = srvk(cluez(gen(r_sk),x),eph)`) +captures exactly the recipient⇄server key agreement — deterministic and fast for ProVerif — +and reuse the shared `crypto__aead_*` for the message-id encryption. A subtle first attempt +had the server as an open oracle re-encrypting one global id onto any hint (a false GotB +"attack"); the fix binds the id to A's genuine entry. Faithfulness caveat: the clue algebra +is hand-modeled, not extracted from `compute_fetch_challenges`/`solve_fetch_challenges`. + +## Verified property inventory (13 RESULT lines, all green — `make proverif-check`) +| File | Property | Verdict | +|---|---|---| +| submission.pv | submission confidentiality / sender auth / sanity | secret / agree / reachable | +| reply.pv | reply confidentiality / journalist auth / sanity | secret / agree / reachable | +| enrollment.pv | rogue journalist refuted / sanity | agree / reachable | +| enrollment_soundness.pv | nr-sig check is load-bearing | attack reproduced (false) | +| fetch.pv | recipient recovers id / wrong-recipient + eavesdropper secrecy | reachable / secret / secret | +| fetch_unlink.pv | recipient anonymity (obs-equivalence) | equivalence true | + +-------------------------------------------------------------------------------- +## 8. Risks / open questions + +- **HPKE-AuthPsk fidelity.** Phase-1 models SD-APKE atomically (§4). It captures + confidentiality + sender-auth but *not* the ML-KEM/DH-AKEM hybrid interior; a + downgrade/KCI property needs the phase-2 decomposition (wrap `hpke.seal/open`). +- **Loop/`Vec`/`Result` handling.** Backend rejects loops/closures/`&mut`; §3c covers + the three sites. Watch for `Result`/`?` and `.expect()` in extracted fns — the PSK + example shows `Result` maps to uniform `bitstring` and failures to `bitstring_err()`, + but confirm per-fn during M1 (may need `replace_body` on a couple of straight-line + wrappers). +- **`missingdecl.pvl` leakage.** Const-eval (e.g. length constants) can leak libcrux + symbols (seen in PSK). Redirect or `pv_stub("nat_lit(0)")` the length helpers; goal = + empty `missingdecl.pvl`. +- **hax-lib rev drift.** The `hax-proverif` switch backend (`637fc91499`) and the dev + `hax-lib` path must be the same build (rust-engine ↔ ocaml-engine version match), else + "ocaml engine crashed". Pin both in `hax.py` and REPRODUCING notes. +- **Trait/generic surface.** `UserSecret`/`UserPublic`/`Api` are generic traits; the + `-i` filter may pull trait machinery. Prefer concretizing roles in the harness and + extracting concrete fns (`encrypt`, `auth_enc`) over trait methods where possible. +``` diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md b/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md new file mode 100644 index 00000000..839c1a02 --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md @@ -0,0 +1,226 @@ +# SecureDrop protocol-minimal — symbolic (ProVerif) verification + +Status report for the hax → ProVerif symbolic security analysis of +`securedrop-protocol-minimal`. This is a **symbolic (Dolev–Yao) analysis**: it proves +protocol-level security properties assuming cryptographic primitives are perfect. It +complements — and is independent of — the F\* track (`proofs/fstar/`, panic-freedom / +functional correctness), which is untouched by this work. + +- **Run it:** `make proverif-check` (engine-free — needs only a `proverif` binary). +- **Re-extract from Rust:** `make proverif-extract` (needs the `hax-proverif` opam switch). +- **Plan / history:** `proofs/proverif/PLAN.md`. + +Result: **13/13 properties verified.** + +--- + +## 1. How it works (one paragraph) + +The hax ProVerif backend lifts the crate's **actual Rust functions** into a ProVerif +model (`extraction/lib.pvl`). Cryptographic leaves are redirected to a shared symbolic +crypto library via source annotations gated on `cfg(hax_backend_proverif)` (invisible to +normal builds, `cargo test`, and F\* extraction). Hand-written ProVerif harnesses +(`queries/*.pv`) instantiate honest participants, an active network attacker, and the +security queries, calling the generated functions. ProVerif then discharges each query. + +--- + +## 2. Verified properties (13 RESULT lines) + +| Layer | File | Property | ProVerif verdict | +|---|---|---|---| +| **Message — submission** | `submission.pv` | Submission **confidentiality** | `not attacker(SECRET_SUBMISSION) is true` | +| | | **Sender authentication** (`JournalistReceived(m,s) ⇒ SourceSubmitted(m,s)`) | `is true` | +| | | Sanity — honest receive reachable | `not event(JournalistReceived) is false` | +| **Message — reply** | `reply.pv` | Reply **confidentiality** | `not attacker(SECRET_REPLY) is true` | +| | | **Journalist authentication** (`SourceReceivedReply(m,j) ⇒ JournalistReplied(m,j)`) | `is true` | +| | | Sanity — honest reply-receive reachable | `not event(SourceReceivedReply) is false` | +| **Enrollment** | `enrollment.pv` | **Rogue journalist refuted** (`ClientAcceptedJournalist(jvk) ⇒ NewsroomSignedJournalist(jvk)`) | `is true` | +| | | Sanity — honest journalist accepted | `not event(ClientAcceptedJournalist) is false` | +| | `enrollment_soundness.pv` | Newsroom-signature check is **load-bearing** (a client that skips it accepts a rogue) | `... ⇒ NewsroomSignedJournalist is false` | +| **Fetch** | `fetch.pv` | Correctness — intended recipient recovers the id | `not event(GotA(MESSAGE_ID)) is false` | +| | | **Wrong-recipient secrecy** — B never recovers A's id | `not event(GotB(MESSAGE_ID)) is true` | +| | | Eavesdropper secrecy of the id | `not attacker(MESSAGE_ID) is true` | +| | `fetch_unlink.pv` | **Recipient anonymity / unlinkability** — server can't tell A from B | `Observational equivalence is true` | + +Interpretation of ProVerif verdicts: +- `not attacker(X) is true` — the attacker can **never** derive `X` (secrecy holds). +- `A ⇒ B is true` — every run reaching `A` also reached `B` (authentication / agreement holds). +- `not event(E) is false` — `E` **is** reachable (a *sanity* check that the honest run + actually runs and the property above is not vacuous). +- `Observational equivalence is true` — the two biprocess sides (message-to-A vs + message-to-B) are indistinguishable to the attacker (unlinkability holds). + +--- + +## 3. Threat model + +- **Network:** a Dolev–Yao attacker fully controls the public channel — it can read, + drop, reorder, replay, and inject arbitrary messages, and derive new terms with any + public operation. +- **Server:** the SecureDrop server is **untrusted**. For fetch, it is modeled as + honest-but-curious (it follows the protocol but tries to learn the recipient); the + network attacker subsumes a fully malicious server for the message-layer properties. +- **Trust anchor:** the FPF signing key is the root of trust. Its public key is public; + its secret key is held by an honest party and only ever signs the honest newsroom. +- **Participants:** an honest source and one or more honest journalists. The attacker may + additionally mint its own journalist key material and attempt to enroll a **rogue + journalist** or inject forged enrollment views. +- **Cryptography:** idealized (perfect) — see §4. + +--- + +## 4. Trust base — what is *assumed* vs. what is *proven* + +The properties in §2 are **proven** by ProVerif **relative to** the following **trusted** +components. A bug or unsound idealization in any trusted component could invalidate a +result. + +### 4a. Trusted: the symbolic cryptographic model (Dolev–Yao idealization) + +These are hand-written and assumed to faithfully idealize the real primitives. Perfect +cryptography is assumed — no computational, algebraic, or side-channel attacks exist +beyond the explicitly modeled equations. + +| File | Idealizes | Assumption | +|---|---|---| +| `lib/primitives.pvl` (vendored) | hax prelude: channel, tuples, options, booleans, machine ints | Standard hax ProVerif prelude | +| `lib/cryptolib.pvl` (vendored) | AEAD, KDF/HKDF, DH (+commutativity), KEM, Ed25519 (EUF-CMA), serialization | Perfect AEAD; one-way KDF/hash; CDH-style DH; unforgeable signatures; injective encodings | +| `handwritten/sd_crypto.pvl` | **SD-APKE** (`sd_apke__authenc/authdec`) and **SD-PKE** (`sd_pke__enc/dec`) | SD-APKE = authenticated PKE binding sender+recipient identity; SD-PKE = confidential PKE. Modeled **atomically** (see §5). | +| `fetch.pv` / `fetch_unlink.pv` (inline) | the 3-party DH fetch clue (`gen/cluex/cluez/srvp/srvk` + `reck`) | Recipient⇄server key agreement; blinding of the recipient key. Hand-modeled (see §5). | + +The vendored `lib/` copies are byte-for-byte from the hax backend +(`hax-lib/proof-libs/proverif/`); see `lib/PROVENANCE.md`. + +### 4b. Trusted: the generated model + the toolchain + +- `extraction/lib.pvl` is **generated by hax** from the annotated Rust. The hax ProVerif + backend is trusted to translate Rust semantics soundly. **Caveat:** this backend is a + work-in-progress (it prints `Experimental backend "proverif" is work in progress`) and + is not yet upstream — see the pins in §6. +- Each `#[hax_lib::proverif::replace_body(...)]` annotation is an **assumed** claim that + the Rust body equals the given symbolic term (an impl≈model assumption). These are the + interface between real code and the trusted crypto model; they are listed in §5b. +- `extraction/lib.pvl.sha256` pins the generated model so drift is detected + (`reconstruct-proverif`); the committed `lib.pvl` is what the engine-free lane checks. + +### 4c. Trusted: the hand-written harness + +- `handwritten/sd_model.pvl` — the honest-participant model: how a source/journalist's + keys relate (`sd_secret`, `sd_public`, `sd_journalist`, the key-bundle model), and the + trait-accessor meanings the extracted generic code calls. Assumed to model honest + participants faithfully. +- `queries/*.pv` — the roles, events, top-level runs, and the security queries + themselves. A mis-stated query proves the wrong thing; the *sanity* rows in §2 guard + against vacuity, and `enrollment_soundness.pv` guards against a vacuous enrollment proof. + +### 4d. Proven (the deliverable) + +Given 4a–4c, ProVerif proves the §2 properties hold against the §3 attacker. + +--- + +## 5. Modeling assumptions & caveats + +### 5a. Fidelity: what is extracted vs. hand-modeled + +**Extracted from the real Rust** (the substance of the analysis): +`message::{auth_enc,auth_dec}`, `metadata::{encrypt,decrypt}`, `sign`/`verify`, +`encrypt_decrypt::encrypt`, **`encrypt_decrypt::decrypt_with_sender`** (the full receive: +trial-decrypt over the key-bundle list → recover the sender key from metadata → +`auth_dec`), the x25519 DH operations, `Plaintext` (de)serialization, and the key / +ciphertext / envelope types. + +**Hand-modeled in the harness** (participants and scenarios, not crypto/protocol logic): +the honest-user key model and trait accessors; the role processes, events, and queries; +the enrollment **process wiring** and domain-separation tags (the `sign`/`verify` calls +themselves are extracted); and — the one substantive departure — the **fetch DH clue**. + +### 5b. Specific assumptions + +1. **SD-APKE is modeled atomically.** HPKE-AuthPsk = DH-AKEM (sender auth) ⊕ ML-KEM (PSK) + is a single symbolic primitive that captures confidentiality + sender authentication. + The internal hybrid is *not* decomposed, so a downgrade/KCI property that depends on + the ML-KEM vs DH-AKEM split is out of scope. (Follow-up in `PLAN.md`.) +2. **The fetch clue uses an idealized 3-party Diffie–Hellman model — this is the + weakest-assumption part of the analysis.** The clue derives a shared key by nested + exponentiation, `mk = g^(x·r_sk·eph)` (source ephemeral `x`, recipient fetch secret + `r_sk`, server per-request `eph`). Two facts force a hand-written model rather than an + extracted one: + - hax's `crypto__dh_shared` is a **2-party** operation (`g^(a·b)` with a single + commutativity equation) and structurally cannot express a 3-fold product. + - Modeling real DH faithfully needs the general exponent-commutativity **equation** + `exp(exp(b,x),y) = exp(exp(b,y),x)`; ProVerif **does not terminate** on it here + (its equational saturation diverges). So under the faithful DH theory, ProVerif + could not *decide* the fetch properties at all. + + `fetch.pv`/`fetch_unlink.pv` therefore replace DH with **dedicated constructors** + (`gen`, `cluex`, `cluez`, `srvp`, `srvk`) and a **single `reduc`**, + `reck(srvp(cluex(x),eph), r_sk) = srvk(cluez(gen(r_sk),x), eph)`, that asserts *only* + the intended recipient⇄server key agreement. **What this abstraction does NOT capture:** + - the **algebraic / homomorphic structure** of exponentiation — products, inverses, + re-blinding/re-randomization of group elements, exponent cancellation, small-subgroup + or invalid-curve behaviour. The attacker in this model can only combine clue terms + through the one `reck` rule, not manipulate them as real group elements. + - consequently the **recipient-unlinkability** (observational-equivalence) result is a + symbolic **assumption of DDH-like indistinguishability**, not a derivation of it: it + shows the honest constructors do not *syntactically* leak the recipient, but it does + **not** rule out an attacker who exploits DH's multiplicative structure. A sound + unlinkability guarantee would require a **computational** DDH argument, or a validated + ProVerif equational theory (which, per the non-termination above, we could not run). + + Net: the fetch results are **relative to this idealized clue algebra**, which is a + stronger and less-audited assumption than the standard `cryptolib` primitives used for + the message and enrollment layers. The clue algebra is *trusted*, not derived from + `compute_fetch_challenges`/`solve_fetch_challenges` (which are also not extracted). +3. **Domain-separated signatures are modeled harness-side.** The four Ed25519 domains + (`fpf-sig-nr`, `nr-sig`, `j-sig-ltk`, `j-sig-eph`) are represented by signing/verifying + a tagged message `(TAG, msg)`, mirroring the code's `len(tag)‖tag‖msg` preimage, rather + than deriving the tags from the `DomainTag` impls. +4. **Serialization is abstracted to identity** for the atomic-key/plaintext types + (`MessagePublicKey::from_bytes`, `Plaintext::{to,from}_bytes`): the byte layout is not + modeled; round-trip is exact. Length/format-confusion attacks are therefore out of + scope. +5. **Bounded honest topology.** Scenarios use one honest source and one honest journalist + with a **single** ephemeral key bundle (the backend unrolls the trial-decrypt loop to a + fixed bound of 3; a single-bundle journalist uses the first iteration). The attacker is + unbounded (replicated), but multi-bundle / multi-journalist honest topologies are not + exhaustively modeled. +6. **`api::verify_long_term`/`verify_ephemeral` are not extracted.** They are blanket-impl + trait methods (`impl Api for T`) that hax cannot extract (the same reason F\* + excludes `api::**`). The client's verification *composition* is written in the harness, + but every signature check it performs is the **extracted** `verify`. + +### 5c. Out of scope + +Computational security (this is symbolic); **algebraic attacks on the fetch +Diffie–Hellman clue** (the 3-party DH is idealized to a single agreement rule, not real +exponentiation — see §5b.2); timing/side channels and traffic analysis beyond the +recipient-unlinkability result; forward secrecy / post-compromise security (keys are +static here); injective agreement / replay protection (only non-injective agreement is +proven); sender-anonymity of the metadata ciphertext beyond recipient unlinkability; and +functional correctness / panic-freedom (the F\* track). + +--- + +## 6. Reproducibility & pins + +- **ProVerif** — any recent 2.0x (developed against the `hax-proverif` opam switch's build). +- **hax ProVerif backend** — the `hax-proverif` opam switch / a `~/hax-proverif-backend` + checkout (draft PR cryspen/hax#2068). Only needed to **re-extract** (`make + proverif-extract`); the engine-free `make proverif-check` needs only `proverif`. +- **`hax-lib`** — crates.io `0.3.7` for normal builds; the dev `hax-lib` (with the + `cfg(hax_backend_proverif)`-gated macros) is injected at extraction time via + `cargo --config`, never as a committed patch, so `cargo build` / CI / F\* are unaffected. +- **CI** — `.github/workflows/proverif.yml` runs the engine-free lane on every push. + +## 7. Integrity guarantees of this change + +- `cargo build` and `cargo test` are unaffected (all annotations are + `cfg(hax_backend_proverif)`-gated). +- **`proofs/fstar/` is byte-identical** — the F\* extraction and verification pipeline is + untouched. +- Source changes are ~80 cfg-gated lines across `message.rs`, `metadata.rs`, `sign.rs`, + `ciphertext.rs`, `keys.rs`, `primitives/x25519.rs`, plus the workspace `Cargo.toml` + lint and the crate `Makefile` targets. Everything else is new files under + `proofs/proverif/`. diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/.gitignore b/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/.gitignore new file mode 100644 index 00000000..91b41269 --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/.gitignore @@ -0,0 +1,2 @@ +# Generated source map — diagnostic only, not part of the committed model. +*.pvl.map diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl b/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl new file mode 100644 index 00000000..cf8f94fd --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl @@ -0,0 +1,319 @@ +(* + Run with: + proverif -lib /hax-lib/proof-libs/proverif/primitives.pvl lib.pvl + + The `primitives.pvl` library ships with hax and supplies + everything the extracted file references that isn't defined + below: the public channel `c`, the `construct_fail` sink, + `bitstring_default`/`bitstring_err`, the `Some`/`None`/ + `True`/`False`/`nat_lit` constructors, `logical_and`/`or`, and + every `rust_primitives::*` / `core::*` / `hax_lib::*` opaque + function the extraction surface needs. + + Any symbol this file references but does NOT define, and that is + not in `primitives.pvl`, is listed in the companion + `missingdecl.pvl`. That file is a DIAGNOSTIC, not part of the + model: each entry must be supplied by hand or by another crate's + extraction (e.g. a separately-extracted dependency). The goal is + for `missingdecl.pvl` to be EMPTY — anything in it is a reachable + definition that was silently stubbed out. +*) + + + + +(* src: protocol-minimal/src/message.rs:93 securedrop_protocol_minimal__message__Impl__private_key *) +(* Returns the private key. *) +letfun securedrop_protocol_minimal__message__Impl__private_key(self: bitstring) = + securedrop_protocol_minimal__message__MessageKeyPair__MessageKeyPair__sk(self). +(* src: protocol-minimal/src/message.rs:113 securedrop_protocol_minimal__message__Impl_1__from_bytes *) +(* Deserialize from `pk1 || pk2` bytes. *) +(* *) +(* # Errors *) +(* *) +(* Returns an error if the byte slice has incorrect length. *) +letfun securedrop_protocol_minimal__message__Impl_1__from_bytes(bytes: bitstring) = bytes. + +(* src: protocol-minimal/src/message.rs:280 securedrop_protocol_minimal__message__auth_enc *) +(* SD-APKE.AuthEnc: encrypt message `m` from sender to recipient. *) +(* *) +(* - `sk = (skS1, skS2)`: sender\'s SD-APKE private key *) +(* - `pk = (pkR1, pkR2)`: recipient\'s SD-APKE public key *) +(* - `ad`: associated data *) +(* - `info`: caller-supplied info (spec prepends `c2` internally: `info = c2 + info`) *) +(* *) +(* # Errors *) +(* *) +(* Returns an error if ML-KEM encapsulation or HPKE sealing fails. *) +letfun securedrop_protocol_minimal__message__auth_enc( + rng: bitstring, + sk: bitstring, + pk: bitstring, + m: bitstring, + ad: bitstring, + info: bitstring +) = + let hax_temp_output = (sd_apke__authenc(sk, pk, m, ad, info)) in + rust_primitives__hax__Tuple2__Tuple2(rng, hax_temp_output). +(* src: protocol-minimal/src/message.rs:343 securedrop_protocol_minimal__message__auth_dec *) +(* SD-APKE.AuthDec: decrypt ciphertext from sender. *) +(* *) +(* - `sk = (skR1, skR2)`: recipient\'s SD-APKE private key *) +(* - `pk = (pkS1, pkS2)`: sender\'s SD-APKE public key *) +(* - `ad`: associated data *) +(* - `info`: caller-supplied info (spec prepends `c2` internally: `info = c2 + info`) *) +(* *) +(* # Errors *) +(* *) +(* Returns an error if ML-KEM decapsulation or HPKE opening fails. *) +letfun securedrop_protocol_minimal__message__auth_dec( + sk: bitstring, + pk: bitstring, + ct: bitstring, + ad: bitstring, + info: bitstring +) = sd_apke__authdec(sk, pk, ct, ad, info). + + + +(* src: protocol-minimal/src/metadata.rs:60 securedrop_protocol_minimal__metadata__Impl__private_key *) +(* Returns the private key. *) +letfun securedrop_protocol_minimal__metadata__Impl__private_key(self: bitstring) = + securedrop_protocol_minimal__metadata__MetadataKeyPair__MetadataKeyPair__sk(self). + +(* src: protocol-minimal/src/metadata.rs:238 securedrop_protocol_minimal__metadata__encrypt *) +(* SD-PKE.Enc: encrypt message `m` to recipient key `pk_r`, returning `(c, c\')`. *) +(* *) +(* `m` is the sender\'s long-term APKE public key, which must be serializable. *) +letfun securedrop_protocol_minimal__metadata__encrypt(pk_r: bitstring, m: bitstring) = + sd_pke__enc(pk_r, m). +(* src: protocol-minimal/src/metadata.rs:276 securedrop_protocol_minimal__metadata__decrypt *) +(* SD-PKE.Dec: decrypt `(c, c\')` using recipient key `sk_r`, returning message `m`. *) +(* *) +(* # Errors *) +(* *) +(* Returns an error if HPKE decryption fails. *) +letfun securedrop_protocol_minimal__metadata__decrypt(sk_r: bitstring, ct: bitstring) = + sd_pke__dec(sk_r, ct). + +(* src: protocol-minimal/src/primitives/x25519.rs:20 securedrop_protocol_minimal__primitives__x25519__Impl__into_bytes *) +letfun securedrop_protocol_minimal__primitives__x25519__Impl__into_bytes(self: bitstring) = self. + +(* src: protocol-minimal/src/primitives/x25519.rs:58 securedrop_protocol_minimal__primitives__x25519__Impl_1__into_bytes *) +letfun securedrop_protocol_minimal__primitives__x25519__Impl_1__into_bytes(self: bitstring) = self. + +(* src: protocol-minimal/src/primitives/x25519.rs:74 securedrop_protocol_minimal__primitives__x25519__Impl_2__into_bytes *) +letfun securedrop_protocol_minimal__primitives__x25519__Impl_2__into_bytes(self: bitstring) = self. +(* src: protocol-minimal/src/primitives/x25519.rs:100 securedrop_protocol_minimal__primitives__x25519__generate_dh_keypair *) +(* Generate a new DH key pair using X25519 *) +letfun securedrop_protocol_minimal__primitives__x25519__generate_dh_keypair(rng: bitstring) = + let hax_temp_output = (new x25519_sk: bitstring; rust_primitives__hax__Tuple2__Tuple2(x25519_sk, crypto__dh_pub(x25519_sk))) in + rust_primitives__hax__Tuple2__Tuple2(rng, hax_temp_output). +(* src: protocol-minimal/src/primitives/x25519.rs:161 securedrop_protocol_minimal__primitives__x25519__dh_shared_secret *) +(* Compute DH shared secret *) +letfun securedrop_protocol_minimal__primitives__x25519__dh_shared_secret( + public_key: bitstring, + private_scalar: bitstring +) = crypto__dh_shared(private_scalar, public_key). +(* src: protocol-minimal/src/ciphertext.rs:44 securedrop_protocol_minimal__ciphertext__Envelope *) +(* The full submission `(C_S, X, Z)` sent from sender to server in step 6. *) +(* *) +(* - `C_S = (ct^APKE, ct^PKE)`: the two ciphertexts *) +(* - `X = g^x`: ephemeral DH public key (hint) *) +(* - `Z = (pk_R^fetch)^x`: DH share for fetching (hint) *) +(* *) +(* The server stores `(id, C_S, X, Z)` per message. *) +fun securedrop_protocol_minimal__ciphertext__Envelope__Envelope( + bitstring, + bitstring, + bitstring, + bitstring +): bitstring [data]. +reduc forall v_0: bitstring, v_1: bitstring, v_2: bitstring, v_3: bitstring; + securedrop_protocol_minimal__ciphertext__Envelope__Envelope__ct_apke( + securedrop_protocol_minimal__ciphertext__Envelope__Envelope(v_0, v_1, v_2, v_3) + ) = v_0. +reduc forall v_0: bitstring, v_1: bitstring, v_2: bitstring, v_3: bitstring; + securedrop_protocol_minimal__ciphertext__Envelope__Envelope__ct_pke( + securedrop_protocol_minimal__ciphertext__Envelope__Envelope(v_0, v_1, v_2, v_3) + ) = v_1. +reduc forall v_0: bitstring, v_1: bitstring, v_2: bitstring, v_3: bitstring; + securedrop_protocol_minimal__ciphertext__Envelope__Envelope__mgdh_pubkey( + securedrop_protocol_minimal__ciphertext__Envelope__Envelope(v_0, v_1, v_2, v_3) + ) = v_2. +reduc forall v_0: bitstring, v_1: bitstring, v_2: bitstring, v_3: bitstring; + securedrop_protocol_minimal__ciphertext__Envelope__Envelope__mgdh( + securedrop_protocol_minimal__ciphertext__Envelope__Envelope(v_0, v_1, v_2, v_3) + ) = v_3. +(* src: protocol-minimal/src/ciphertext.rs:78 securedrop_protocol_minimal__ciphertext__Plaintext *) +(* Toy pt structure - TODO: provide params in correct order *) +fun securedrop_protocol_minimal__ciphertext__Plaintext__Plaintext( + bitstring, + bitstring, + bitstring +): bitstring [data]. +reduc forall v_0: bitstring, v_1: bitstring, v_2: bitstring; + securedrop_protocol_minimal__ciphertext__Plaintext__Plaintext__sender_reply_pubkey_hybrid( + securedrop_protocol_minimal__ciphertext__Plaintext__Plaintext(v_0, v_1, v_2) + ) = v_0. +reduc forall v_0: bitstring, v_1: bitstring, v_2: bitstring; + securedrop_protocol_minimal__ciphertext__Plaintext__Plaintext__sender_fetch_key( + securedrop_protocol_minimal__ciphertext__Plaintext__Plaintext(v_0, v_1, v_2) + ) = v_1. +reduc forall v_0: bitstring, v_1: bitstring, v_2: bitstring; + securedrop_protocol_minimal__ciphertext__Plaintext__Plaintext__msg( + securedrop_protocol_minimal__ciphertext__Plaintext__Plaintext(v_0, v_1, v_2) + ) = v_2. +(* src: protocol-minimal/src/ciphertext.rs:90 securedrop_protocol_minimal__ciphertext__Impl_1__to_bytes *) +letfun securedrop_protocol_minimal__ciphertext__Impl_1__to_bytes(self: bitstring) = self. +(* src: protocol-minimal/src/ciphertext.rs:107 securedrop_protocol_minimal__ciphertext__Impl_1__from_bytes *) +letfun securedrop_protocol_minimal__ciphertext__Impl_1__from_bytes(pt_bytes: bitstring) = pt_bytes. + + + + + + + +(* src: protocol-minimal/src/sign.rs:244 securedrop_protocol_minimal__sign__Impl_10__sign *) +(* Sign `msg` in domain `D`, returning a `Signature`. *) +(* *) +(* The actual preimage is `len(tag) || tag || msg` where `tag = D::TAG`. *) +letfun securedrop_protocol_minimal__sign__Impl_10__sign(self: bitstring, msg: bitstring) = + crypto__sign(self, msg). +(* src: protocol-minimal/src/sign.rs:279 securedrop_protocol_minimal__sign__Impl_11__verify *) +(* Verify `sig` over `msg`. The domain is determined by the type of `sig`. *) +(* *) +(* Returns an error if the signature is invalid. *) +letfun securedrop_protocol_minimal__sign__Impl_11__verify( + self: bitstring, + msg: bitstring, + sig: bitstring +) = crypto__sig_verify(self, msg, sig). +(* src: protocol-minimal/src/encrypt_decrypt.rs:16 securedrop_protocol_minimal__encrypt_decrypt__NR_ID *) +const securedrop_protocol_minimal__encrypt_decrypt__NR_ID: bitstring. +(* src: protocol-minimal/src/encrypt_decrypt.rs:25 securedrop_protocol_minimal__encrypt_decrypt__encrypt *) +(* Encrypt a message from a sender to a recipient (step 6). *) +(* *) +(* Produces an [`Envelope`] containing: *) +(* - `ct^APKE`: SD-APKE ciphertext (encrypted message) *) +(* - `ct^PKE`: SD-PKE ciphertext (encrypted sender APKE public key) *) +(* - `(X, Z)`: hint for privacy-preserving message fetching *) +letfun securedrop_protocol_minimal__encrypt_decrypt__encrypt( + rng: bitstring, + sender: bitstring, + plaintext: bitstring, + recipient: bitstring +) = + let rust_primitives__hax__Tuple2__Tuple2( + tmp0: bitstring, + out_kw: bitstring + ) = securedrop_protocol_minimal__message__auth_enc( + rng, + securedrop_protocol_minimal__traits__UserSecret__message_auth_key(sender), + securedrop_protocol_minimal__traits__UserPublic__message_enc_pk(recipient), + securedrop_protocol_minimal__ciphertext__Impl_1__to_bytes(plaintext), + securedrop_protocol_minimal__encrypt_decrypt__NR_ID, + securedrop_protocol_minimal__primitives__x25519__Impl__into_bytes( + securedrop_protocol_minimal__traits__UserPublic__fetch_pk(recipient) + ) + ) in (let rust_primitives__hax__Tuple2__Tuple2( + tmp0_1: bitstring, + out_kw_1: bitstring + ) = securedrop_protocol_minimal__primitives__x25519__generate_dh_keypair( + tmp0 + ) in (let rust_primitives__hax__Tuple2__Tuple2( + hint_esk: bitstring, + hint_epk: bitstring + ) = core__result__Impl__expect( + out_kw_1, + string_lit__DH_x20Keygen_x20_x28hint_x29_x20failed + ) in rust_primitives__hax__Tuple2__Tuple2( + tmp0_1, + securedrop_protocol_minimal__ciphertext__Envelope__Envelope( + core__result__Impl__expect(out_kw, string_lit__SD_x2dAPKE_x20AuthEnc_x20failed), + core__result__Impl__expect( + securedrop_protocol_minimal__metadata__encrypt( + securedrop_protocol_minimal__traits__UserPublic__message_metadata_pk(recipient), + securedrop_protocol_minimal__traits__UserSecret__own_message_auth_pk(sender) + ), + string_lit__Valid_x20Keybundle_x20should_x20allow_x20metadata_x20seal + ), + securedrop_protocol_minimal__primitives__x25519__Impl__into_bytes(hint_epk), + securedrop_protocol_minimal__primitives__x25519__Impl_2__into_bytes( + core__result__Impl__expect( + securedrop_protocol_minimal__primitives__x25519__dh_shared_secret( + securedrop_protocol_minimal__traits__UserPublic__fetch_pk(recipient), + securedrop_protocol_minimal__primitives__x25519__Impl_1__into_bytes(hint_esk) + ), + string_lit__Failed_x20to_x20generate_x20shared_x20secret + ) + ) + ) + ) else bitstring_err()) else bitstring_err()) else bitstring_err(). +(* src: protocol-minimal/src/encrypt_decrypt.rs:81 securedrop_protocol_minimal__encrypt_decrypt__decrypt_with_sender *) +(* Decrypt like [`decrypt`], additionally returning the sender's long-term *) +(* SD-APKE public key `pk_S^APKE` recovered from `ct^PKE`. *) +letfun securedrop_protocol_minimal__encrypt_decrypt__decrypt_with_sender( + receiver: bitstring, + envelope: bitstring +) = + let found = None() in + let found_3 = ((let bl__seq0 = (core__iter__traits__collect__IntoIterator__into_iter( + core__slice__Impl__iter(securedrop_protocol_minimal__traits__UserSecret__keybundles(receiver)) + )) in let bl__acc0 = (found) in + let rust_primitives__hax__array_cons(bundle, bl__seq1) = bl__seq0 in (let found_1 = bl__acc0 in + let bl__acc1 = (let m = securedrop_protocol_minimal__metadata__decrypt( + securedrop_protocol_minimal__metadata__Impl__private_key( + securedrop_protocol_minimal__keys__MessageKeyBundle__MessageKeyBundle__metadata_kp(bundle) + ), + securedrop_protocol_minimal__ciphertext__Envelope__Envelope__ct_pke(envelope) + ) in Some(rust_primitives__hax__Tuple2__Tuple2(bundle, m))) in + let rust_primitives__hax__array_cons(bundle, bl__seq2) = bl__seq1 in (let found_1 = bl__acc1 in + let bl__acc2 = (let m = securedrop_protocol_minimal__metadata__decrypt( + securedrop_protocol_minimal__metadata__Impl__private_key( + securedrop_protocol_minimal__keys__MessageKeyBundle__MessageKeyBundle__metadata_kp(bundle) + ), + securedrop_protocol_minimal__ciphertext__Envelope__Envelope__ct_pke(envelope) + ) in Some(rust_primitives__hax__Tuple2__Tuple2(bundle, m))) in + let rust_primitives__hax__array_cons(bundle, bl__seq3) = bl__seq2 in (let found_1 = bl__acc2 in + let bl__acc3 = (let m = securedrop_protocol_minimal__metadata__decrypt( + securedrop_protocol_minimal__metadata__Impl__private_key( + securedrop_protocol_minimal__keys__MessageKeyBundle__MessageKeyBundle__metadata_kp(bundle) + ), + securedrop_protocol_minimal__ciphertext__Envelope__Envelope__ct_pke(envelope) + ) in Some(rust_primitives__hax__Tuple2__Tuple2(bundle, m))) in + let rust_primitives__hax__array_cons(bl__xh, bl__xt) = bl__seq3 in bitstring_err() else (bl__acc3)) else (bl__acc2)) else (bl__acc1)) else (bl__acc0))) in + let rust_primitives__hax__Tuple2__Tuple2( + bundle_1: bitstring, + raw_metadata: bitstring + ) = core__option__Impl__expect( + found_3, + string_lit__we_x20should_x20find_x20exactly_x201_x20result + ) in (let sender_pk = core__result__Impl__expect( + securedrop_protocol_minimal__message__Impl_1__from_bytes(raw_metadata), + string_lit__Metadata_x20must_x20contain_x20valid_x20sender_x20APKE_x20key_x20tuple + ) in + rust_primitives__hax__Tuple2__Tuple2( + core__result__Impl__unwrap( + securedrop_protocol_minimal__ciphertext__Impl_1__from_bytes( + core__result__Impl__expect( + securedrop_protocol_minimal__message__auth_dec( + securedrop_protocol_minimal__message__Impl__private_key( + securedrop_protocol_minimal__keys__MessageKeyBundle__MessageKeyBundle__apke(bundle_1) + ), + sender_pk, + securedrop_protocol_minimal__ciphertext__Envelope__Envelope__ct_apke(envelope), + securedrop_protocol_minimal__encrypt_decrypt__NR_ID, + securedrop_protocol_minimal__primitives__x25519__Impl__into_bytes( + rust_primitives__hax__Tuple2__Tuple2__1( + securedrop_protocol_minimal__traits__UserSecret__fetch_keypair(receiver) + ) + ) + ), + string_lit__SD_x2dAPKE_x20AuthDec_x20failed + ) + ) + ), + sender_pk + )) else bitstring_err(). \ No newline at end of file diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl.sha256 b/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl.sha256 new file mode 100644 index 00000000..5f25af65 --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl.sha256 @@ -0,0 +1 @@ +ae2bb600c8192292fd769e5c9d1fd49691715ffe9f2044cb3238eb7a64ea6edb lib.pvl diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/missingdecl.pvl b/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/missingdecl.pvl new file mode 100644 index 00000000..b67a5032 --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/missingdecl.pvl @@ -0,0 +1,18 @@ +(*****************************************************************) +(* missingdecl.pvl — UNDEFINED externals referenced by lib.pvl *) +(* *) +(* DIAGNOSTIC, not part of the model. Each symbol below is *) +(* referenced by lib.pvl but has no definition (and is not in *) +(* primitives.pvl). Supply a real one by hand, or by extracting *) +(* the crate that owns it (e.g. a separately-extracted *) +(* dependency). Declared WITHOUT `[data]` because the real *) +(* nature (one-way fun / data constructor / letfun) is unknown. *) +(* GOAL: this file is EMPTY. *) +(*****************************************************************) +const string_lit__DH_x20Keygen_x20_x28hint_x29_x20failed: bitstring. +const string_lit__Failed_x20to_x20generate_x20shared_x20secret: bitstring. +const string_lit__Metadata_x20must_x20contain_x20valid_x20sender_x20APKE_x20key_x20tuple: bitstring. +const string_lit__SD_x2dAPKE_x20AuthDec_x20failed: bitstring. +const string_lit__SD_x2dAPKE_x20AuthEnc_x20failed: bitstring. +const string_lit__Valid_x20Keybundle_x20should_x20allow_x20metadata_x20seal: bitstring. +const string_lit__we_x20should_x20find_x20exactly_x201_x20result: bitstring. diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/handwritten/sd_crypto.pvl b/securedrop-protocol/protocol-minimal/proofs/proverif/handwritten/sd_crypto.pvl new file mode 100644 index 00000000..4cab0ce3 --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/handwritten/sd_crypto.pvl @@ -0,0 +1,48 @@ +(*****************************************************************) +(* sd_crypto.pvl — SecureDrop-specific symbolic crypto *) +(* *) +(* Composite primitives the generic cryptolib.pvl does not *) +(* cover. Load AFTER primitives.pvl + cryptolib.pvl: *) +(* proverif -lib primitives -lib cryptolib -lib sd_crypto \ *) +(* -lib missingdecl -lib lib queries/.pv *) +(* *) +(* Uniform `bitstring` model (no `type` decls) so names resolve *) +(* directly against the extracted lib.pvl. *) +(*****************************************************************) + +(*===============================================================*) +(* SD-APKE — SecureDrop Authenticated PKE. *) +(* HPKE(AuthPsk) = DH-AKEM (sender authentication) + ML-KEM PSK. *) +(* Modeled atomically: confidentiality + IMPLICIT SENDER AUTH. *) +(* *) +(* sd_apke__pk(sk) : APKE public key of sk *) +(* sd_apke__authenc(skS,pkR,m,ad,info) -> ct *) +(* sd_apke__authdec(skR,pkS,ct,ad,info) -> m (partial) *) +(* *) +(* authdec yields m ONLY for a ct produced by the matching *) +(* sender skS (whose public key pkS = sd_apke__pk(skS)) and *) +(* recipient (whose public key was sd_apke__pk(skR)). The *) +(* ciphertext term carries skS as a subterm, so a recipient *) +(* holding skR + the public pkS can open it, but neither *) +(* confidentiality (needs skR) nor authenticity (needs skS to *) +(* forge) can be broken by the Dolev-Yao attacker. *) +(*===============================================================*) +fun sd_apke__pk(bitstring): bitstring. +fun sd_apke__authenc(bitstring, bitstring, bitstring, bitstring, bitstring): bitstring. + (* skS, pkR, m, ad, info -> ct *) +reduc forall skS: bitstring, skR: bitstring, m: bitstring, ad: bitstring, info: bitstring; + sd_apke__authdec(skR, sd_apke__pk(skS), + sd_apke__authenc(skS, sd_apke__pk(skR), m, ad, info), + ad, info) = m. + +(*===============================================================*) +(* SD-PKE — SecureDrop metadata PKE. *) +(* HPKE(Base) over X-Wing. Confidentiality only (no sender auth). *) +(* sd_pke__pk(sk) : metadata public key of sk *) +(* sd_pke__enc(pkR, m) -> ct *) +(* sd_pke__dec(skR, ct) -> m (partial inverse) *) +(*===============================================================*) +fun sd_pke__pk(bitstring): bitstring. +fun sd_pke__enc(bitstring, bitstring): bitstring. (* pkR, m -> ct *) +reduc forall skR: bitstring, m: bitstring; + sd_pke__dec(skR, sd_pke__enc(sd_pke__pk(skR), m)) = m. diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/handwritten/sd_model.pvl b/securedrop-protocol/protocol-minimal/proofs/proverif/handwritten/sd_model.pvl new file mode 100644 index 00000000..a48e7be7 --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/handwritten/sd_model.pvl @@ -0,0 +1,58 @@ +(*****************************************************************) +(* sd_model.pvl — honest-user model for the extracted protocol *) +(* *) +(* `encrypt_decrypt::encrypt` is generic over UserSecret / *) +(* UserPublic, so hax extracts its key accessors as abstract *) +(* functions. Here we give them meaning over concrete honest *) +(* user terms — a user IS its bundle of keys (the SPQR model.pvl *) +(* pattern). Load AFTER sd_crypto.pvl, BEFORE lib.pvl. *) +(* *) +(* A source (UserSecret) carries (skApke, skFetch, skMeta). *) +(* A recipient view (UserPublic) carries the public keys the *) +(* sender needs: the EPHEMERAL apke enc key, the fetch key, and *) +(* the metadata key. *) +(*****************************************************************) + +(* Secret user: long-term/ephemeral secret keys. *) +fun sd_secret(bitstring, bitstring, bitstring): bitstring [data]. (* skApke, skFetch, skMeta *) +reduc forall a: bitstring, f: bitstring, m: bitstring; + securedrop_protocol_minimal__traits__UserSecret__message_auth_key(sd_secret(a, f, m)) = a. +reduc forall a: bitstring, f: bitstring, m: bitstring; + securedrop_protocol_minimal__traits__UserSecret__own_message_auth_pk(sd_secret(a, f, m)) = sd_apke__pk(a). + +(* Public recipient view: (message_enc_pk, fetch_pk, metadata_pk). *) +fun sd_public(bitstring, bitstring, bitstring): bitstring [data]. (* pkEnc, pkFetch, pkMeta *) +reduc forall pe: bitstring, pf: bitstring, pm: bitstring; + securedrop_protocol_minimal__traits__UserPublic__message_enc_pk(sd_public(pe, pf, pm)) = pe. +reduc forall pe: bitstring, pf: bitstring, pm: bitstring; + securedrop_protocol_minimal__traits__UserPublic__fetch_pk(sd_public(pe, pf, pm)) = pf. +reduc forall pe: bitstring, pf: bitstring, pm: bitstring; + securedrop_protocol_minimal__traits__UserPublic__message_metadata_pk(sd_public(pe, pf, pm)) = pm. + +(* Receiver model for the extracted `decrypt_with_sender`: a journalist holds one + ephemeral key bundle (apke secret + metadata secret) and a fetch keypair. The + key-bundle / keypair structs are `#[opaque]` in the ProVerif extraction, so ALL + their machinery lives here (this breaks the lib<->model dependency cycle: the + bundle constructor would otherwise be defined in lib.pvl, which loads AFTER this). + The backend's trial-decrypt loop consumes `keybundles()` as an `array_cons` list. *) +fun sd_bundle(bitstring, bitstring): bitstring [data]. (* apkeSk, metaSk *) +fun sd_kp_apke(bitstring): bitstring [data]. (* wraps apke secret *) +fun sd_kp_meta(bitstring): bitstring [data]. (* wraps metadata secret *) + +(* bundle.apke / bundle.metadata_kp, then keypair.private_key() (the `sk` field). *) +reduc forall a: bitstring, m: bitstring; + securedrop_protocol_minimal__keys__MessageKeyBundle__MessageKeyBundle__apke(sd_bundle(a, m)) = sd_kp_apke(a). +reduc forall a: bitstring, m: bitstring; + securedrop_protocol_minimal__keys__MessageKeyBundle__MessageKeyBundle__metadata_kp(sd_bundle(a, m)) = sd_kp_meta(m). +reduc forall a: bitstring; + securedrop_protocol_minimal__message__MessageKeyPair__MessageKeyPair__sk(sd_kp_apke(a)) = a. +reduc forall m: bitstring; + securedrop_protocol_minimal__metadata__MetadataKeyPair__MetadataKeyPair__sk(sd_kp_meta(m)) = m. + +fun sd_journalist(bitstring, bitstring, bitstring): bitstring [data]. (* apkeSk, metaSk, fetchSk *) +reduc forall a: bitstring, m: bitstring, f: bitstring; + securedrop_protocol_minimal__traits__UserSecret__keybundles(sd_journalist(a, m, f)) = + rust_primitives__hax__array_cons(sd_bundle(a, m), rust_primitives__hax__array_nil()). +reduc forall a: bitstring, m: bitstring, f: bitstring; + securedrop_protocol_minimal__traits__UserSecret__fetch_keypair(sd_journalist(a, m, f)) = + rust_primitives__hax__Tuple2__Tuple2(f, crypto__dh_pub(f)). diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/hax.py b/securedrop-protocol/protocol-minimal/proofs/proverif/hax.py new file mode 100644 index 00000000..ed6e3d80 --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/hax.py @@ -0,0 +1,353 @@ +#!/usr/bin/env python3 +"""ProVerif driver for securedrop-protocol-minimal (hax ProVerif backend). + +Mirrors the SPQR / Mandrake flagship setups. Subcommands: + + extract-proverif `cargo hax into -i '' proverif` -> extraction/lib.pvl + (injects the dev hax-lib via `cargo --config`; restores Cargo.lock) + verify-proverif run ProVerif on queries/*.pv, print RESULT lines + check-proverif run ProVerif and assert each query's (* EXPECTPV ... END *) block + `check-proverif update` regenerates those blocks + +Toolchain: the `hax-proverif` opam switch supplies cargo-hax + hax-rust-engine + +hax-engine + proverif. `HAX_PROVERIF_DIR` (default ~/hax-proverif-backend) supplies +the dev hax-lib (proverif macros) and the shared primitives.pvl / cryptolib.pvl. +The ProVerif annotations are gated on cfg(hax_backend_proverif), which hax sets +itself during `into proverif` — so normal builds / `into fstar` are unaffected. +""" +import argparse +import hashlib +import os +import re +import shutil +import subprocess +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +CRATE = os.path.normpath(os.path.join(HERE, "..", "..")) # protocol-minimal/ +GEN = os.path.join(HERE, "extraction") +HANDWRITTEN = os.path.join(HERE, "handwritten") +VENDORED = os.path.join(HERE, "lib") # vendored primitives.pvl / cryptolib.pvl +QUERIES = os.path.join(HERE, "queries") +LIB_SHA = os.path.join(GEN, "lib.pvl.sha256") + +HAX_PROVERIF_DIR = os.environ.get( + "HAX_PROVERIF_DIR", os.path.expanduser("~/hax-proverif-backend") +) +HAX_OPAM_SWITCH = os.environ.get("HAX_OPAM_SWITCH", "hax-proverif") + + +def _pvlib_dir(): + """Directory holding primitives.pvl / cryptolib.pvl: the vendored in-repo copy + (self-contained, engine-free CI) if present, else the hax checkout.""" + if os.path.exists(os.path.join(VENDORED, "primitives.pvl")): + return VENDORED + return os.path.join(HAX_PROVERIF_DIR, "hax-lib", "proof-libs", "proverif") + +# ProVerif extraction roots. `-**` drops everything; each `+` re-selects a protocol +# entry point and pulls in its transitive closure. Crypto leaves are redirected to +# the symbolic model by source-level cfg(hax_backend_proverif) `replace_body` +# annotations, so their libcrux/hpke internals never reach lib.pvl. +PROVERIF_INCLUDE = " ".join([ + "-**", + "+securedrop_protocol_minimal::encrypt_decrypt::encrypt", + "+securedrop_protocol_minimal::encrypt_decrypt::decrypt_with_sender", + "+securedrop_protocol_minimal::message::auth_enc", + "+securedrop_protocol_minimal::message::auth_dec", + "+securedrop_protocol_minimal::metadata::encrypt", + "+securedrop_protocol_minimal::metadata::decrypt", + "+securedrop_protocol_minimal::sign::**::sign", + "+securedrop_protocol_minimal::sign::**::verify", +]) + +# -lib load order (declare-before-use): generic prelude -> generic crypto -> +# SecureDrop composites -> diagnostic stubs -> generated model -> query file. +def proverif_libs(): + pvlib = _pvlib_dir() + return [ + "-lib", os.path.join(pvlib, "primitives"), + "-lib", os.path.join(pvlib, "cryptolib"), + "-lib", os.path.join(HANDWRITTEN, "sd_crypto"), + "-lib", os.path.join(HANDWRITTEN, "sd_model"), + "-lib", os.path.join(GEN, "missingdecl"), + "-lib", os.path.join(GEN, "lib"), + ] + + +def opam_prefix(): + """Command prefix that runs the wrapped command with the hax-proverif switch env + (cargo-hax + hax-rust-engine + hax-engine on PATH). `opam exec` preserves the base + PATH, so system cargo / proverif stay available. If opam isn't on PATH we assume + the caller already `eval`'d the switch env.""" + if _has(["opam", "--version"]): + return ["opam", "exec", "--switch", HAX_OPAM_SWITCH, "--"] + return [] + + +def _has(cmd): + try: + subprocess.run(cmd, capture_output=True) + return True + except FileNotFoundError: + return False + + +def child_env(): + env = dict(os.environ) + env["HAX_PROVERIF_DIR"] = HAX_PROVERIF_DIR + return env + + +def cmd_extract(args): + env = child_env() + include = args.include if args.include else PROVERIF_INCLUDE + # Inject the dev hax-lib (proverif macros) via `cargo --config`, NOT a committed + # [patch.crates-io], so normal builds / CI stay on crates.io hax-lib 0.3.7. + lib = os.path.join(HAX_PROVERIF_DIR, "hax-lib") + patch = [] + for crate, path in [ + ("hax-lib", lib), + ("hax-lib-macros", os.path.join(lib, "macros")), + ("hax-lib-macros-types", os.path.join(lib, "macros", "types")), + ]: + patch += ["--config", 'patch.crates-io."{}".path="{}"'.format(crate, path)] + # The --config patch rewrites hax-lib's Cargo.lock entry; preserve the committed lock. + lock = os.path.join(CRATE, "Cargo.lock") + ws_lock = os.path.normpath(os.path.join(CRATE, "..", "Cargo.lock")) + backups = {} + for p in (lock, ws_lock): + if os.path.exists(p): + with open(p, "rb") as f: + backups[p] = f.read() + try: + rc = subprocess.run( + opam_prefix() + ["cargo", "hax", "-C"] + patch + [";", "into", "-i", include, "proverif"], + cwd=CRATE, env=env, + ).returncode + finally: + for p, data in backups.items(): + with open(p, "wb") as f: + f.write(data) + # Pin the generated snapshot so the engine-free `reconstruct-proverif` lane can + # detect drift (SPQR pattern). + lib = os.path.join(GEN, "lib.pvl") + if os.path.exists(lib): + with open(LIB_SHA, "w") as f: + f.write(_sha256(lib) + " lib.pvl\n") + # cargo-hax exits nonzero on diagnostics but still writes output; filter + report. + md = os.path.join(GEN, "missingdecl.pvl") + if os.path.exists(md): + _filter_missingdecl(md) + leaked = [l for l in open(md).read().splitlines() + if l.strip() and not l.strip().startswith("(*") + and "string_lit__" not in l] + print("\n== missingdecl.pvl: {} non-string-literal external(s) ==".format(len(leaked))) + for l in leaked: + print(" " + l) + if not leaked: + print(" (clean — only benign string literals remain)") + return rc + + +# Names of symbols the extracted model references but that are DEFINED by our +# hand-written libs (sd_crypto.pvl, sd_model.pvl). hax can't see those definitions, +# so it lists them in missingdecl.pvl; leaving them there would double-declare the +# symbol at ProVerif load time. Strip them (mandrake computes missingdecl the same +# way: "referenced but not defined by ANY loaded lib"). +_DECL_RE = re.compile(r"^\s*(?:fun|letfun|const)\s+([A-Za-z_][A-Za-z0-9_]*)") +_REDUC_RE = re.compile(r"([A-Za-z_][A-Za-z0-9_]*)\s*\(") + + +def _handwritten_defined(): + # Names DEFINED by any lib loaded alongside the model: our handwritten libs AND + # the vendored primitives/cryptolib. hax only excludes `fun`/`const` decls from + # missingdecl, not `reduc`-defined destructors (e.g. Tuple2__0/1 live in + # primitives.pvl as reducs), so those leak in and would double-declare. Drop them. + names = set() + scan = [] + if os.path.isdir(HANDWRITTEN): + scan += [os.path.join(HANDWRITTEN, f) for f in os.listdir(HANDWRITTEN) if f.endswith(".pvl")] + pvlib = _pvlib_dir() + scan += [os.path.join(pvlib, f) for f in ("primitives.pvl", "cryptolib.pvl") + if os.path.exists(os.path.join(pvlib, f))] + for path in scan: + text = open(path).read() + # fun / letfun / const declarations (line-based) + for line in text.splitlines(): + m = _DECL_RE.match(line.strip()) + if m: + names.add(m.group(1)) + # reduc destructor heads: `reduc forall ...; NAME(pat) = rhs.` — the head + # NAME may sit on a later line than `reduc`, so scan each reduc statement. + for chunk in text.split("reduc")[1:]: + semi = chunk.find(";") + seg = chunk[semi + 1:] if semi >= 0 else chunk + mm = _REDUC_RE.search(seg) + if mm: + names.add(mm.group(1)) + return names + + +def _filter_missingdecl(md): + defined = _handwritten_defined() + kept = [] + for line in open(md).read().splitlines(): + m = _DECL_RE.match(line.strip()) + if m and m.group(1) in defined: + continue # defined by a handwritten lib; drop the redundant stub + kept.append(line) + with open(md, "w") as f: + f.write("\n".join(kept) + "\n") + + +def _sha256(path): + h = hashlib.sha256() + with open(path, "rb") as f: + for chunk in iter(lambda: f.read(65536), b""): + h.update(chunk) + return h.hexdigest() + + +def cmd_reconstruct(args): + """Engine-free CI lane: confirm the committed lib.pvl snapshot is intact (matches + its pinned digest) so ProVerif runs against a known model without rebuilding hax.""" + lib = os.path.join(GEN, "lib.pvl") + if not os.path.exists(lib): + print("ERROR: {} missing — run extract-proverif first.".format(lib)) + return 1 + if not os.path.exists(LIB_SHA): + print("ERROR: {} missing — run extract-proverif to pin it.".format(LIB_SHA)) + return 1 + want = open(LIB_SHA).read().split()[0] + got = _sha256(lib) + if want != got: + print("MISMATCH: lib.pvl digest\n pinned: {}\n current: {}".format(want, got)) + print("The committed model drifted from its pin. Re-run extract-proverif and " + "re-verify verdicts before committing.") + return 1 + pvlib = _pvlib_dir() + print("reconstruct-proverif: lib.pvl matches pin ({}…); libs from {}.".format( + got[:12], "vendored lib/" if pvlib == VENDORED else pvlib)) + return 0 + + +_EXPECTPV_RE = re.compile(r"\(\*\s*EXPECTPV\b.*?\bEND\s*\*\)", re.DOTALL) + + +def _proverif_prefix(): + # ProVerif is a plain binary — the check/verify lanes must NOT depend on the + # hax-proverif opam switch (CI installs only `proverif`). Use it directly if on + # PATH; else fall back to the switch (local dev where it lives only there). + return [] if shutil.which("proverif") else opam_prefix() + + +def _run_proverif(env, query): + cmd = _proverif_prefix() + ["proverif"] + proverif_libs() + [os.path.join(QUERIES, query)] + out = subprocess.run(cmd, cwd=HERE, env=env, capture_output=True, text=True) + combined = out.stdout + out.stderr + return combined, [l.strip() for l in combined.splitlines() if l.strip().startswith("RESULT")] + + +def _expected(query): + text = open(os.path.join(QUERIES, query)).read() + m = _EXPECTPV_RE.search(text) + if not m: + return None + return [l.strip() for l in m.group(0).splitlines() if l.strip().startswith("RESULT")] + + +def _queries(): + if not os.path.isdir(QUERIES): + return [] + return sorted(f for f in os.listdir(QUERIES) if f.endswith(".pv")) + + +def cmd_verify(args): + env = child_env() + targets = args.queries if args.queries else _queries() + for q in targets: + combined, results = _run_proverif(env, q) + print("== {} ==".format(q)) + for r in results: + print(" " + r) + return 0 + + +def cmd_check(args): + env = child_env() + targets = args.queries if args.queries else _queries() + grand_ok = grand_total = 0 + failed = False + for q in targets: + combined, actual = _run_proverif(env, q) + if args.update: + _write_expectpv(q, actual) + print(" {:<28} updated ({} RESULT lines)".format(q, len(actual))) + continue + expected = _expected(q) + if expected is None: + print(" {:<28} NO EXPECTPV BLOCK".format(q)) + failed = True + continue + n = min(len(expected), len(actual)) + ok = sum(1 for i in range(n) if expected[i] == actual[i]) + file_ok = len(expected) == len(actual) and ok == len(expected) + grand_ok += ok + grand_total += len(expected) + failed = failed or not file_ok + print(" {:<28} {}/{} match [{}]".format(q, ok, len(expected), "OK" if file_ok else "FAIL")) + if not file_ok: + for i in range(max(len(expected), len(actual))): + e = expected[i] if i < len(expected) else "(none)" + a = actual[i] if i < len(actual) else "(none)" + if e != a: + print(" exp: {}\n got: {}".format(e, a)) + if args.update: + return 0 + print("\n{}/{} RESULT lines match EXPECTPV.".format(grand_ok, grand_total)) + if failed: + print("CHECK FAILED.") + return 1 + print("CHECK PASSED.") + return 0 + + +def _write_expectpv(query, actual): + path = os.path.join(QUERIES, query) + text = open(path).read() + block = "(* EXPECTPV\n" + "\n".join(actual) + "\nEND *)" + if _EXPECTPV_RE.search(text): + text = _EXPECTPV_RE.sub(block, text) + else: + text = text.rstrip() + "\n\n" + block + "\n" + with open(path, "w") as f: + f.write(text) + + +def main(): + p = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + sub = p.add_subparsers(dest="cmd", required=True) + + e = sub.add_parser("extract-proverif", help="cargo hax into proverif -> extraction/lib.pvl") + e.add_argument("--include", help="override the -i target filter") + e.set_defaults(func=cmd_extract) + + r = sub.add_parser("reconstruct-proverif", + help="engine-free: verify the committed lib.pvl snapshot digest") + r.set_defaults(func=cmd_reconstruct) + + v = sub.add_parser("verify-proverif", help="run ProVerif, print RESULT lines") + v.add_argument("queries", nargs="*", help="query files (default: all queries/*.pv)") + v.set_defaults(func=cmd_verify) + + c = sub.add_parser("check-proverif", help="run ProVerif, assert EXPECTPV blocks") + c.add_argument("--update", action="store_true", help="regenerate EXPECTPV blocks") + c.add_argument("queries", nargs="*", help="query files (default: all queries/*.pv)") + c.set_defaults(func=cmd_check) + + args = p.parse_args() + sys.exit(args.func(args)) + + +if __name__ == "__main__": + main() diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/lib/PROVENANCE.md b/securedrop-protocol/protocol-minimal/proofs/proverif/lib/PROVENANCE.md new file mode 100644 index 00000000..2d6d773b --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/lib/PROVENANCE.md @@ -0,0 +1,24 @@ +# Vendored ProVerif support libraries + +`primitives.pvl` and `cryptolib.pvl` are **verbatim copies** of the hax ProVerif +backend's shared symbolic libraries, from: + + ~/hax-proverif-backend/hax-lib/proof-libs/proverif/{primitives,cryptolib}.pvl + (hax ProVerif backend — draft PR cryspen/hax#2068) + +They are vendored here so the ProVerif check (`hax.py check-proverif`) runs +**self-contained** — no hax checkout / opam switch required, only a `proverif` +binary. This is what the engine-free CI lane (`hax.py reconstruct-proverif`) uses, +and it also freezes the trusted crypto model so upstream changes can't silently +alter our verdicts. + +- `primitives.pvl` — hax uniform-bitstring prelude (channel `c`, tuple/Option/bool + constructors, `nat_lit`, `bitstring_err`, machine-int helpers). +- `cryptolib.pvl` — generic Dolev-Yao crypto (`crypto__aead_*`, `crypto__kdf`, + `crypto__hkdf_*`, `crypto__dh_*`, `crypto__kem_*`, `crypto__vk_of`/`sign`/ + `sig_verify`, `crypto__serialize*`). + +**Refresh** (only when the upstream shared libs change): re-copy both files from the +backend checkout, then re-run `hax.py extract-proverif && hax.py check-proverif` and +re-commit if verdicts are unchanged. The SecureDrop-specific composites live +separately in `../handwritten/{sd_crypto,sd_model}.pvl`. diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/lib/cryptolib.pvl b/securedrop-protocol/protocol-minimal/proofs/proverif/lib/cryptolib.pvl new file mode 100644 index 00000000..b41fedc3 --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/lib/cryptolib.pvl @@ -0,0 +1,124 @@ +(*****************************************************************) +(* hax — unified symbolic crypto library (cryptolib.pvl) *) +(*****************************************************************) +(* A single, vetted Dolev-Yao model of the standard cryptographic *) +(* primitives, shared by every hax ProVerif extraction. Protocol *) +(* code never re-declares these: each crypto wrapper redirects to *) +(* a primitive below with *) +(* *) +(* #[hax_lib::proverif::replace_body("crypto__aead_enc(k,m,ad)")] *) +(* *) +(* so the protocol stays plain Rust (no `${}` antiquotes, no per- *) +(* example `fun`/`reduc` blocks) and the trusted model lives once, *) +(* here, where it can be audited in isolation. *) +(* *) +(* Everything is uniform `bitstring` (the hax ProVerif model): no *) +(* `type` declarations, so these names resolve directly against *) +(* extracted code. One-way primitives are opaque `fun`s; their *) +(* correctness/inverse relations are `reduc` destructors (partial: *) +(* a forged input simply has no value, modelling unforgeability). *) +(* *) +(* Load after primitives.pvl: *) +(* proverif -lib primitives.pvl -lib cryptolib.pvl lib.pvl *) +(* *) +(* Provenance: unifies the per-example models of proverif-psk, *) +(* libcrux-psq (`psq_crypto.pvl`), Mandrake/Minos (`crypto/*.rs` *) +(* `before`+`replace_body` blocks), Bertie (`handwritten_lib.pvl`) *) +(* and SPQR (`handwritten/cryptolib.pvl`). *) +(*****************************************************************) + +(*===============================================================*) +(* Hash — one-way, collision-resistant, injective in the term *) +(* algebra. `crypto__hash` takes one argument; hash several values *) +(* by hashing a tuple, and chain a running transcript by hashing *) +(* `(old, input)`. *) +(*===============================================================*) +fun crypto__hash(bitstring): bitstring. + +(*===============================================================*) +(* AEAD — authenticated encryption with associated data. *) +(* *) +(* Combined form (ciphertext carries the tag): `crypto__aead_enc` *) +(* produces an opaque ciphertext; `crypto__aead_dec` is the *) +(* partial inverse — it yields the plaintext only for a genuine *) +(* ciphertext under the matching key and AAD, so a forgery fails. *) +(*===============================================================*) +fun crypto__aead_enc(bitstring, bitstring, bitstring): bitstring. (* key, plaintext, aad -> ciphertext *) +reduc forall k: bitstring, pt: bitstring, ad: bitstring; + crypto__aead_dec(k, crypto__aead_enc(k, pt, ad), ad) = pt. + +(* Detached form (separate ciphertext + tag on the wire), e.g. *) +(* libcrux `encrypt_detached` / PSQ. *) +fun crypto__aead_ct(bitstring, bitstring, bitstring): bitstring. (* key, plaintext, aad -> ciphertext *) +fun crypto__aead_tag(bitstring, bitstring, bitstring): bitstring. (* key, plaintext, aad -> tag *) +reduc forall k: bitstring, pt: bitstring, ad: bitstring; + crypto__aead_dec_detached(k, crypto__aead_ct(k, pt, ad), crypto__aead_tag(k, pt, ad), ad) = pt. + +(*===============================================================*) +(* KDF / HKDF — one-way key derivation. *) +(*===============================================================*) +fun crypto__kdf(bitstring, bitstring): bitstring. (* ikm, info -> okm *) +fun crypto__hkdf_extract(bitstring, bitstring): bitstring. (* salt, ikm -> prk *) +fun crypto__hkdf_expand(bitstring, bitstring): bitstring. (* prk, info -> okm *) + +(*===============================================================*) +(* Diffie-Hellman — `crypto__dh_pub(sk)` is the public key, *) +(* `crypto__dh_shared(sk, pk)` the shared secret, related by the *) +(* standard commutativity equation. *) +(*===============================================================*) +fun crypto__dh_pub(bitstring): bitstring. +fun crypto__dh_shared(bitstring, bitstring): bitstring. (* my_sk, peer_pk -> shared *) +equation forall x: bitstring, y: bitstring; + crypto__dh_shared(x, crypto__dh_pub(y)) = crypto__dh_shared(y, crypto__dh_pub(x)). + +(*===============================================================*) +(* KEM (e.g. ML-KEM / Kyber) — encapsulate a fresh shared secret *) +(* `ss` to a public key; only the secret-key holder decapsulates. *) +(* `ss` is chosen fresh by the caller (`new ss; ...`) so each *) +(* encapsulation is distinct. *) +(*===============================================================*) +fun crypto__kem_pk(bitstring): bitstring. (* sk -> pk *) +fun crypto__kem_encaps(bitstring, bitstring): bitstring. (* pk, ss -> ciphertext *) +reduc forall sk: bitstring, ss: bitstring; + crypto__kem_decaps(sk, crypto__kem_encaps(crypto__kem_pk(sk), ss)) = ss. + +(*===============================================================*) +(* Signatures (EUF-CMA) — `crypto__vk_of(sk)` is the verification *) +(* key; `crypto__sig_verify` succeeds (returns unit) only for a *) +(* genuine signature under the matching key, so a forgery fails. *) +(*===============================================================*) +fun crypto__vk_of(bitstring): bitstring. (* sk -> vk *) +fun crypto__sign(bitstring, bitstring): bitstring. (* sk, message -> signature *) +reduc forall sk: bitstring, m: bitstring; + crypto__sig_verify(crypto__vk_of(sk), m, crypto__sign(sk, m)) = + rust_primitives__hax__Tuple0__Tuple0. + +(*===============================================================*) +(* MAC / HMAC — `crypto__mac` is the tag; `crypto__mac_verify` *) +(* succeeds (returns unit) only for a genuine tag. *) +(*===============================================================*) +fun crypto__mac(bitstring, bitstring): bitstring. (* key, message -> tag *) +reduc forall k: bitstring, m: bitstring; + crypto__mac_verify(k, m, crypto__mac(k, m)) = rust_primitives__hax__Tuple0__Tuple0. + +(*===============================================================*) +(* Serialization — invertible wire encoding. *) +(* *) +(* Single serializer per protocol: `crypto__serialize(x)` is an *) +(* injective encoding; `crypto__deserialize` recovers the payload. *) +(* A protocol with ONE wire format (e.g. proverif-psk) redirects *) +(* its serializer/parser straight to these. *) +(*===============================================================*) +fun crypto__serialize(bitstring): bitstring. (* payload -> bytes *) +reduc forall x: bitstring; + crypto__deserialize(crypto__serialize(x)) = x. + +(* Tagged variant — for a protocol with SEVERAL distinct wire *) +(* formats. Model serializer `f(x)` as `crypto__serialize_tagged *) +(* (tag_f, x)` and its parser as `crypto__deserialize_tagged *) +(* (tag_f, bytes)`; the per-format `tag_f` is a distinct nullary *) +(* constant, which keeps the formats' encodings from unifying. *) +(* (Each `tag_f` must be declared by the using protocol.) *) +fun crypto__serialize_tagged(bitstring, bitstring): bitstring. (* tag, payload -> bytes *) +reduc forall t: bitstring, x: bitstring; + crypto__deserialize_tagged(t, crypto__serialize_tagged(t, x)) = x. diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/lib/primitives.pvl b/securedrop-protocol/protocol-minimal/proofs/proverif/lib/primitives.pvl new file mode 100644 index 00000000..2b87329e --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/lib/primitives.pvl @@ -0,0 +1,503 @@ +(*****************************************************************) +(* hax — ProVerif primitives library *) +(*****************************************************************) +(* Anything that used to live in the per-extraction `lib.pvl` *) +(* preamble is here instead. Loading this file via `-lib` gives *) +(* the extracted file everything it needs to typecheck: *) +(* *) +(* - `channel c.` — the public attacker channel. *) +(* - `construct_fail` / `empty` — fail/default helpers. *) +(* - `Some`/`None` (`Option_err`) — `Option` constructors. *) +(* - `True`/`False` (`bool_default`/`bool_err`) — booleans. *) +(* - `nat_lit` — encode `usize`/`uN`/`iN` literals. *) +(* - `logical_and`/`logical_or` — opaque `&&`/`||`. *) +(* - `rust_primitives::*`, `core::num`/`ops`/`cmp`/`slice` *) +(* trait roots, `hax_lib::*` helpers, the tuple constructors. *) +(* *) +(* `core_models::*` symbols are out of scope here; they'll *) +(* migrate upstream as `#[proverif_replace]` annotations. *) +(* *) +(* Use: *) +(* proverif -lib primitives.pvl lib.pvl *) +(*****************************************************************) + +(*** Public attacker channel ***) +channel c. + +(*** Fail / default helpers ***) +fun construct_fail() : bitstring +reduc construct_fail() = fail. + +const empty: bitstring. +letfun bitstring_default() = empty. +letfun bitstring_err() = let x = construct_fail() in bitstring_default(). + +(*** Option ***) +fun Some(bitstring): bitstring [data]. +fun None(): bitstring [data]. +letfun Option_err() = let x = construct_fail() in None(). + +(*** Boolean encoding ***) +fun True(): bitstring [data]. +fun False(): bitstring [data]. +letfun bool_default() = False(). +letfun bool_err() = let x = construct_fail() in False(). + +(*** Integer literal lifting ***) +fun nat_lit(nat): bitstring [data]. + +(*** Opaque short-circuit operators ***) +fun logical_and(bitstring, bitstring): bitstring. +fun logical_or(bitstring, bitstring): bitstring. + +(*** rust_primitives::hax — tuple constructors, dropped bodies, ***) +(*** machine_int / int operators (output of the Specialize phase) ***) + +const rust_primitives__hax__Tuple0__Tuple0: bitstring. +fun rust_primitives__hax__Tuple1__Tuple1(bitstring): bitstring [data]. +fun rust_primitives__hax__Tuple2__Tuple2(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__Tuple3__Tuple3(bitstring, bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__Tuple4__Tuple4(bitstring, bitstring, bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__Tuple5__Tuple5(bitstring, bitstring, bitstring, bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__Tuple6__Tuple6(bitstring, bitstring, bitstring, bitstring, bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__Tuple7__Tuple7(bitstring, bitstring, bitstring, bitstring, bitstring, bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__Tuple8__Tuple8(bitstring, bitstring, bitstring, bitstring, bitstring, bitstring, bitstring, bitstring): bitstring [data]. + +const rust_primitives__hax__dropped_body: bitstring. +fun rust_primitives__hax__never_to_any(bitstring): bitstring [data]. +fun rust_primitives__hax__cast_op(bitstring): bitstring [data]. +fun rust_primitives__hax__logical_op_and(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__logical_op_or(bitstring, bitstring): bitstring [data]. + +(* `+ 1` on a `nat_lit` reduces concretely (`nat_lit(x) + nat_lit(1) = nat_lit(x+1)`) + so loop/epoch counters become `nat_lit(1)`, `nat_lit(2)`, ... that queries can + name and order (ProVerif `nat` supports only `x + constant`). Any other operands + (byte arithmetic on opaque blobs) fall through to an opaque `[data]` term. *) +fun rust_primitives__hax__machine_int__add_opaque(bitstring, bitstring): bitstring [data]. +letfun rust_primitives__hax__machine_int__add(a: bitstring, b: bitstring) = + let nat_lit(x) = a in + (let nat_lit(1) = b in nat_lit(x + 1) + else rust_primitives__hax__machine_int__add_opaque(a, b)) + else rust_primitives__hax__machine_int__add_opaque(a, b). +fun rust_primitives__hax__machine_int__sub(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__machine_int__mul(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__machine_int__div(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__machine_int__rem(bitstring, bitstring): bitstring [data]. +(* Integer (in)equality is *structural* equality on the symbolic terms, like + `PartialEq::eq` below. Without this, `eq(x, x)` stays an opaque term that + never reduces to `True()`, so every `if a == b` / `assert_eq!(a, b)` / + `find(|e| e.id == id)` mis-fires (e.g. a prefix check that always "fails"). + The ordering comparisons (`lt`/`le`/`gt`/`ge`) and arithmetic stay opaque — + the model carries no integer arithmetic. *) +letfun rust_primitives__hax__machine_int__eq(a: bitstring, b: bitstring) = + let (= a) = b in True() else False(). +letfun rust_primitives__hax__machine_int__ne(a: bitstring, b: bitstring) = + let (= a) = b in False() else True(). +fun rust_primitives__hax__machine_int__lt(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__machine_int__le(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__machine_int__gt(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__machine_int__ge(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__machine_int__shl(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__machine_int__shr(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__machine_int__bitxor(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__machine_int__bitand(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__machine_int__bitor(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__machine_int__not(bitstring): bitstring [data]. + +fun rust_primitives__hax__int__add(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__int__sub(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__int__mul(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__int__div(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__int__rem(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__int__neg(bitstring): bitstring [data]. +fun rust_primitives__hax__int__eq(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__int__ne(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__int__lt(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__int__le(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__int__gt(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__int__ge(bitstring, bitstring): bitstring [data]. +fun rust_primitives__hax__int__from_machine(bitstring): bitstring [data]. +fun rust_primitives__hax__int__into_machine(bitstring): bitstring [data]. + +(*** rust_primitives::arithmetic / slice / sequence — non-auto-decl ***) +(* The ~251 per-int-width arithmetic ops and most slice / sequence *) +(* primitives are opaque `fun NAME(...): bitstring [data].` shapes, *) +(* shape-identical to what the auto-decl pass synthesises, and have *) +(* `#[cfg_attr(hax_backend_proverif, hax_lib::pv_constructor)]` on *) +(* their Rust source. They've been removed from this file. *) +(* What stays below is the small set that is *not* shape-equivalent *) +(* to auto-decl: identity letfuns that collapse otherwise-distinct *) +(* collection wrappers (so equality fires across `&v[..]` vs *) +(* `v.as_slice()`), the `*SIZE_*` consts, and synthesised names *) +(* (`neg`, `slice_index_range`, `hax::repeat`) with no Rust source. *) + +const rust_primitives__arithmetic__ISIZE_MAX: bitstring. +const rust_primitives__arithmetic__ISIZE_MIN: bitstring. +const rust_primitives__arithmetic__USIZE_MAX: bitstring. +const rust_primitives__arithmetic__SIZE_BITS: bitstring. + +fun rust_primitives__arithmetic__neg(bitstring): bitstring [data]. + +fun rust_primitives__slice__slice_index_range(bitstring, bitstring, bitstring): bitstring [data]. +letfun rust_primitives__slice__slice_to_array(x: bitstring) = x. +letfun rust_primitives__slice__as_slice(x: bitstring) = x. +fun rust_primitives__slice__len(bitstring): bitstring [data]. + +letfun rust_primitives__sequence__seq_to_vec(x: bitstring) = x. +letfun rust_primitives__sequence__vec_to_seq(x: bitstring) = x. +fun rust_primitives__sequence__seq_len(bitstring): bitstring [data]. + +letfun rust_primitives__unsize(x: bitstring) = x. + +fun rust_primitives__hax__repeat(bitstring, bitstring): bitstring [data]. + +(* Fixed-size array literals `[a, b, c]` are encoded as a cons-list, since *) +(* ProVerif is first-order and has no array literals. The backend emits *) +(* `array_cons(a, array_cons(b, array_cons(c, array_nil())))`. Collections *) +(* iterated by a `for` loop are modelled as the same cons-list ("Seq"): the *) +(* backend unrolls the loop by *destructuring* `array_cons` off the front a *) +(* bounded number of times (peeling real element values), taking the `else` *) +(* / done branch once the Seq is `array_nil`, and failing with *) +(* `bitstring_err()` if a present element remains past the bound. *) +fun rust_primitives__hax__array_nil(): bitstring [data]. +fun rust_primitives__hax__array_cons(bitstring, bitstring): bitstring [data]. + +(* Seq operations (workstream 2). A `Vec`/slice is the `array_cons` cons-list *) +(* above. The operations below give that list *real* semantics, bounded to the *) +(* first few elements (matching the loop unroll bound), and degrade to an *) +(* opaque term when an operand is not an `array_cons` Seq — e.g. a byte buffer *) +(* (`Vec`/`Bytes`) carried as an uninterpreted crypto blob, where element- *) +(* wise structure is neither known nor needed. This split keeps structural *) +(* collections (`Vec`, …) peelable while byte concatenation stays an *) +(* opaque, collision-free symbol. *) +(* Byte concatenation of two opaque blobs. Modeled as an invertible pair + ([data]) — the standard symbolic abstraction for length-known concatenation, + so a later fixed-offset split (`s[..n]` / `s[n..]`, e.g. unpacking a hybrid + KEM encapsulation `classic_encap ++ pq_encap`) recovers the two parts. This + is conservative (it only gives the attacker more power). *) +fun array_concat(bitstring, bitstring): bitstring [data]. +fun array_index_opaque(bitstring, bitstring): bitstring. (* opaque index fallback *) +fun array_insert_opaque(bitstring, bitstring, bitstring): bitstring. (* opaque insert *) +fun array_remove_rest(bitstring, bitstring): bitstring. (* opaque "vec minus pos" *) +(* `a ++ b`: prepend the first few elements of `a` onto `b`; if `a` is opaque *) +(* (a byte blob) fall back to opaque concat. `array_extend_rest` finishes the *) +(* tail past the unrolled prefix. *) +letfun array_extend_rest(r: bitstring, b: bitstring) = + let rust_primitives__hax__array_nil() = r in b + else array_concat(r, b). +letfun array_extend(a: bitstring, b: bitstring) = + let rust_primitives__hax__array_cons(a0, r0) = a in ( + let rust_primitives__hax__array_cons(a1, r1) = r0 in ( + let rust_primitives__hax__array_cons(a2, r2) = r1 in ( + rust_primitives__hax__array_cons(a0, rust_primitives__hax__array_cons(a1, rust_primitives__hax__array_cons(a2, array_extend_rest(r2, b)))) + ) else rust_primitives__hax__array_cons(a0, rust_primitives__hax__array_cons(a1, b)) + ) else rust_primitives__hax__array_cons(a0, b) + ) else let rust_primitives__hax__array_nil() = a in b + else array_concat(a, b). + +(* `for x in coll` reaches the backend with an iterator of *) +(* `coll.iter()` / `IntoIterator::into_iter(coll)`. For the loop's Seq to be *) +(* the underlying cons-list, these iterator-producing wrappers are identity. *) +letfun core__slice__Impl__iter(x: bitstring) = x. +letfun core__iter__traits__collect__IntoIterator__into_iter(x: bitstring) = x. + +(*** core::cmp / ops — letfuns with non-opaque semantics ***) +(* These are *not* shape-equivalent to the auto-decl fallback: they *) +(* fire ProVerif rewrite rules. Plain opaque ops on the same *) +(* trait root (`PartialOrd::lt`, `Index::index`, `Fn::call`, *) +(* `slice::Impl::len`, `core::num::Impl_N::MAX/MIN`, etc.) are *) +(* equivalent to auto-decl and have been removed. *) + +(* Symbolic equality: `eq(x, x) = True()`, `eq(x, y) = False()` when + `x`, `y` are syntactically distinct ProVerif terms. Without this, + `PartialEq::eq` is opaque and a guard like + let (=True()) = eq(a, b) in ... + never fires even when `a` and `b` are *the same* constructor — which + silently makes large parts of protocol-state machinery unreachable. *) +letfun core__cmp__PartialEq__eq(a: bitstring, b: bitstring) = + let (=a) = b in True() else False(). +letfun core__cmp__PartialEq__ne(a: bitstring, b: bitstring) = + let (=a) = b in False() else True(). + +(* `core::ops::bit::Not::not` on `bool`. Negates *known* booleans only: + `True->False`, `False->True`, and an OPAQUE condition stays opaque. The + last case matters for `assert!(cond)` / `if !cond { panic }` where `cond` + is an un-modeled comparison (e.g. a length bound `okm_len <= 255*32` using + the opaque `<=`): mapping the opaque value to `True()` would make + `let (=True()) = not_kw(cond) in panic` fire spuriously and kill the trace. + Leaving it opaque means the assert is skipped (sound over-approximation), + while real `if !x` on a `True`/`False` value still works. *) +letfun core__ops__bit__Not__not_kw(b: bitstring) = + let (=True()) = b in False() + else let (=False()) = b in True() + else b. + +(*** core::convert — identity wrappers ***) +(* `From::from`, `Into::into`, `AsRef::as_ref`, `TryInto::try_into` *) +(* are all "wrap/unwrap one bitstring as another bitstring" under *) +(* the uniform-bitstring model. Keeping them opaque made `let *) +(* (=Pattern()) = X::into(v) in ...` not match its corresponding *) +(* `v` constructor. *) + +letfun core__convert__From__from(x: bitstring) = x. +letfun core__convert__Into__into(x: bitstring) = x. +letfun core__convert__AsRef__as_ref(x: bitstring) = x. +letfun core__convert__TryInto__try_into(x: bitstring) = x. +letfun core__convert__TryFrom__try_from(x: bitstring) = x. + +(*** core::ops::deref — also identity ***) +letfun core__ops__deref__Deref__deref(x: bitstring) = x. +letfun core__ops__deref__DerefMut__deref_mut(x: bitstring) = x. + +(*** alloc::* — Vec / Box wrappers are identity at the symbolic ***) +(*** level. Real protocol semantics don't care which heap- ***) +(*** allocation flavour the bytes are in. ***) +letfun alloc__slice__Impl__to_vec(x: bitstring) = x. +letfun alloc__vec__Impl_1__as_slice(x: bitstring) = x. +letfun alloc__borrow__ToOwned__to_owned(x: bitstring) = x. +letfun alloc__boxed__Impl__new_kw(x: bitstring) = x. + +(*** rand_core — `RngCore::fill_bytes` returns fresh bytes ***) +(* The trait method mutates its `dest: &mut [u8]` to fresh randomness *) +(* and returns the (state, dest) pair via the `&mut` mutation hax *) +(* phase rewrites. Symbolically this is a fresh `new` value. *) +letfun rand_core__RngCore__fill_bytes(rng: bitstring, dest: bitstring) = + new b: bitstring; + rust_primitives__hax__Tuple2__Tuple2(rng, b). + +(* `hax_lib::prop::constructors::from_bool` is a bool -> prop coercion *) +(* (identity in the bitstring model); `hax_lib::assume` is a proof hint *) +(* with no runtime effect, and the extracted code discards its result *) +(* (`let wildcard = assume(..)`). Both are identity `letfun`s: faithful *) +(* and footprint-free (an opaque `fun` would add a spurious constructor *) +(* to the attacker term algebra). Defining them here also keeps them *) +(* out of the auto-declared `missingdecl` diagnostic. *) +letfun hax_lib__prop__constructors__from_bool(b: bitstring) = b. +letfun hax_lib__assume(p: bitstring) = p. + +(*****************************************************************) +(* std prelude — formerly synthesised by the auto-decl pass as *) +(* invertible `[data]`. Made explicit here with real semantics *) +(* (or honest opaque stubs) so `missingdecl.pvl` stays a signal *) +(* and the one-way shapes are not silently destructurable. *) +(*****************************************************************) + +(*** Tuple field projectors `t.0` .. `t.5` (over the [data] tuple ctors) ***) +reduc forall a0: bitstring; + rust_primitives__hax__Tuple1__Tuple1__0(rust_primitives__hax__Tuple1__Tuple1(a0)) = a0. +reduc forall a0: bitstring, a1: bitstring; + rust_primitives__hax__Tuple2__Tuple2__0(rust_primitives__hax__Tuple2__Tuple2(a0,a1)) = a0. +reduc forall a0: bitstring, a1: bitstring; + rust_primitives__hax__Tuple2__Tuple2__1(rust_primitives__hax__Tuple2__Tuple2(a0,a1)) = a1. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring; + rust_primitives__hax__Tuple3__Tuple3__0(rust_primitives__hax__Tuple3__Tuple3(a0,a1,a2)) = a0. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring; + rust_primitives__hax__Tuple3__Tuple3__1(rust_primitives__hax__Tuple3__Tuple3(a0,a1,a2)) = a1. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring; + rust_primitives__hax__Tuple3__Tuple3__2(rust_primitives__hax__Tuple3__Tuple3(a0,a1,a2)) = a2. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring; + rust_primitives__hax__Tuple4__Tuple4__0(rust_primitives__hax__Tuple4__Tuple4(a0,a1,a2,a3)) = a0. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring; + rust_primitives__hax__Tuple4__Tuple4__1(rust_primitives__hax__Tuple4__Tuple4(a0,a1,a2,a3)) = a1. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring; + rust_primitives__hax__Tuple4__Tuple4__2(rust_primitives__hax__Tuple4__Tuple4(a0,a1,a2,a3)) = a2. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring; + rust_primitives__hax__Tuple4__Tuple4__3(rust_primitives__hax__Tuple4__Tuple4(a0,a1,a2,a3)) = a3. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring, a4: bitstring; + rust_primitives__hax__Tuple5__Tuple5__0(rust_primitives__hax__Tuple5__Tuple5(a0,a1,a2,a3,a4)) = a0. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring, a4: bitstring; + rust_primitives__hax__Tuple5__Tuple5__1(rust_primitives__hax__Tuple5__Tuple5(a0,a1,a2,a3,a4)) = a1. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring, a4: bitstring; + rust_primitives__hax__Tuple5__Tuple5__2(rust_primitives__hax__Tuple5__Tuple5(a0,a1,a2,a3,a4)) = a2. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring, a4: bitstring; + rust_primitives__hax__Tuple5__Tuple5__3(rust_primitives__hax__Tuple5__Tuple5(a0,a1,a2,a3,a4)) = a3. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring, a4: bitstring; + rust_primitives__hax__Tuple5__Tuple5__4(rust_primitives__hax__Tuple5__Tuple5(a0,a1,a2,a3,a4)) = a4. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring, a4: bitstring, a5: bitstring; + rust_primitives__hax__Tuple6__Tuple6__0(rust_primitives__hax__Tuple6__Tuple6(a0,a1,a2,a3,a4,a5)) = a0. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring, a4: bitstring, a5: bitstring; + rust_primitives__hax__Tuple6__Tuple6__1(rust_primitives__hax__Tuple6__Tuple6(a0,a1,a2,a3,a4,a5)) = a1. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring, a4: bitstring, a5: bitstring; + rust_primitives__hax__Tuple6__Tuple6__2(rust_primitives__hax__Tuple6__Tuple6(a0,a1,a2,a3,a4,a5)) = a2. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring, a4: bitstring, a5: bitstring; + rust_primitives__hax__Tuple6__Tuple6__3(rust_primitives__hax__Tuple6__Tuple6(a0,a1,a2,a3,a4,a5)) = a3. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring, a4: bitstring, a5: bitstring; + rust_primitives__hax__Tuple6__Tuple6__4(rust_primitives__hax__Tuple6__Tuple6(a0,a1,a2,a3,a4,a5)) = a4. +reduc forall a0: bitstring, a1: bitstring, a2: bitstring, a3: bitstring, a4: bitstring, a5: bitstring; + rust_primitives__hax__Tuple6__Tuple6__5(rust_primitives__hax__Tuple6__Tuple6(a0,a1,a2,a3,a4,a5)) = a5. + +(*** Option methods, over the `Some`/`None` constructors above. ***) +(* `unwrap`/`expect` on `None` is a panic -> `bitstring_err()` kills the *) +(* trace; `is_some`/`is_none` branch; `as_ref`/`cloned` are identity. *) +letfun core__option__Impl__unwrap(o: bitstring) = + let Some(x) = o in x else bitstring_err(). +letfun core__option__Impl__expect(o: bitstring, m: bitstring) = + let Some(x) = o in x else bitstring_err(). +letfun core__option__Impl__is_some(o: bitstring) = + let Some(x) = o in True() else False(). +letfun core__option__Impl__is_none(o: bitstring) = + let Some(x) = o in False() else True(). +letfun core__option__Impl__as_ref(o: bitstring) = o. +letfun core__option__Impl_2__cloned(o: bitstring) = o. +(* full-path Option ctors are referenced at a handful of sites; bodies *) +(* otherwise use the short `Some`/`None` the backend special-cases to. *) +fun core__option__Option__Some(bitstring): bitstring [data]. +const core__option__Option__None: bitstring. + +(*** Result is transparent under uniform-bitstring: a value that ***) +(*** reaches a use is the `Ok` payload, and errors are `bitstring_err()`, ***) +(*** so `unwrap` is the identity. `Ok`/`Err` ctors resolve referenced sites. ***) +letfun core__result__Impl__unwrap(r: bitstring) = r. +fun core__result__Result__Ok(bitstring): bitstring [data]. +fun core__result__Result__Err(bitstring): bitstring [data]. + +(*** core::clone — identity at the symbolic level ***) +letfun core__clone__Clone__clone(x: bitstring) = x. + +(*** alloc::string / slice — String is its bytes; these are identity ***) +letfun alloc__string__Impl__as_bytes(x: bitstring) = x. +letfun alloc__string__Impl__into_bytes(x: bitstring) = x. +letfun alloc__string__ToString__to_string(x: bitstring) = x. +letfun alloc__slice__Impl__into_vec(x: bitstring) = x. +letfun alloc__slice__Impl__sort(x: bitstring) = x. (* order-agnostic symbolically *) +letfun alloc__slice__Impl__join(x: bitstring, sep: bitstring) = x. +letfun core__hint__must_use(x: bitstring) = x. +letfun hex__encode(x: bitstring) = x. (* bytes <-> hex string, same symbol *) + +(* Injective serialization of two fixed-length byte fields (`a || b`). + Real serialization concatenates FIXED-LENGTH fields, so the byte string + determines the split unambiguously and the encoding is INJECTIVE in + (a, b). The flat `array_extend`/`array_concat` byte model is deliberately + NOT injective (boundaries shift, e.g. `array_extend(nil, x) = x`), which is + fine for opaque blobs but UNSOUND when a multi-field serialization feeds a + hash or signature: an attacker could re-partition a signed structure + (move bytes across the field boundary) into a different struct with the + same bytes, breaking authenticity. Use this constructor where a fixed-field + serialization is hashed/signed and never re-parsed. *) +fun serialize_fields2(bitstring, bitstring): bitstring. + +(*** Iterators: the iterator IS the underlying cons-list, so `collect`/`rev` ***) +(*** are identity (membership is order-agnostic). `extend` is Seq append. ***) +letfun core__iter__traits__iterator__Iterator__collect(x: bitstring) = x. +letfun core__iter__traits__iterator__Iterator__rev(x: bitstring) = x. +letfun core__iter__traits__collect__Extend__extend(a: bitstring, b: bitstring) = array_extend(a, b). + +(*** core::ops::range — RangeFrom bound as data ***) +fun core__ops__range__RangeFrom__RangeFrom(bitstring): bitstring [data]. + +(*** Panics kill the trace (an unreachable path in a sound model). ***) +letfun core__panicking__panic(x: bitstring) = bitstring_err(). +letfun core__panicking__panic_fmt(x: bitstring) = bitstring_err(). +letfun core__panicking__assert_failed(a: bitstring, b: bitstring, c: bitstring, d: bitstring) = bitstring_err(). +const core__panicking__AssertKind__Eq: bitstring. + +(*** Formatting / IO — debug-only, irrelevant to the security model. ***) +fun core__fmt__rt__Impl__new_debug(bitstring): bitstring. +fun core__fmt__rt__Impl__new_display(bitstring): bitstring. +fun core__fmt__rt__Impl_1__new_const(bitstring): bitstring. +fun core__fmt__rt__Impl_1__new_v1(bitstring, bitstring): bitstring. +fun alloc__fmt__format(bitstring): bitstring. +letfun std__io__stdio__u_print(x: bitstring) = rust_primitives__hax__Tuple0__Tuple0. +letfun std__io__stdio__u_eprint(x: bitstring) = rust_primitives__hax__Tuple0__Tuple0. + +(*** rand_core — fresh randomness, mirroring `RngCore::fill_bytes` above. ***) +letfun rand_core__TryRngCore__try_fill_bytes(rng: bitstring, dest: bitstring) = + new b: bitstring; + rust_primitives__hax__Tuple2__Tuple2(rng, b). +letfun rand__rngs__thread__rng(u: bitstring) = new r: bitstring; r. +const rand_core__os__OsRng__OsRng: bitstring. + +(*** Vec / slice as the array_cons Seq. `new`/`is_empty` are exact. ***) +(*** `push`/`append`/`index` have real Seq semantics (workstream 2); ***) +(*** `from_elem`/`len`/`last` remain opaque pending the count/Option model. ***) +letfun alloc__vec__Impl__new_kw(u: bitstring) = rust_primitives__hax__array_nil(). +letfun alloc__vec__Impl_1__is_empty(v: bitstring) = + let rust_primitives__hax__array_nil() = v in True() else False(). +letfun core__slice__Impl__is_empty(v: bitstring) = + let rust_primitives__hax__array_nil() = v in True() else False(). +fun alloc__vec__from_elem(bitstring, bitstring): bitstring. +(* `push` prepends: the Seq is newest-first, so `last()` (newest) is the head *) +(* and order-agnostic searches (`find`/`any`) are unaffected. This is O(1) and *) +(* avoids a bounded end-append that would overflow the loop bound. *) +letfun alloc__vec__Impl_1__push(s: bitstring, x: bitstring) = + rust_primitives__hax__array_cons(x, s). +letfun alloc__vec__Impl_1__append(a: bitstring, b: bitstring) = array_extend(a, b). +fun alloc__vec__Impl_1__len(bitstring): bitstring. +fun core__slice__Impl__last(bitstring): bitstring. +(* `s[0]` -> head, `s[1..]` -> tail; other indices / opaque (byte-buffer) *) +(* operands fall back to an opaque accessor. *) +letfun core__ops__index__Index__index(s: bitstring, pos: bitstring) = + let (= nat_lit(0)) = pos in + (let rust_primitives__hax__array_cons(x, r) = s in x else array_index_opaque(s, pos)) + else let (= core__ops__range__RangeFrom__RangeFrom(nat_lit(1))) = pos in + (let rust_primitives__hax__array_cons(x, r) = s in r else array_index_opaque(s, pos)) + (* Fixed-offset split of a two-part concatenation: `s[..n]` -> first part, + `s[n..]` -> second part (the offset itself is abstracted away). *) + else let array_concat(a, b) = s in + (let core__ops__range__RangeFrom__RangeFrom(n) = pos in b else a) + else array_index_opaque(s, pos). +(* `dst.copy_from_slice(src)` overwrites `dst` with `src`: the `&mut self` + output becomes `src`. Used to thread a decrypted plaintext into a `&mut` + output buffer (e.g. `decrypt_aesgcm256`). *) +letfun core__slice__Impl__copy_from_slice(self: bitstring, src: bitstring) = src. +letfun core__slice__Impl__clone_from_slice(self: bitstring, src: bitstring) = src. + +(*****************************************************************) +(* More std prelude, surfaced once minos (not just mandrake) is *) +(* composed in. Same conventions: ADT variants are `[data]`, *) +(* Result/Option methods follow the transparent/structural model *) +(* above, byte<->int conversions are identity, and the remaining *) +(* Vec/slice ops are Seq stubs (workstream 2). *) +(*****************************************************************) + +(*** core::ops::ControlFlow — an ADT that survives some folds; pattern- ***) +(*** matched in bodies, so it must be `[data]`. ***) +fun core__ops__control_flow__ControlFlow__Break(bitstring): bitstring [data]. +fun core__ops__control_flow__ControlFlow__Continue(bitstring): bitstring [data]. + +(*** core::ops::range — remaining range bounds as data / unit const ***) +fun core__ops__range__Range__Range(bitstring, bitstring): bitstring [data]. +fun core__ops__range__RangeTo__RangeTo(bitstring): bitstring [data]. +const core__ops__range__RangeFull__RangeFull: bitstring. + +(*** core::num — opaque MAX const; be/le byte<->int reinterpretation is id ***) +const core__num__Impl_9__MAX: bitstring. +letfun core__num__Impl_7__from_be_bytes(x: bitstring) = x. +letfun core__num__Impl_7__to_be_bytes(x: bitstring) = x. + +(*** Option / Result — extra methods (see the transparent Result model). ***) +letfun core__option__Impl__unwrap_or(o: bitstring, d: bitstring) = + let Some(x) = o in x else d. +letfun core__result__Impl__expect(r: bitstring, m: bitstring) = r. +(* Under the transparent Result model a value reaching `is_ok`/`is_err` is the + bare `Ok` payload (treated as ok) unless it is an EXPLICIT `Err(_)` ctor. + Some boundaries (e.g. signature `verify`) must distinguish a real failure + from success WITHOUT killing the trace, so they return `Err(())` rather than + letting a destructor fail; these checks honor that `Err`. *) +letfun core__result__Impl__is_ok(r: bitstring) = + let core__result__Result__Err(e) = r in False() else True(). +letfun core__result__Impl__is_err(r: bitstring) = + let core__result__Result__Err(e) = r in True() else False(). +fun core__result__Impl__map(bitstring, bitstring): bitstring. (* closure apply — workstream 2 *) + +(*** str/slice — bytes view is identity; len is opaque (no arithmetic). ***) +letfun core__str__Impl__as_bytes(x: bitstring) = x. +fun core__slice__Impl__len(bitstring): bitstring. +fun core__iter__traits__exact_size__ExactSizeIterator__len(bitstring): bitstring. + +(*** Vec — `with_capacity` is an empty cons-list; `extend_from_slice` is Seq ***) +(*** append. `insert(s,0,x)` prepends and `remove(s,0)` peels the head — the ***) +(*** key/prefix wrappers (`hpke::add_prefix`/`drop_prefix`) use exactly these ***) +(*** at position 0, so they must cancel; other positions stay opaque. ***) +letfun alloc__vec__Impl__with_capacity(n: bitstring) = rust_primitives__hax__array_nil(). +letfun alloc__vec__Impl_1__insert_kw(s: bitstring, pos: bitstring, x: bitstring) = + let (= nat_lit(0)) = pos in rust_primitives__hax__array_cons(x, s) + else array_insert_opaque(s, pos, x). +(* `Vec::remove(&mut self, i) -> T` is functionalized to `(self_without_i, removed_i)`. *) +letfun alloc__vec__Impl_1__remove(s: bitstring, pos: bitstring) = + let (= nat_lit(0)) = pos in + (let rust_primitives__hax__array_cons(x, r) = s in + rust_primitives__hax__Tuple2__Tuple2(r, x) + else rust_primitives__hax__Tuple2__Tuple2(array_remove_rest(s, pos), array_index_opaque(s, pos))) + else rust_primitives__hax__Tuple2__Tuple2(array_remove_rest(s, pos), array_index_opaque(s, pos)). +letfun alloc__vec__Impl_2__extend_from_slice(a: bitstring, b: bitstring) = array_extend(a, b). diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/queries/enrollment.pv b/securedrop-protocol/protocol-minimal/proofs/proverif/queries/enrollment.pv new file mode 100644 index 00000000..8319fa1a --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/queries/enrollment.pv @@ -0,0 +1,84 @@ +(*****************************************************************) +(* enrollment.pv — M3: FPF -> Newsroom -> Journalist trust chain *) +(* *) +(* Trust model (api.rs handle_welcome / verify_long_term): *) +(* - FPF signing key is the public trust anchor. *) +(* - FPF signs the newsroom verifying key (domain fpf-sig-nr)*) +(* - the newsroom signs each journalist vk (domain nr-sig) *) +(* - the journalist self-signs its long-term keys (domain j-sig-ltk)*) +(* A client accepts a journalist only after checking the whole *) +(* chain. The Dolev-Yao attacker may mint its own journalist *) +(* keys and inject forged views, but lacks the newsroom key. *) +(* *) +(* Signatures use the REAL extracted `sign`/`verify`; domain *) +(* separation is modeled by signing/verifying the tagged message *) +(* (TAG, msg) — mirroring the code's `len(tag)||tag||msg` *) +(* preimage, with a distinct nullary TAG per domain. *) +(* *) +(* Property: ClientAcceptedJournalist(jvk) ==> the newsroom *) +(* actually signed jvk (no rogue journalist can be accepted). *) +(*****************************************************************) + +(* Distinct domain-separation tags (mirror sign.rs DomainTag impls). *) +const TAG_FPF_NR: bitstring. (* "fpf-sig-nr" *) +const TAG_NR_J: bitstring. (* "nr-sig" *) +const TAG_J_LTK: bitstring. (* "j-sig-ltk" *) + +event FpfSignedNewsroom(bitstring). (* nr_vk *) +event NewsroomSignedJournalist(bitstring). (* j_vk *) +event ClientAcceptedJournalist(bitstring). (* j_vk *) + +(* Sign / verify in a domain, via the extracted primitives. `ver` yields unit + only for a genuine signature (forgery has no value -> the `let` blocks). *) +letfun sig(sk: bitstring, tag: bitstring, msg: bitstring) = + securedrop_protocol_minimal__sign__Impl_10__sign(sk, + rust_primitives__hax__Tuple2__Tuple2(tag, msg)). +letfun ver(vk: bitstring, tag: bitstring, msg: bitstring, s: bitstring) = + securedrop_protocol_minimal__sign__Impl_11__verify(vk, + rust_primitives__hax__Tuple2__Tuple2(tag, msg), s). + +(* Property (rogue journalist can't be accepted). *) +query jvk: bitstring; + event(ClientAcceptedJournalist(jvk)) ==> event(NewsroomSignedJournalist(jvk)). + +(* Sanity: an honest journalist IS accepted (non-vacuous). *) +query jvk: bitstring; event(ClientAcceptedJournalist(jvk)). + +(* Honest enrollment: the trusted newsroom mints an honest journalist, who + self-signs its long-term keys; the newsroom signs the journalist vk. *) +let HonestEnrollment(nr_sk: bitstring) = + new j_sk: bitstring; + let j_vk = crypto__vk_of(j_sk) in + new ltk: bitstring; (* long-term key bytes (apke||fetch) *) + let selfsig = sig(j_sk, TAG_J_LTK, ltk) in + event NewsroomSignedJournalist(j_vk); + let nr_sig = sig(nr_sk, TAG_NR_J, j_vk) in + out(c, rust_primitives__hax__Tuple4__Tuple4(j_vk, ltk, selfsig, nr_sig)). + +(* Client: verify FPF's endorsement of the newsroom, then verify a journalist + long-term view against that newsroom (the api.rs verify_long_term checks). *) +let Client(fpf_vk: bitstring) = + in(c, nr_vk: bitstring); + in(c, fpf_sig: bitstring); + let ok_nr = ver(fpf_vk, TAG_FPF_NR, nr_vk, fpf_sig) in + in(c, rust_primitives__hax__Tuple4__Tuple4(j_vk: bitstring, ltk: bitstring, + selfsig: bitstring, nr_sig: bitstring)); + let ok_j = ver(nr_vk, TAG_NR_J, j_vk, nr_sig) in (* newsroom signed j_vk *) + let ok_lt = ver(j_vk, TAG_J_LTK, ltk, selfsig) in (* journalist self-signed ltk *) + event ClientAcceptedJournalist(j_vk). + +process + new fpf_sk: bitstring; + let fpf_vk = crypto__vk_of(fpf_sk) in + out(c, fpf_vk); (* trust anchor is public *) + new nr_sk: bitstring; + let nr_vk = crypto__vk_of(nr_sk) in + event FpfSignedNewsroom(nr_vk); (* FPF endorses THE honest newsroom *) + out(c, nr_vk); + out(c, sig(fpf_sk, TAG_FPF_NR, nr_vk)); + ( !HonestEnrollment(nr_sk) | !Client(fpf_vk) ) + +(* EXPECTPV +RESULT event(ClientAcceptedJournalist(jvk)) ==> event(NewsroomSignedJournalist(jvk)) is true. +RESULT not event(ClientAcceptedJournalist(jvk)) is false. +END *) diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/queries/enrollment_soundness.pv b/securedrop-protocol/protocol-minimal/proofs/proverif/queries/enrollment_soundness.pv new file mode 100644 index 00000000..d5b63de4 --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/queries/enrollment_soundness.pv @@ -0,0 +1,63 @@ +(*****************************************************************) +(* enrollment_soundness.pv — M3 sanity: the newsroom-signature *) +(* check in the trust chain is LOAD-BEARING. *) +(* *) +(* A BROKEN client that verifies only the journalist self-sig *) +(* (skipping the newsroom's signature over the journalist vk) *) +(* CAN be made to accept a rogue journalist that the newsroom *) +(* never signed. So the correspondence below is EXPECTED FALSE — *) +(* demonstrating that enrollment.pv's `is true` verdict is not *) +(* vacuous, and that removing the nr-sig check reintroduces the *) +(* rogue-journalist attack. *) +(*****************************************************************) + +const TAG_FPF_NR: bitstring. +const TAG_NR_J: bitstring. +const TAG_J_LTK: bitstring. + +event NewsroomSignedJournalist(bitstring). +event BrokenClientAccepted(bitstring). + +letfun sig(sk: bitstring, tag: bitstring, msg: bitstring) = + securedrop_protocol_minimal__sign__Impl_10__sign(sk, + rust_primitives__hax__Tuple2__Tuple2(tag, msg)). +letfun ver(vk: bitstring, tag: bitstring, msg: bitstring, s: bitstring) = + securedrop_protocol_minimal__sign__Impl_11__verify(vk, + rust_primitives__hax__Tuple2__Tuple2(tag, msg), s). + +(* EXPECTED FALSE: a rogue journalist (never newsroom-signed) is accepted. *) +query jvk: bitstring; + event(BrokenClientAccepted(jvk)) ==> event(NewsroomSignedJournalist(jvk)). + +let HonestEnrollment(nr_sk: bitstring) = + new j_sk: bitstring; + let j_vk = crypto__vk_of(j_sk) in + new ltk: bitstring; + let selfsig = sig(j_sk, TAG_J_LTK, ltk) in + event NewsroomSignedJournalist(j_vk); + let nr_sig = sig(nr_sk, TAG_NR_J, j_vk) in + out(c, rust_primitives__hax__Tuple4__Tuple4(j_vk, ltk, selfsig, nr_sig)). + +(* Broken: skips the `ver(nr_vk, TAG_NR_J, j_vk, nr_sig)` check. *) +let BrokenClient(fpf_vk: bitstring) = + in(c, nr_vk: bitstring); + in(c, fpf_sig: bitstring); + let ok_nr = ver(fpf_vk, TAG_FPF_NR, nr_vk, fpf_sig) in + in(c, rust_primitives__hax__Tuple4__Tuple4(j_vk: bitstring, ltk: bitstring, + selfsig: bitstring, nr_sig: bitstring)); + let ok_lt = ver(j_vk, TAG_J_LTK, ltk, selfsig) in (* ONLY the self-sig *) + event BrokenClientAccepted(j_vk). + +process + new fpf_sk: bitstring; + let fpf_vk = crypto__vk_of(fpf_sk) in + out(c, fpf_vk); + new nr_sk: bitstring; + let nr_vk = crypto__vk_of(nr_sk) in + out(c, nr_vk); + out(c, sig(fpf_sk, TAG_FPF_NR, nr_vk)); + ( !HonestEnrollment(nr_sk) | !BrokenClient(fpf_vk) ) + +(* EXPECTPV +RESULT event(BrokenClientAccepted(jvk)) ==> event(NewsroomSignedJournalist(jvk)) is false. +END *) diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/queries/fetch.pv b/securedrop-protocol/protocol-minimal/proofs/proverif/queries/fetch.pv new file mode 100644 index 00000000..655384da --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/queries/fetch.pv @@ -0,0 +1,79 @@ +(*****************************************************************) +(* fetch.pv — privacy-preserving message fetching (the DH clue) *) +(* *) +(* encrypt_decrypt.rs: a submission carries a hint (X = g^x, *) +(* Z = pk_R^x). The untrusted server, per fetch request, picks a *) +(* fresh eph and returns (pmgdh = X^eph, enc_id = AEAD_mk(id)) *) +(* with mk = Z^eph. The recipient (fetch secret r_sk, pk_R = *) +(* g^r_sk) recovers mk = pmgdh^r_sk and decrypts. A 3-party DH: *) +(* mk = g^(x·r_sk·eph). Because Z = pk_R^x BLINDS pk_R, the *) +(* server never learns the recipient. *) +(* *) +(* Modeling note: hax's `crypto__dh_shared` (a 2-party op) cannot *) +(* express the nested 3-party exponentiation, and ProVerif does *) +(* not terminate on the general exp-commutativity equation here. *) +(* So the clue is modeled with dedicated constructors whose single *) +(* correctness `reduc` captures exactly the recipient==server key *) +(* agreement — deterministic for ProVerif. AEAD reuses cryptolib. *) +(* *) +(* This file: functional correctness + wrong-recipient secrecy. *) +(* Recipient anonymity (unlinkability) is in fetch_unlink.pv. *) +(*****************************************************************) + +fun gen(bitstring): bitstring. (* r_sk -> pk_R = g^r_sk *) +fun cluex(bitstring): bitstring. (* x -> X = g^x *) +fun cluez(bitstring, bitstring): bitstring. (* pk, x -> Z = pk^x *) +fun srvp(bitstring, bitstring): bitstring. (* X, eph -> pmgdh = X^eph *) +fun srvk(bitstring, bitstring): bitstring. (* Z, eph -> mk (server side) = Z^eph *) +(* Recipient recovers the server's mk from pmgdh + its fetch secret. This ONE rule + is the 3-party DH agreement: pmgdh^r_sk = Z^eph exactly when Z = (g^r_sk)^x. *) +reduc forall r_sk: bitstring, x: bitstring, eph: bitstring; + reck(srvp(cluex(x), eph), r_sk) = srvk(cluez(gen(r_sk), x), eph). + +free MESSAGE_ID: bitstring [private]. (* the server's id for A's stored message *) +event GotA(bitstring). (* intended recipient recovered an id *) +event GotB(bitstring). (* a DIFFERENT recipient recovered an id *) + +(* Correctness: the intended recipient A recovers the ACTUAL message id (reachable). *) +query event(GotA(MESSAGE_ID)). +(* Wrong-recipient secrecy: B (message addressed to A) NEVER recovers A's message id. *) +query event(GotB(MESSAGE_ID)). +(* Message-id confidentiality: a network eavesdropper never learns it either. *) +query attacker(MESSAGE_ID). + +(* One honest message stored for A. `MESSAGE_ID` is the server's id for THIS entry + (each stored entry has its own id; the attacker submitting other entries just gets + its own ids back — irrelevant to A's id). The server re-derives the fetch challenge + with a fresh per-request `eph`, so `!Serve` models repeated fetch requests. *) +let Serve(bigX: bitstring, bigZ: bitstring) = + new eph: bitstring; + out(c, (srvp(bigX, eph), crypto__aead_enc(srvk(bigZ, eph), MESSAGE_ID, empty))). + +let RecipientA(r_sk: bitstring) = + in(c, ch: bitstring); + let (p: bitstring, e: bitstring) = ch in + let id = crypto__aead_dec(reck(p, r_sk), e, empty) in + event GotA(id). + +let RecipientB(r_sk: bitstring) = + in(c, ch: bitstring); + let (p: bitstring, e: bitstring) = ch in + let id = crypto__aead_dec(reck(p, r_sk), e, empty) in + event GotB(id). + +process + new r_sk_A: bitstring; new r_sk_B: bitstring; + let pk_A = gen(r_sk_A) in + let pk_B = gen(r_sk_B) in + out(c, pk_A); out(c, pk_B); + new x: bitstring; (* source's ephemeral for the hint *) + let bigX = cluex(x) in + let bigZ = cluez(pk_A, x) in + out(c, bigX); out(c, bigZ); (* the hint (X, Z) is stored on the untrusted server *) + ( !Serve(bigX, bigZ) | RecipientA(r_sk_A) | RecipientB(r_sk_B) ) + +(* EXPECTPV +RESULT not event(GotA(MESSAGE_ID[])) is false. +RESULT not event(GotB(MESSAGE_ID[])) is true. +RESULT not attacker(MESSAGE_ID[]) is true. +END *) diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/queries/fetch_unlink.pv b/securedrop-protocol/protocol-minimal/proofs/proverif/queries/fetch_unlink.pv new file mode 100644 index 00000000..ae299f06 --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/queries/fetch_unlink.pv @@ -0,0 +1,44 @@ +(*****************************************************************) +(* fetch_unlink.pv — recipient anonymity / unlinkability *) +(* *) +(* The privacy goal of the DH fetch clue: the UNTRUSTED SERVER *) +(* (and any network eavesdropper) cannot tell WHICH recipient a *) +(* stored message is addressed to. Because the hint Z = pk_R^x *) +(* blinds pk_R with the source's fresh x, a message for A is *) +(* indistinguishable from one for B. *) +(* *) +(* Modeled as ProVerif observational equivalence (diff- *) +(* equivalence): the biprocess submits to `choice[pk_A, pk_B]` and *) +(* the attacker observes the stored hint (X, Z) plus every fetch *) +(* challenge (pmgdh, enc_id). If the two sides are equivalent, the *) +(* server learns nothing about the recipient. *) +(* *) +(* Recipients are NOT run here: unlinkability is about what the *) +(* server/eavesdropper sees, not about a recipient's own decrypt. *) +(* Same clue/DH constructors as fetch.pv (defined inline). *) +(*****************************************************************) + +fun gen(bitstring): bitstring. +fun cluex(bitstring): bitstring. +fun cluez(bitstring, bitstring): bitstring. +fun srvp(bitstring, bitstring): bitstring. +fun srvk(bitstring, bitstring): bitstring. + +free MID: bitstring [private]. (* the stored message's id (same content, differing recipient) *) + +process + new r_sk_A: bitstring; new r_sk_B: bitstring; + let pk_A = gen(r_sk_A) in + let pk_B = gen(r_sk_B) in + out(c, pk_A); out(c, pk_B); (* both recipients' fetch pubkeys are public *) + new x: bitstring; (* source's fresh ephemeral *) + let bigX = cluex(x) in + let bigZ = cluez(choice[pk_A, pk_B], x) in (* addressed to A vs B *) + out(c, bigX); out(c, bigZ); (* the stored hint (X, Z) *) + (* the server re-derives the fetch challenge with a fresh eph per request *) + ! ( new eph: bitstring; + out(c, (srvp(bigX, eph), crypto__aead_enc(srvk(bigZ, eph), MID, empty))) ) + +(* EXPECTPV +RESULT Observational equivalence is true. +END *) diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/queries/reply.pv b/securedrop-protocol/protocol-minimal/proofs/proverif/queries/reply.pv new file mode 100644 index 00000000..14908fcc --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/queries/reply.pv @@ -0,0 +1,69 @@ +(*****************************************************************) +(* reply.pv — journalist -> source reply *) +(* *) +(* The reply direction reuses the SAME extracted *) +(* `encrypt_decrypt::encrypt`, with the journalist as sender and *) +(* the source (via its reply keys) as recipient. The source's *) +(* reply keys are public (carried in its submission), so the *) +(* reply's secrecy rests on the source's SECRET keys. *) +(* *) +(* Properties (mirroring submission.pv, roles swapped): *) +(* 2. Reply confidentiality — attacker cannot learn the reply. *) +(* Journalist authentication — if the source accepts reply m *) +(* as from journalist j, the journalist really sent it. *) +(* Sanity — the honest source receives the reply. *) +(*****************************************************************) + +event JournalistReplied(bitstring, bitstring). (* pt_bytes, journalist_apke_pk *) +event SourceReceivedReply(bitstring, bitstring). (* pt_bytes, recovered journalist_apke_pk *) + +free SECRET_REPLY: bitstring [private]. + +(* 2. Reply confidentiality. *) +query attacker(SECRET_REPLY). + +(* Journalist authentication of the reply (non-injective agreement). *) +query m: bitstring, j: bitstring; + event(SourceReceivedReply(m, j)) ==> event(JournalistReplied(m, j)). + +(* Sanity: the honest source receives the reply (non-vacuous). *) +query m: bitstring, j: bitstring; event(SourceReceivedReply(m, j)). + +(* Honest journalist: replies to the source's public view with its long-term + reply APKE key. (A journalist's own reply plaintext carries no reply keys, so + the other plaintext fields are irrelevant placeholders here.) *) +let JournalistReply(journalist: bitstring, source_pub: bitstring, ph1: bitstring, ph2: bitstring) = + new rng: bitstring; + let pt = securedrop_protocol_minimal__ciphertext__Plaintext__Plaintext( + ph1, ph2, SECRET_REPLY) in + let pt_bytes = securedrop_protocol_minimal__ciphertext__Impl_1__to_bytes(pt) in + event JournalistReplied(pt_bytes, + securedrop_protocol_minimal__traits__UserSecret__own_message_auth_pk(journalist)); + let rust_primitives__hax__Tuple2__Tuple2(rng2, env) = + securedrop_protocol_minimal__encrypt_decrypt__encrypt(rng, journalist, pt, source_pub) in + out(c, env). + +(* Honest source: runs the FULL extracted receive (`decrypt` = `decrypt_with_sender`) + — recovers the journalist's reply APKE key from the metadata, then SD-APKE.AuthDec. *) +let SourceReceive(source: bitstring) = + in(c, env: bitstring); + let rust_primitives__hax__Tuple2__Tuple2(pt, j_apke_pk) = + securedrop_protocol_minimal__encrypt_decrypt__decrypt_with_sender(source, env) in + event SourceReceivedReply(pt, j_apke_pk). + +process + new j_apke_sk: bitstring; new j_fetch_sk: bitstring; new j_meta_sk: bitstring; + new s_apke_sk: bitstring; new s_fetch_sk: bitstring; new s_meta_sk: bitstring; + new ph1: bitstring; new ph2: bitstring; + let journalist = sd_secret(j_apke_sk, j_fetch_sk, j_meta_sk) in + (* source reply view: the source's long-term APKE key, fetch key, metadata key *) + let source_pub = sd_public( + sd_apke__pk(s_apke_sk), crypto__dh_pub(s_fetch_sk), sd_pke__pk(s_meta_sk)) in + ( JournalistReply(journalist, source_pub, ph1, ph2) + | SourceReceive(sd_journalist(s_apke_sk, s_meta_sk, s_fetch_sk)) ) + +(* EXPECTPV +RESULT not attacker(SECRET_REPLY[]) is true. +RESULT event(SourceReceivedReply(m_11,j)) ==> event(JournalistReplied(m_11,j)) is true. +RESULT not event(SourceReceivedReply(m_11,j)) is false. +END *) diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/queries/submission.pv b/securedrop-protocol/protocol-minimal/proofs/proverif/queries/submission.pv new file mode 100644 index 00000000..91770a99 --- /dev/null +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/queries/submission.pv @@ -0,0 +1,70 @@ +(*****************************************************************) +(* submission.pv — M2: source -> journalist submission *) +(* *) +(* Drives the ACTUAL extracted `encrypt_decrypt::encrypt` (which *) +(* composes SD-APKE auth_enc + SD-PKE metadata + the DH fetch *) +(* hint) with an honest source and an honest journalist, and *) +(* models the journalist's receive with the extracted primitives *) +(* (metadata::decrypt to recover the sender key, then auth_dec). *) +(* *) +(* Properties: *) +(* 1. Submission confidentiality — attacker cannot learn the msg.*) +(* 3. Sender authentication — if the journalist accepts msg m as *) +(* from sender s, the source really sent m as s (SD-APKE *) +(* implicit authentication). *) +(* 5. Sanity — the honest run reaches the receive (not vacuous). *) +(*****************************************************************) + +event SourceSubmitted(bitstring, bitstring). (* pt_bytes, sender_apke_pk *) +event JournalistReceived(bitstring, bitstring). (* pt_bytes, recovered sender_apke_pk *) + +free SECRET_SUBMISSION: bitstring [private]. + +(* 1. Submission confidentiality. *) +query attacker(SECRET_SUBMISSION). + +(* 3. Sender authentication (non-injective agreement). *) +query m: bitstring, s: bitstring; + event(JournalistReceived(m, s)) ==> event(SourceSubmitted(m, s)). + +(* 5. Sanity / reachability: the honest receive is reachable. *) +query m: bitstring, s: bitstring; event(JournalistReceived(m, s)). + +(* Honest source: builds a plaintext carrying SECRET_SUBMISSION, records the + submission, then runs the extracted encrypt over its keys + the recipient view. *) +let Source(source: bitstring, recipient_pub: bitstring, reply_pk: bitstring, fetch_key: bitstring) = + new rng: bitstring; + let pt = securedrop_protocol_minimal__ciphertext__Plaintext__Plaintext( + reply_pk, fetch_key, SECRET_SUBMISSION) in + let pt_bytes = securedrop_protocol_minimal__ciphertext__Impl_1__to_bytes(pt) in + event SourceSubmitted(pt_bytes, + securedrop_protocol_minimal__traits__UserSecret__own_message_auth_pk(source)); + let rust_primitives__hax__Tuple2__Tuple2(rng2, env) = + securedrop_protocol_minimal__encrypt_decrypt__encrypt(rng, source, pt, recipient_pub) in + out(c, env). + +(* Honest journalist: runs the FULL extracted `decrypt_with_sender` — trial-decrypt + over its key bundles to find the matching one, recover the sender's APKE key from + the metadata, then SD-APKE.AuthDec (binds sender identity). Records the receive. *) +let Journalist(journalist: bitstring) = + in(c, env: bitstring); + let rust_primitives__hax__Tuple2__Tuple2(pt, sender_apke_pk) = + securedrop_protocol_minimal__encrypt_decrypt__decrypt_with_sender(journalist, env) in + event JournalistReceived(pt, sender_apke_pk). + +process + new skS_apke: bitstring; new skS_fetch: bitstring; new skS_meta: bitstring; + new skR_apke: bitstring; new skR_fetch: bitstring; new skR_meta: bitstring; + new reply_pk: bitstring; new fetch_key: bitstring; + let source = sd_secret(skS_apke, skS_fetch, skS_meta) in + (* recipient view = journalist ephemeral enc key, fetch key, metadata key *) + let recipient_pub = sd_public( + sd_apke__pk(skR_apke), crypto__dh_pub(skR_fetch), sd_pke__pk(skR_meta)) in + ( Source(source, recipient_pub, reply_pk, fetch_key) + | Journalist(sd_journalist(skR_apke, skR_meta, skR_fetch)) ) + +(* EXPECTPV +RESULT not attacker(SECRET_SUBMISSION[]) is true. +RESULT event(JournalistReceived(m_11,s)) ==> event(SourceSubmitted(m_11,s)) is true. +RESULT not event(JournalistReceived(m_11,s)) is false. +END *) diff --git a/securedrop-protocol/protocol-minimal/src/ciphertext.rs b/securedrop-protocol/protocol-minimal/src/ciphertext.rs index 99db4579..a1687fb5 100644 --- a/securedrop-protocol/protocol-minimal/src/ciphertext.rs +++ b/securedrop-protocol/protocol-minimal/src/ciphertext.rs @@ -85,6 +85,9 @@ pub struct Plaintext { } impl Plaintext { + // ProVerif: the plaintext is carried as an atomic term; to_bytes/from_bytes are + // identity so it round-trips through encrypt -> auth_enc/auth_dec -> decrypt. + #[cfg_attr(hax_backend_proverif, hax_lib::proverif::replace_body("self"))] pub fn to_bytes(&self) -> alloc::vec::Vec { // TODO: Deviates from spec let mut buf = Vec::new(); @@ -101,6 +104,7 @@ impl Plaintext { } // Toy parsing only + #[cfg_attr(hax_backend_proverif, hax_lib::proverif::replace_body("pt_bytes"))] pub fn from_bytes(pt_bytes: &[u8]) -> Result { let mut offset = 0; diff --git a/securedrop-protocol/protocol-minimal/src/keys.rs b/securedrop-protocol/protocol-minimal/src/keys.rs index 8f9bbae0..b80d299a 100644 --- a/securedrop-protocol/protocol-minimal/src/keys.rs +++ b/securedrop-protocol/protocol-minimal/src/keys.rs @@ -55,6 +55,9 @@ impl KeyBundlePublic { } } +// ProVerif: modeled in the harness (proofs/proverif/handwritten/sd_model.pvl) so the +// receiver's key-bundle machinery lives entirely there (avoids a lib<->model cycle). +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] pub(crate) struct MessageKeyBundle { pub(crate) apke: MessageKeyPair, pub(crate) metadata_kp: MetadataKeyPair, diff --git a/securedrop-protocol/protocol-minimal/src/message.rs b/securedrop-protocol/protocol-minimal/src/message.rs index d6592c37..71999fa0 100644 --- a/securedrop-protocol/protocol-minimal/src/message.rs +++ b/securedrop-protocol/protocol-minimal/src/message.rs @@ -53,6 +53,9 @@ const LEN_MLKEM_ENCAPS_RAND: usize = 32; /// /// - `pk1`: DHKEM(X25519) component (`pk^AKEM`) /// - `pk2`: ML-KEM-768 component (`pk^PQ`) +// ProVerif: SD-APKE key tuple is an atomic public key `sd_apke__pk(sk)` in the +// symbolic model (see proofs/proverif/handwritten/sd_crypto.pvl). +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] #[derive(Debug, Clone)] pub struct MessagePublicKey { pub(crate) dhakem: DhAkemPublicKey, // pk1 in spec @@ -63,12 +66,14 @@ pub struct MessagePublicKey { /// /// - `sk1`: DHKEM(X25519) component (`sk^AKEM`) /// - `sk2`: ML-KEM-768 component (`sk^PQ`) +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] pub struct MessagePrivateKey { pub(crate) dhakem: DhAkemPrivateKey, // sk1 in spec pub(crate) mlkem: MLKEM768PrivateKey, // sk2 in spec } /// A `(MessagePrivateKey, MessagePublicKey)` SD-APKE keypair. +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] pub struct MessageKeyPair { sk: MessagePrivateKey, pk: MessagePublicKey, @@ -104,6 +109,8 @@ impl MessagePublicKey { /// # Errors /// /// Returns an error if the byte slice has incorrect length. + // ProVerif: the APKE public key is atomic (opaque), so serialize/parse is identity. + #[cfg_attr(hax_backend_proverif, hax_lib::proverif::replace_body("bytes"))] pub fn from_bytes(bytes: &[u8]) -> Result { use crate::primitives::dh_akem::DH_AKEM_PUBLIC_KEY_LEN; use crate::primitives::mlkem::MLKEM768_PUBLIC_KEY_LEN; @@ -147,6 +154,7 @@ impl<'de> serde::Deserialize<'de> for MessagePublicKey { } /// SD-APKE ciphertext `((c1, cp), c2)`. +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] #[derive(Debug, Clone)] pub struct MessageCiphertext { /// HPKE encapsulation output (`c1` in the spec) @@ -264,6 +272,13 @@ pub(crate) fn deterministic_keygen( /// # Errors /// /// Returns an error if ML-KEM encapsulation or HPKE sealing fails. +// ProVerif: SD-APKE.AuthEnc is modeled atomically (HPKE-AuthPsk = DH-AKEM sender +// auth + ML-KEM PSK) by the symbolic primitive `sd_apke__authenc`. Fresh KEM +// randomness is drawn inside the letfun, so `rng` is dropped. +#[cfg_attr( + hax_backend_proverif, + hax_lib::proverif::replace_body("sd_apke__authenc(sk, pk, m, ad, info)") +)] pub fn auth_enc( rng: &mut R, sk: &MessagePrivateKey, // (skS1, skS2) @@ -320,6 +335,13 @@ pub fn auth_enc( /// # Errors /// /// Returns an error if ML-KEM decapsulation or HPKE opening fails. +// ProVerif: partial inverse of `sd_apke__authenc`. Succeeds only for a ciphertext +// produced by the matching sender `pk` and recipient `sk` (binds sender identity — +// SD-APKE implicit authentication). +#[cfg_attr( + hax_backend_proverif, + hax_lib::proverif::replace_body("sd_apke__authdec(sk, pk, ct, ad, info)") +)] pub fn auth_dec( sk: &MessagePrivateKey, // (skR1, skR2) pk: &MessagePublicKey, // (pkS1, pkS2) diff --git a/securedrop-protocol/protocol-minimal/src/metadata.rs b/securedrop-protocol/protocol-minimal/src/metadata.rs index 8c6c726d..d326992b 100644 --- a/securedrop-protocol/protocol-minimal/src/metadata.rs +++ b/securedrop-protocol/protocol-minimal/src/metadata.rs @@ -34,13 +34,17 @@ use crate::primitives::xwing::{ pub(crate) const LEN_METADATA_CIPHERTEXT: usize = 1232; /// The recipient's metadata public key (`pk_R^PKE` in the spec). +// ProVerif: atomic public key `sd_pke__pk(sk)` (see handwritten/sd_crypto.pvl). +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] #[derive(Debug, Clone)] pub struct MetadataPublicKey(pub(crate) XWingPublicKey); /// The recipient's metadata private key (`sk_R^PKE` in the spec). +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] pub struct MetadataPrivateKey(pub(crate) XWingPrivateKey); /// A `(MetadataPrivateKey, MetadataPublicKey)` SD-PKE keypair. +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] pub struct MetadataKeyPair { sk: MetadataPrivateKey, pk: MetadataPublicKey, @@ -81,6 +85,7 @@ impl MetadataKeyPair { /// SD-PKE ciphertext `(c, c')`: X-Wing encapsulation `c` together with HPKE /// ciphertext `c'`. +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] #[derive(Debug, Clone)] pub struct MetadataCiphertext { /// HPKE encapsulation output (`c` in the spec) @@ -226,6 +231,12 @@ impl MetadataPrivateKey { /// SD-PKE.Enc: encrypt message `m` to recipient key `pk_r`, returning `(c, c')`. /// /// `m` is the sender's long-term APKE public key, which must be serializable. +// ProVerif: SD-PKE (HPKE-Base over X-Wing) modeled as a public-key encryption +// primitive `sd_pke__enc` (confidentiality only; no sender auth). +#[cfg_attr( + hax_backend_proverif, + hax_lib::proverif::replace_body("sd_pke__enc(pk_r, m)") +)] pub(crate) fn encrypt( pk_r: &MetadataPublicKey, m: &MessagePublicKey, @@ -260,6 +271,10 @@ pub(crate) fn encrypt( /// # Errors /// /// Returns an error if HPKE decryption fails. +#[cfg_attr( + hax_backend_proverif, + hax_lib::proverif::replace_body("sd_pke__dec(sk_r, ct)") +)] pub fn decrypt( sk_r: &MetadataPrivateKey, ct: &MetadataCiphertext, diff --git a/securedrop-protocol/protocol-minimal/src/primitives/x25519.rs b/securedrop-protocol/protocol-minimal/src/primitives/x25519.rs index f501ae8d..b47e4693 100644 --- a/securedrop-protocol/protocol-minimal/src/primitives/x25519.rs +++ b/securedrop-protocol/protocol-minimal/src/primitives/x25519.rs @@ -11,10 +11,13 @@ pub(crate) const DH_SHARED_SECRET_LEN: usize = crate::primitives::provider::curve25519::LEN_DH_SHARE; /// An X25519 public key. +// ProVerif: atomic DH element; `pk = crypto__dh_pub(sk)`. into_bytes is identity. +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] #[derive(Debug, Clone, Copy)] pub struct DHPublicKey([u8; DH_PUBLIC_KEY_LEN]); impl DHPublicKey { + #[cfg_attr(hax_backend_proverif, hax_lib::proverif::replace_body("self"))] pub fn into_bytes(self) -> [u8; DH_PUBLIC_KEY_LEN] { self.0 } @@ -42,14 +45,17 @@ impl<'de> serde::Deserialize<'de> for DHPublicKey { } /// An X25519 private key. +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] #[derive(Debug, Clone)] pub struct DHPrivateKey([u8; DH_PRIVATE_KEY_LEN]); impl DHPrivateKey { + #[cfg_attr(hax_backend_proverif, hax_lib::proverif::replace_body("self"))] pub fn as_bytes(&self) -> &[u8; DH_PRIVATE_KEY_LEN] { &self.0 } + #[cfg_attr(hax_backend_proverif, hax_lib::proverif::replace_body("self"))] pub fn into_bytes(self) -> [u8; DH_PRIVATE_KEY_LEN] { self.0 } @@ -60,10 +66,12 @@ impl DHPrivateKey { } /// An X25519 shared secret. +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] #[derive(Debug, Clone)] pub struct DHSharedSecret([u8; 32]); impl DHSharedSecret { + #[cfg_attr(hax_backend_proverif, hax_lib::proverif::replace_body("self"))] pub fn into_bytes(self) -> [u8; 32] { self.0 } @@ -86,6 +94,13 @@ pub fn deterministic_dh_keygen(randomness: [u8; 32]) -> Result<(DHPrivateKey, DH } /// Generate a new DH key pair using X25519 +// ProVerif: fresh scalar `sk`; public key is `crypto__dh_pub(sk)`. +#[cfg_attr( + hax_backend_proverif, + hax_lib::proverif::replace_body( + "new x25519_sk: bitstring; rust_primitives__hax__Tuple2__Tuple2(x25519_sk, crypto__dh_pub(x25519_sk))" + ) +)] pub fn generate_dh_keypair( rng: &mut R, ) -> Result<(DHPrivateKey, DHPublicKey), Error> { @@ -140,6 +155,11 @@ pub fn dh_public_key_from_scalar(scalar: [u8; 32]) -> DHPublicKey { } /// Compute DH shared secret +// ProVerif: `crypto__dh_shared(sk, pk)` with the standard commutativity equation. +#[cfg_attr( + hax_backend_proverif, + hax_lib::proverif::replace_body("crypto__dh_shared(private_scalar, public_key)") +)] pub fn dh_shared_secret( public_key: &DHPublicKey, private_scalar: [u8; 32], diff --git a/securedrop-protocol/protocol-minimal/src/sign.rs b/securedrop-protocol/protocol-minimal/src/sign.rs index 545667b1..2854b93c 100644 --- a/securedrop-protocol/protocol-minimal/src/sign.rs +++ b/securedrop-protocol/protocol-minimal/src/sign.rs @@ -83,6 +83,7 @@ impl DomainTag for FpfOnNewsroom { /// A `Signature` can only be verified against a message using the same /// domain `D`, making cross-domain misuse a compile error rather than a /// runtime failure. +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] pub struct Signature { bytes: [u8; 64], // `PhantomData` rather than `PhantomData D>`: the function type @@ -165,10 +166,13 @@ fn tagged_preimage(msg: &[u8]) -> Vec { } /// An Ed25519 verification key. +// ProVerif: `vk = crypto__vk_of(sk)` in the symbolic model. +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] #[derive(Copy, Clone)] pub struct VerifyingKey([u8; KEY_LEN_ED25519]); /// An Ed25519 signing key. +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] pub(crate) struct SigningSecretKey([u8; KEY_LEN_ED25519]); impl VerifyingKey { @@ -191,6 +195,7 @@ impl SigningSecretKey { } } +#[cfg_attr(hax_backend_proverif, hax_lib::opaque)] pub struct SigningKey { pub vk: VerifyingKey, sk: SigningSecretKey, @@ -231,6 +236,13 @@ impl SigningKey { /// Sign `msg` in domain `D`, returning a `Signature`. /// /// The actual preimage is `len(tag) || tag || msg` where `tag = D::TAG`. + // ProVerif: EUF-CMA signature `crypto__sign(sk, msg)`. NOTE (M3): the type-level + // domain separator `D` is not yet reflected in the symbolic term; add the tag to + // the signed message when modeling the enrollment trust chain. + #[cfg_attr( + hax_backend_proverif, + hax_lib::proverif::replace_body("crypto__sign(self, msg)") + )] pub fn sign(&self, msg: &[u8]) -> Signature { let preimage = tagged_preimage::(msg); let bytes = provider::ed25519::sign(&preimage, self.sk.as_bytes()); @@ -260,6 +272,12 @@ impl VerifyingKey { /// Verify `sig` over `msg`. The domain is determined by the type of `sig`. /// /// Returns an error if the signature is invalid. + // ProVerif: `crypto__sig_verify(vk, msg, sig)` reduces to unit only for a genuine + // signature under the matching key (forgery has no value -> propagates as `Err`). + #[cfg_attr( + hax_backend_proverif, + hax_lib::proverif::replace_body("crypto__sig_verify(self, msg, sig)") + )] pub fn verify(&self, msg: &[u8], sig: &Signature) -> Result<(), Error> { let preimage = tagged_preimage::(msg); provider::ed25519::verify(&preimage, self.as_bytes(), &sig.bytes) From c63e7d118212209b0776f1e8884902ec4b988d6b Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Tue, 14 Jul 2026 15:11:58 +0200 Subject: [PATCH 2/6] docs(proverif): concrete two-level reproduction + toolchain pins MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Level 1 (public tools only): `make proverif-check` re-runs all 13 verdicts against the committed, SHA-pinned model snapshot — needs only ProVerif 2.05. Level 2 (re-derive from Rust): needs the unmerged hax ProVerif backend (cryspen/hax @ proverif-rust-backend, PR #2068, commit 637fc91499). Co-Authored-By: Claude Opus 4.8 (1M context) --- .../proofs/proverif/VERIFICATION.md | 59 +++++++++++++++---- 1 file changed, 49 insertions(+), 10 deletions(-) diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md b/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md index 839c1a02..23c1b2d8 100644 --- a/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md @@ -203,16 +203,55 @@ functional correctness / panic-freedom (the F\* track). --- -## 6. Reproducibility & pins - -- **ProVerif** — any recent 2.0x (developed against the `hax-proverif` opam switch's build). -- **hax ProVerif backend** — the `hax-proverif` opam switch / a `~/hax-proverif-backend` - checkout (draft PR cryspen/hax#2068). Only needed to **re-extract** (`make - proverif-extract`); the engine-free `make proverif-check` needs only `proverif`. -- **`hax-lib`** — crates.io `0.3.7` for normal builds; the dev `hax-lib` (with the - `cfg(hax_backend_proverif)`-gated macros) is injected at extraction time via - `cargo --config`, never as a committed patch, so `cargo build` / CI / F\* are unaffected. -- **CI** — `.github/workflows/proverif.yml` runs the engine-free lane on every push. +## 6. Reproducing the results + +There are two levels. **Level 1 needs only public tools; Level 2 additionally needs the +(public but unreleased) hax ProVerif backend.** + +### Level 1 — re-check the verdicts (public tools only, no hax) + +The generated model (`extraction/lib.pvl`, SHA-pinned in `extraction/lib.pvl.sha256`), the +vendored symbolic libraries (`lib/{primitives,cryptolib}.pvl`), the SecureDrop crypto model +(`handwritten/*.pvl`), and every query (`queries/*.pv`) are all committed. So ProVerif +alone re-checks all 13 properties: + +```sh +opam install proverif # ProVerif 2.05 (public, INRIA); or install it any other way +# from the crate root: securedrop-protocol/protocol-minimal +make proverif-check # runs reconstruct-proverif (digest check) + all queries +``` + +`make proverif-check` invokes `proverif` directly (no opam switch, no hax); if `proverif` +is only reachable via opam, use `opam exec -- make proverif-check`. This is exactly what +`.github/workflows/proverif.yml` runs on every push. Trusting (or auditing) the committed +`lib.pvl` — which carries `(* src: : ... *)` provenance comments and a +`lib.pvl.map` source map back to the Rust — is all Level 1 requires. + +### Level 2 — re-derive the model from the Rust (needs the hax backend) + +To regenerate `lib.pvl` from the Rust source rather than trust the committed snapshot: + +- Build the hax ProVerif backend from **`github.com/cryspen/hax`, branch + `proverif-rust-backend`** (draft PR **#2068**; engine used here: commit + **`637fc91499`**). This backend is **not merged upstream and not a released tool** — it + must be built from that branch (it prints `Experimental backend "proverif" is work in + progress`). See that repo's `setup-local.sh` (installs into a `hax-proverif` opam switch) + or `setup-hax.sh` (opam-free source build). +- Point `HAX_PROVERIF_DIR` at that checkout and run `make proverif-extract`, then + `make proverif-check`. Extraction rewrites `lib.pvl` and re-pins its digest; a faithful + re-extraction leaves the committed model unchanged. + +### Pins + +- **ProVerif** — 2.05. +- **hax ProVerif backend** — `cryspen/hax` @ `proverif-rust-backend` (PR #2068), engine + commit `637fc91499`. Vendored `lib/*.pvl` are byte-copies from that tree + (`hax-lib/proof-libs/proverif/`); see `lib/PROVENANCE.md`. +- **`hax-lib`** — crates.io `0.3.7` for normal builds; the dev `hax-lib` carrying the + `cfg(hax_backend_proverif)`-gated macros is injected at extraction time via + `cargo --config` (not a committed patch), so `cargo build` / CI / F\* are unaffected. +- **CI** — `.github/workflows/proverif.yml` runs Level 1 on every push (installs ProVerif + via opam; no hax build). ## 7. Integrity guarantees of this change From 26aea20dec9507502e32fdf2a3c80a5f75341f29 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Tue, 14 Jul 2026 15:39:45 +0200 Subject: [PATCH 3/6] proverif: extract sign/verify + tagged_preimage; correct fidelity docs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lower the abstraction boundary for signatures: the Ed25519 leaf moves to provider::ed25519::{sign,verify} (crypto__sign / crypto__sig_verify), so SigningKey::sign / VerifyingKey::verify and the domain-separated preimage (tagged_preimage: len||tag||msg) are now EXTRACTED real Rust rather than atomic replace_body redirects. Caveat (documented): the backend erases the generic DomainTag's type parameter, collapsing the four signature domains to one tag, so domain SEPARATION stays harness-side. Suite unchanged (13/13 green). Also correct VERIFICATION.md §5a to distinguish (i) extracted-as-composition (encrypt, decrypt_with_sender, sign/verify) from (ii) leaf-abstracted crypto (SD-APKE/SD-PKE atomic, ed25519/x25519 leaves) from (iii) harness-modeled, and scope the SD-APKE/SD-PKE leaf-boundary-lowering work (probe: ~10 clean leaves). Co-Authored-By: Claude Opus 4.8 (1M context) --- .../protocol-minimal/proofs/proverif/PLAN.md | 21 ++++++- .../proofs/proverif/VERIFICATION.md | 59 +++++++++++++----- .../proofs/proverif/extraction/lib.pvl | 62 +++++++++++++++++-- .../proofs/proverif/extraction/lib.pvl.sha256 | 2 +- .../proofs/proverif/handwritten/sd_model.pvl | 8 +++ .../src/primitives/provider.rs | 14 ++++- .../protocol-minimal/src/sign.rs | 34 +++++----- 7 files changed, 160 insertions(+), 40 deletions(-) diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/PLAN.md b/securedrop-protocol/protocol-minimal/proofs/proverif/PLAN.md index 450eca4b..acdb221a 100644 --- a/securedrop-protocol/protocol-minimal/proofs/proverif/PLAN.md +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/PLAN.md @@ -344,7 +344,26 @@ Engine discovery: prefer the `hax-proverif` opam switch; honor `HAX_PROVERIF_DIR `missingdecl` filter (also drops names defined by the vendored libs, e.g. reduc-defined `Tuple2__0/1`). `missingdecl` stays clean; suite still **13/13**. The backend auto-unrolls the trial-decrypt loop (fixed bound 3; a single-bundle journalist uses the first iteration). -- HPKE-AuthPsk decomposition; migrate `replace_body`→`pv_model` when the tracing backend lands. +### Lowering the leaf boundary (extract more, abstract only leaf crypto + serialization) +Goal: only abstract true leaf crypto (HPKE, ML-KEM, X-Wing, Ed25519, X25519, ChaCha20, +HKDF) and serialization; extract the compositions above them. +- **`sign`/`verify` + `tagged_preimage`. ✅ DONE (2026-07-14).** Leaf moved to + `provider::ed25519::{sign,verify}` (`crypto__sign`/`crypto__sig_verify`); the + domain-separated preimage composition is now extracted real Rust. Caveat: the backend + erases the generic `DomainTag`'s `D`, collapsing the four domains to one tag, so domain + *separation* stays harness-side (VERIFICATION.md §5b.3). Suite unchanged (13/13). +- **SD-APKE `auth_enc`/`auth_dec` (☐).** Probe confirmed the composition (ML-KEM encaps → + `c2‖info` → HPKE-AuthPsk seal → ciphertext assembly) extracts with ~10 clean leaves + (`hpke_rs__Impl_7__{new,seal,open}` + config consts, `libcrux…Kem__{encaps,decaps}`, + `rand…fill_bytes`). Completing it needs: (a) define those HPKE-AuthPsk + ML-KEM leaves in + the crypto model (Option-wrapped psk/sender-sk, config-keyed, sender-auth reduc); + (b) un-opaque `MessagePublicKey`/`PrivateKey`/`MessageCiphertext`; (c) re-model the + harness with hybrid (DH-AKEM ⊕ ML-KEM) keys — ripples through submission/reply/receiver. + Risk: HPKE-AuthPsk leaf may stress ProVerif termination. Highest value. +- **SD-PKE `metadata::{encrypt,decrypt}` (☐).** Same HPKE leaf (Base mode, no PSK/sender). +- **`api::verify_long_term`/`verify_ephemeral` (☐).** Blocked by the blanket `impl Api + for T` that hax can't extract; needs a refactor to a concrete/free fn. +- migrate `replace_body`→`pv_model` when the tracing backend lands. ### FETCH-NOTES (the one modeling departure) Every other property drives the **extracted** Rust. The fetch mechanism is a **3-party DH diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md b/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md index 23c1b2d8..37851a5d 100644 --- a/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md @@ -122,19 +122,41 @@ Given 4a–4c, ProVerif proves the §2 properties hold against the §3 attacker. ## 5. Modeling assumptions & caveats -### 5a. Fidelity: what is extracted vs. hand-modeled - -**Extracted from the real Rust** (the substance of the analysis): -`message::{auth_enc,auth_dec}`, `metadata::{encrypt,decrypt}`, `sign`/`verify`, -`encrypt_decrypt::encrypt`, **`encrypt_decrypt::decrypt_with_sender`** (the full receive: -trial-decrypt over the key-bundle list → recover the sender key from metadata → -`auth_dec`), the x25519 DH operations, `Plaintext` (de)serialization, and the key / -ciphertext / envelope types. - -**Hand-modeled in the harness** (participants and scenarios, not crypto/protocol logic): -the honest-user key model and trait accessors; the role processes, events, and queries; -the enrollment **process wiring** and domain-separation tags (the `sign`/`verify` calls -themselves are extracted); and — the one substantive departure — the **fetch DH clue**. +### 5a. Fidelity: what is extracted vs. abstracted vs. harness-modeled + +Three distinct categories — be precise about which is which: + +**(i) Extracted as real composition** — the actual Rust control/data flow becomes the +ProVerif model; only the leaves it calls are abstracted. This is the verified +protocol/orchestration logic: +- `encrypt_decrypt::encrypt` — the submission/reply orchestration (which key goes to + which operation, the `NR_ID` associated data, the recipient fetch-pubkey `info`, the + `(X,Z)` fetch-hint construction, the `Envelope` assembly). +- `encrypt_decrypt::decrypt_with_sender` — the receive orchestration (trial-decrypt over + the key-bundle list → recover the sender key from the metadata ciphertext → `auth_dec` + with the recovered key + matching AD/info). +- `sign`/`verify` + `tagged_preimage` — the domain-separated signing-preimage composition + `len‖tag‖msg` (only the Ed25519 op is a leaf). + +**(ii) Abstracted to a symbolic primitive** (the "leaf" boundary, via `replace_body` / +opaque). This is idealized, not verified — as is standard and necessary for symbolic +analysis: +- **Crypto leaves:** `message::{auth_enc,auth_dec}` (SD-APKE modeled **atomically** — + §5b.1), `metadata::{encrypt,decrypt}` (SD-PKE atomically), the Ed25519 `provider` op, + the x25519 DH ops, and (in fetch) the DH clue algebra (§5b.2). +- **Serialization leaves:** `Plaintext` / `MessagePublicKey` (de)serialization → identity; + key / ciphertext / signature / envelope types are opaque bitstrings. + +**(iii) Not extracted / harness-modeled:** key generation & passphrase derivation +(`opaque`); `api::verify_long_term`/`verify_ephemeral` (blanket `impl` that hax can't +extract — the harness re-expresses the composition but drives the **real extracted** +`verify`); the honest-user key model and trait accessors; the roles, events, and queries; +the enrollment process wiring + per-domain tags (§5b.3); the fetch DH clue (§5b.2). + +**In progress:** pushing the leaf boundary further down — extracting `auth_enc`/`auth_dec` +(SD-APKE) and `metadata` (SD-PKE) so only ML-KEM / HPKE / X-Wing remain leaves. A probe +confirms these compositions extract with ~10 clean leaves; completing it requires +modeling the HPKE-AuthPsk + ML-KEM leaves and a hybrid-key harness (`PLAN.md`). ### 5b. Specific assumptions @@ -173,10 +195,13 @@ themselves are extracted); and — the one substantive departure — the **fetch stronger and less-audited assumption than the standard `cryptolib` primitives used for the message and enrollment layers. The clue algebra is *trusted*, not derived from `compute_fetch_challenges`/`solve_fetch_challenges` (which are also not extracted). -3. **Domain-separated signatures are modeled harness-side.** The four Ed25519 domains - (`fpf-sig-nr`, `nr-sig`, `j-sig-ltk`, `j-sig-eph`) are represented by signing/verifying - a tagged message `(TAG, msg)`, mirroring the code's `len(tag)‖tag‖msg` preimage, rather - than deriving the tags from the `DomainTag` impls. +3. **Domain-separated signatures: preimage extracted, tags harness-side.** `sign`/`verify` + and `tagged_preimage` are extracted (the `len‖tag‖msg` preimage is real, only the + Ed25519 op is a leaf). But the ProVerif backend **erases the type parameter `D`** of the + generic `DomainTag::tag()` (it does not monomorphize), so all four domains + (`fpf-sig-nr`/`nr-sig`/`j-sig-ltk`/`j-sig-eph`) collapse to one opaque tag in the + extracted model. Domain **separation** is therefore restored harness-side, by signing/ + verifying a per-domain-tagged message `(TAG, msg)` on top of the extracted preimage. 4. **Serialization is abstracted to identity** for the atomic-key/plaintext types (`MessagePublicKey::from_bytes`, `Plaintext::{to,from}_bytes`): the byte layout is not modeled; round-trip is exact. Length/format-confusion attacks are therefore out of diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl b/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl index cf8f94fd..694f34e7 100644 --- a/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl @@ -171,17 +171,66 @@ letfun securedrop_protocol_minimal__ciphertext__Impl_1__from_bytes(pt_bytes: bit +(* src: protocol-minimal/src/primitives/provider.rs:47 securedrop_protocol_minimal__primitives__provider__ed25519__sign *) +(* Sign `payload` with Ed25519 secret key bytes. *) +letfun securedrop_protocol_minimal__primitives__provider__ed25519__sign( + payload: bitstring, + private_key: bitstring +) = crypto__sign(private_key, payload). +(* src: protocol-minimal/src/primitives/provider.rs:58 securedrop_protocol_minimal__primitives__provider__ed25519__verify *) +(* Verify an Ed25519 `signature` over `payload` with verifying key bytes. *) +letfun securedrop_protocol_minimal__primitives__provider__ed25519__verify( + payload: bitstring, + public_key: bitstring, + signature: bitstring +) = crypto__sig_verify(public_key, payload, signature). +(* src: protocol-minimal/src/sign.rs:123 securedrop_protocol_minimal__sign__Impl_7__from_bytes *) +(* Reconstruct a [`Signature`] from its serialization. *) +letfun securedrop_protocol_minimal__sign__Impl_7__from_bytes(bytes: bitstring) = bytes. +(* src: protocol-minimal/src/sign.rs:132 securedrop_protocol_minimal__sign__Impl_7__as_bytes *) +(* The byte serialization of this signature. *) +letfun securedrop_protocol_minimal__sign__Impl_7__as_bytes(self: bitstring) = self. +(* src: protocol-minimal/src/sign.rs:157 securedrop_protocol_minimal__sign__tagged_preimage *) +(* Construct the tagged signing preimage: `len(tag) || tag || msg`. *) +letfun securedrop_protocol_minimal__sign__tagged_preimage(msg: bitstring) = + let tag = securedrop_protocol_minimal__sign__DomainTag__tag( + rust_primitives__hax__Tuple0__Tuple0 + ) in + alloc__vec__Impl_2__extend_from_slice( + alloc__vec__Impl_2__extend_from_slice( + alloc__vec__Impl_1__push( + alloc__vec__Impl__with_capacity( + rust_primitives__hax__machine_int__add( + rust_primitives__hax__machine_int__add(nat_lit(1), core__slice__Impl__len(tag)), + core__slice__Impl__len(msg) + ) + ), + core__slice__Impl__len(tag) + ), + tag + ), + msg + ). +(* src: protocol-minimal/src/sign.rs:183 securedrop_protocol_minimal__sign__Impl_8__as_bytes *) +letfun securedrop_protocol_minimal__sign__Impl_8__as_bytes(self: bitstring) = self. -(* src: protocol-minimal/src/sign.rs:244 securedrop_protocol_minimal__sign__Impl_10__sign *) +(* src: protocol-minimal/src/sign.rs:257 securedrop_protocol_minimal__sign__Impl_10__as_bytes *) +letfun securedrop_protocol_minimal__sign__Impl_10__as_bytes(self: bitstring) = self. +(* src: protocol-minimal/src/sign.rs:247 securedrop_protocol_minimal__sign__Impl_10__sign *) (* Sign `msg` in domain `D`, returning a `Signature`. *) (* *) (* The actual preimage is `len(tag) || tag || msg` where `tag = D::TAG`. *) letfun securedrop_protocol_minimal__sign__Impl_10__sign(self: bitstring, msg: bitstring) = - crypto__sign(self, msg). -(* src: protocol-minimal/src/sign.rs:279 securedrop_protocol_minimal__sign__Impl_11__verify *) + securedrop_protocol_minimal__sign__Impl_7__from_bytes( + securedrop_protocol_minimal__primitives__provider__ed25519__sign( + securedrop_protocol_minimal__sign__tagged_preimage(msg), + securedrop_protocol_minimal__sign__Impl_10__as_bytes(self) + ) + ). +(* src: protocol-minimal/src/sign.rs:283 securedrop_protocol_minimal__sign__Impl_11__verify *) (* Verify `sig` over `msg`. The domain is determined by the type of `sig`. *) (* *) (* Returns an error if the signature is invalid. *) @@ -189,7 +238,12 @@ letfun securedrop_protocol_minimal__sign__Impl_11__verify( self: bitstring, msg: bitstring, sig: bitstring -) = crypto__sig_verify(self, msg, sig). +) = + securedrop_protocol_minimal__primitives__provider__ed25519__verify( + securedrop_protocol_minimal__sign__tagged_preimage(msg), + securedrop_protocol_minimal__sign__Impl_8__as_bytes(self), + securedrop_protocol_minimal__sign__Impl_7__as_bytes(sig) + ). (* src: protocol-minimal/src/encrypt_decrypt.rs:16 securedrop_protocol_minimal__encrypt_decrypt__NR_ID *) const securedrop_protocol_minimal__encrypt_decrypt__NR_ID: bitstring. (* src: protocol-minimal/src/encrypt_decrypt.rs:25 securedrop_protocol_minimal__encrypt_decrypt__encrypt *) diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl.sha256 b/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl.sha256 index 5f25af65..879c32b5 100644 --- a/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl.sha256 +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/extraction/lib.pvl.sha256 @@ -1 +1 @@ -ae2bb600c8192292fd769e5c9d1fd49691715ffe9f2044cb3238eb7a64ea6edb lib.pvl +9dcb28c42d15244cc849dc6c695801d7264c47d180c2afefed3237bfabdd6fc9 lib.pvl diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/handwritten/sd_model.pvl b/securedrop-protocol/protocol-minimal/proofs/proverif/handwritten/sd_model.pvl index a48e7be7..472d7c96 100644 --- a/securedrop-protocol/protocol-minimal/proofs/proverif/handwritten/sd_model.pvl +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/handwritten/sd_model.pvl @@ -13,6 +13,14 @@ (* the metadata key. *) (*****************************************************************) +(* `DomainTag::tag()` is generic over the domain type `D`; the ProVerif backend erases + the type parameter (it does not monomorphize), so the extracted `tagged_preimage` + calls `DomainTag__tag(Tuple0)` — one opaque tag for ALL four domains. The signing + preimage composition (`len‖tag‖msg`) and the Ed25519 leaf are extracted; but domain + SEPARATION (fpf-sig-nr / nr-sig / j-sig-ltk / j-sig-eph) is consequently modeled + harness-side, by signing/verifying a per-domain-tagged message (see enrollment.pv). *) +fun securedrop_protocol_minimal__sign__DomainTag__tag(bitstring): bitstring. + (* Secret user: long-term/ephemeral secret keys. *) fun sd_secret(bitstring, bitstring, bitstring): bitstring [data]. (* skApke, skFetch, skMeta *) reduc forall a: bitstring, f: bitstring, m: bitstring; diff --git a/securedrop-protocol/protocol-minimal/src/primitives/provider.rs b/securedrop-protocol/protocol-minimal/src/primitives/provider.rs index 40b90226..d7dc1f24 100644 --- a/securedrop-protocol/protocol-minimal/src/primitives/provider.rs +++ b/securedrop-protocol/protocol-minimal/src/primitives/provider.rs @@ -40,13 +40,23 @@ pub mod ed25519 { } /// Sign `payload` with Ed25519 secret key bytes. - #[cfg_attr(hax, hax_lib::opaque)] + // ProVerif LEAF: EUF-CMA signature. (F* keeps this opaque.) + #[cfg_attr(all(hax, not(hax_backend_proverif)), hax_lib::opaque)] + #[cfg_attr( + hax_backend_proverif, + hax_lib::proverif::replace_body("crypto__sign(private_key, payload)") + )] pub(crate) fn sign(payload: &[u8], private_key: &[u8; 32]) -> [u8; 64] { libcrux_ed25519::sign(payload, private_key).expect("Ed25519 signing is infallible") } /// Verify an Ed25519 `signature` over `payload` with verifying key bytes. - #[cfg_attr(hax, hax_lib::opaque)] + // ProVerif LEAF: reduces to unit only for a genuine signature. + #[cfg_attr(all(hax, not(hax_backend_proverif)), hax_lib::opaque)] + #[cfg_attr( + hax_backend_proverif, + hax_lib::proverif::replace_body("crypto__sig_verify(public_key, payload, signature)") + )] pub(crate) fn verify( payload: &[u8], public_key: &[u8; 32], diff --git a/securedrop-protocol/protocol-minimal/src/sign.rs b/securedrop-protocol/protocol-minimal/src/sign.rs index 2854b93c..41a1b5ab 100644 --- a/securedrop-protocol/protocol-minimal/src/sign.rs +++ b/securedrop-protocol/protocol-minimal/src/sign.rs @@ -119,6 +119,8 @@ impl Eq for Signature {} impl Signature { /// Reconstruct a [`Signature`] from its serialization. + // ProVerif serialization leaf: signature is atomic (opaque), so this is identity. + #[cfg_attr(hax_backend_proverif, hax_lib::proverif::replace_body("bytes"))] pub fn from_bytes(bytes: [u8; 64]) -> Self { Self { bytes, @@ -127,6 +129,7 @@ impl Signature { } /// The byte serialization of this signature. + #[cfg_attr(hax_backend_proverif, hax_lib::proverif::replace_body("self"))] pub fn as_bytes(&self) -> [u8; 64] { self.bytes } @@ -176,6 +179,8 @@ pub struct VerifyingKey([u8; KEY_LEN_ED25519]); pub(crate) struct SigningSecretKey([u8; KEY_LEN_ED25519]); impl VerifyingKey { + // ProVerif serialization leaf: the verifying key is atomic (opaque) -> identity. + #[cfg_attr(hax_backend_proverif, hax_lib::proverif::replace_body("self"))] pub(crate) fn as_bytes(&self) -> &[u8; KEY_LEN_ED25519] { &self.0 } @@ -236,19 +241,20 @@ impl SigningKey { /// Sign `msg` in domain `D`, returning a `Signature`. /// /// The actual preimage is `len(tag) || tag || msg` where `tag = D::TAG`. - // ProVerif: EUF-CMA signature `crypto__sign(sk, msg)`. NOTE (M3): the type-level - // domain separator `D` is not yet reflected in the symbolic term; add the tag to - // the signed message when modeling the enrollment trust chain. - #[cfg_attr( - hax_backend_proverif, - hax_lib::proverif::replace_body("crypto__sign(self, msg)") - )] + // ProVerif: EXTRACTED. The domain-separated preimage (`tagged_preimage`) and the + // Ed25519 leaf (`provider::ed25519::sign`) are the only abstracted parts, so domain + // separation is now part of the verified model rather than the harness. pub fn sign(&self, msg: &[u8]) -> Signature { let preimage = tagged_preimage::(msg); - let bytes = provider::ed25519::sign(&preimage, self.sk.as_bytes()); + // `self.as_bytes()` (not `self.sk.as_bytes()`) so the opaque signing key needs + // no field access in the ProVerif model. + let sk = self.as_bytes(); + let bytes = provider::ed25519::sign(&preimage, &sk); Signature::from_bytes(bytes) } + // ProVerif serialization leaf: the signing key is atomic (opaque) -> identity. + #[cfg_attr(hax_backend_proverif, hax_lib::proverif::replace_body("self"))] pub(crate) fn as_bytes(&self) -> [u8; 32] { *self.sk.as_bytes() } @@ -272,15 +278,13 @@ impl VerifyingKey { /// Verify `sig` over `msg`. The domain is determined by the type of `sig`. /// /// Returns an error if the signature is invalid. - // ProVerif: `crypto__sig_verify(vk, msg, sig)` reduces to unit only for a genuine - // signature under the matching key (forgery has no value -> propagates as `Err`). - #[cfg_attr( - hax_backend_proverif, - hax_lib::proverif::replace_body("crypto__sig_verify(self, msg, sig)") - )] + // ProVerif: EXTRACTED (same domain-separated preimage as `sign`); only the Ed25519 + // leaf (`provider::ed25519::verify`) is abstracted. pub fn verify(&self, msg: &[u8], sig: &Signature) -> Result<(), Error> { let preimage = tagged_preimage::(msg); - provider::ed25519::verify(&preimage, self.as_bytes(), &sig.bytes) + // `sig.as_bytes()` (not `sig.bytes`) so the opaque signature needs no field access. + let sig_bytes = sig.as_bytes(); + provider::ed25519::verify(&preimage, self.as_bytes(), &sig_bytes) .map_err(|_| anyhow::anyhow!("Signature verification failed")) } } From 9a0b5e23feb28de23e84cf0cf6c7642ff1e9109b Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Tue, 14 Jul 2026 16:05:04 +0200 Subject: [PATCH 4/6] ci: fix lint + F* diff from the sign/verify extraction - proverif.yml: pin ocaml/setup-ocaml to a commit SHA (zizmor unpinned-uses). - Re-extract F* for the semantically-equivalent sign.rs refactor: only Sign.fst changes (as_bytes hoisted + a local); it still type-checks/verifies. Correct the "F* untouched" claim in VERIFICATION.md accordingly. Co-Authored-By: Claude Opus 4.8 (1M context) --- .github/workflows/proverif.yml | 2 +- .../extraction/Securedrop_protocol_minimal.Sign.fst | 12 +++++++----- .../protocol-minimal/proofs/proverif/VERIFICATION.md | 10 +++++++--- 3 files changed, 15 insertions(+), 9 deletions(-) diff --git a/.github/workflows/proverif.yml b/.github/workflows/proverif.yml index 2e4821e4..a77e1e75 100644 --- a/.github/workflows/proverif.yml +++ b/.github/workflows/proverif.yml @@ -22,7 +22,7 @@ jobs: persist-credentials: false - name: Set up OCaml (for ProVerif) - uses: ocaml/setup-ocaml@v3 + uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3 with: ocaml-compiler: "5.3" diff --git a/securedrop-protocol/protocol-minimal/proofs/fstar/extraction/Securedrop_protocol_minimal.Sign.fst b/securedrop-protocol/protocol-minimal/proofs/fstar/extraction/Securedrop_protocol_minimal.Sign.fst index 7fae6c5e..357f3ca0 100644 --- a/securedrop-protocol/protocol-minimal/proofs/fstar/extraction/Securedrop_protocol_minimal.Sign.fst +++ b/securedrop-protocol/protocol-minimal/proofs/fstar/extraction/Securedrop_protocol_minimal.Sign.fst @@ -423,6 +423,9 @@ let impl_SigningKey__new <: (v_R & Core_models.Result.t_Result t_SigningKey Anyhow.t_Error) +let impl_SigningKey__as_bytes (self: t_SigningKey) : t_Array u8 (mk_usize 32) = + impl_SigningSecretKey__as_bytes self.f_sk + /// Sign `msg` in domain `D`, returning a `Signature`. /// The actual preimage is `len(tag) || tag || msg` where `tag = D::TAG`. let impl_SigningKey__sign @@ -432,18 +435,16 @@ let impl_SigningKey__sign (msg: t_Slice u8) : t_Signature v_D = let preimage:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = tagged_preimage #v_D msg in + let sk:t_Array u8 (mk_usize 32) = impl_SigningKey__as_bytes self in let bytes:t_Array u8 (mk_usize 64) = Securedrop_protocol_minimal.Primitives.Provider.Ed25519.sign (Alloc.Vec.impl_1__as_slice preimage <: t_Slice u8) - (impl_SigningSecretKey__as_bytes self.f_sk <: t_Array u8 (mk_usize 32)) + sk in impl_7__from_bytes #v_D bytes -let impl_SigningKey__as_bytes (self: t_SigningKey) : t_Array u8 (mk_usize 32) = - impl_SigningSecretKey__as_bytes self.f_sk - let impl_SigningKey__from_seed (seed: t_Array u8 (mk_usize 32)) : t_SigningKey = let pk:t_Array u8 (mk_usize 32) = Rust_primitives.Hax.repeat (mk_u8 0) (mk_usize 32) in let pk:t_Array u8 (mk_usize 32) = @@ -466,6 +467,7 @@ let impl_VerifyingKey__verify (sig: t_Signature v_D) : Core_models.Result.t_Result Prims.unit Anyhow.t_Error = let preimage:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = tagged_preimage #v_D msg in + let sig_bytes:t_Array u8 (mk_usize 64) = impl_7__as_bytes #v_D sig in Core_models.Result.impl__map_err #Prims.unit #Anyhow.t_Error #Anyhow.t_Error @@ -475,7 +477,7 @@ let impl_VerifyingKey__verify <: t_Slice u8) (impl_VerifyingKey__as_bytes self <: t_Array u8 (mk_usize 32)) - sig.f_bytes + sig_bytes <: Core_models.Result.t_Result Prims.unit Anyhow.t_Error) (fun temp_0_ -> diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md b/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md index 37851a5d..7b28d446 100644 --- a/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md @@ -4,7 +4,10 @@ Status report for the hax → ProVerif symbolic security analysis of `securedrop-protocol-minimal`. This is a **symbolic (Dolev–Yao) analysis**: it proves protocol-level security properties assuming cryptographic primitives are perfect. It complements — and is independent of — the F\* track (`proofs/fstar/`, panic-freedom / -functional correctness), which is untouched by this work. +functional correctness). The F\* extraction is essentially untouched: one +semantically-equivalent refactor to `sign.rs` (to keep the opaque signing key free of +field access) changed a single extracted module (`Sign.fst`, re-committed, still verifies); +all other F\* modules are byte-identical. - **Run it:** `make proverif-check` (engine-free — needs only a `proverif` binary). - **Re-extract from Rust:** `make proverif-extract` (needs the `hax-proverif` opam switch). @@ -282,8 +285,9 @@ To regenerate `lib.pvl` from the Rust source rather than trust the committed sna - `cargo build` and `cargo test` are unaffected (all annotations are `cfg(hax_backend_proverif)`-gated). -- **`proofs/fstar/` is byte-identical** — the F\* extraction and verification pipeline is - untouched. +- **`proofs/fstar/` is byte-identical except `Sign.fst`** — the one semantically-equivalent + `sign.rs` refactor re-extracted that single module (re-committed; still type-checks and + verifies). Every other F\* module and the verification pipeline are unchanged. - Source changes are ~80 cfg-gated lines across `message.rs`, `metadata.rs`, `sign.rs`, `ciphertext.rs`, `keys.rs`, `primitives/x25519.rs`, plus the workspace `Cargo.toml` lint and the crate `Makefile` targets. Everything else is new files under From 14f4f3d07238e466ef51f23970e5e0e0d29252be Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Tue, 14 Jul 2026 16:27:38 +0200 Subject: [PATCH 5/6] docs(proverif): lead with what's translated vs assumed; summarize goals MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - New §1 "What is translated to ProVerif, and what is assumed": three layers (translated protocol logic / idealized crypto / hand-written model), stating up front that the composition is verified while the crypto primitives and the SD-APKE/SD-PKE/fetch constructions are assumed. - §2: English summary of the target security goals (confidentiality, message authentication, enrollment trust chain / no rogue journalists, fetch privacy + recipient anonymity, non-vacuity) before the RESULT table. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../proofs/proverif/VERIFICATION.md | 75 ++++++++++++++++--- 1 file changed, 66 insertions(+), 9 deletions(-) diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md b/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md index 7b28d446..5f367824 100644 --- a/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md @@ -17,18 +17,75 @@ Result: **13/13 properties verified.** --- -## 1. How it works (one paragraph) - -The hax ProVerif backend lifts the crate's **actual Rust functions** into a ProVerif -model (`extraction/lib.pvl`). Cryptographic leaves are redirected to a shared symbolic -crypto library via source annotations gated on `cfg(hax_backend_proverif)` (invisible to -normal builds, `cargo test`, and F\* extraction). Hand-written ProVerif harnesses -(`queries/*.pv`) instantiate honest participants, an active network attacker, and the -security queries, calling the generated functions. ProVerif then discharges each query. +## 1. What is translated to ProVerif, and what is assumed + +**Mechanism.** The hax ProVerif backend translates the crate's **actual Rust functions** +into a ProVerif model (`extraction/lib.pvl`). At the bottom, cryptographic and +serialization "leaf" functions are redirected to a symbolic crypto library (via source +annotations gated on `cfg(hax_backend_proverif)`, invisible to normal builds / `cargo +test` / F\* extraction). Hand-written harnesses (`queries/*.pv`) then instantiate honest +participants and an active network attacker that drive those translated functions, and +ProVerif discharges each security query. + +So the analysis has three layers — **only the first is *verified*; the other two are +*assumed*:** + +**① Translated Rust — the verified protocol logic.** The end-to-end message flow and the +signature construction are translated from the real Rust, so their control/data flow *is* +what ProVerif checks — which key feeds which operation, the associated-data / `info` +binding, the envelope assembly, the trial-decrypt dispatch, the signing preimage: +- `encrypt_decrypt::encrypt` — submission/reply orchestration. +- `encrypt_decrypt::decrypt_with_sender` — receive orchestration (trial-decrypt → recover + sender key from metadata → authenticated-decrypt). +- `sign` / `verify` / `tagged_preimage` — the domain-separated signing preimage. + +**② Idealized cryptography — assumed perfect (standard for symbolic analysis).** Every +cryptographic operation is replaced by a perfect Dolev–Yao abstraction; ProVerif never +reasons about the primitive's internals. This covers the true leaves (Ed25519, X25519) +**and, in the current model, more than the leaves**: the SD-APKE and SD-PKE constructions +(`auth_enc`/`auth_dec`, `metadata::encrypt`/`decrypt`) are modeled **atomically** rather +than decomposed into ML-KEM ⊕ DH-AKEM ⊕ HPKE, and the fetch DH clue uses an idealized +algebra. Serialization is modeled as **identity** (byte layout unverified), and key +generation / passphrase derivation is **not translated at all**. + +**③ Hand-written model — assumed faithful.** The honest-participant key model, the roles +and events, the security queries themselves, and the enrollment verification composition +(`api::verify_long_term`, which hax cannot extract) are hand-written ProVerif, trusted to +model the protocol correctly. + +The precise, itemized breakdown is in **§5** (fidelity + assumptions); the trust base is +in **§4**. In short: **the protocol *composition* is verified; the crypto *primitives* and +the SD-APKE/SD-PKE/fetch *constructions* are assumed.** Lowering the ② boundary so only +true leaves are idealized is in-progress (§5a, `PLAN.md`). --- -## 2. Verified properties (13 RESULT lines) +## 2. Verified properties + +At a high level, the analysis targets the security goals a SecureDrop-style system needs, +against an active network attacker and an untrusted server (§3): + +- **Message confidentiality.** A source's submission — and a journalist's reply — remains + secret; neither the network attacker nor the untrusted server learns the message. +- **Message authentication (implicit, via SD-APKE).** If a journalist accepts a message as + coming from a given source, that source really sent it; symmetrically, a source that + accepts a reply can be sure it came from the journalist. An attacker cannot forge or + tamper with a message under an honest party's identity. +- **Enrollment trust chain — no rogue journalists.** A client accepts a journalist's keys + only when the chain of trust holds: FPF (the root anchor) signed the newsroom, and the + newsroom signed that journalist. An attacker who mints its own journalist keys and + injects a forged enrollment cannot get a client to accept it. A companion *soundness* + check demonstrates the newsroom-signature step is load-bearing (removing it reintroduces + the attack — so the guarantee is not vacuous). +- **Privacy-preserving fetch.** Only the intended recipient can recover a message's id from + the server's fetch challenges (a wrong recipient and a network eavesdropper cannot); and + the untrusted server cannot tell **which recipient** a stored message is addressed to — + *recipient anonymity / unlinkability*. +- **Non-vacuity (sanity).** For each authentication/secrecy goal, the honest run is shown to + actually reach the relevant event, so the correspondence results above are not vacuously + true. + +Each row below is one ProVerif `RESULT` line (all 13 currently pass — `make proverif-check`): | Layer | File | Property | ProVerif verdict | |---|---|---|---| From 25dbadfa8df264b47346b5c0aded8a57eb5459d7 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Tue, 14 Jul 2026 17:40:55 +0200 Subject: [PATCH 6/6] docs(proverif): add "Coverage in numbers" (translated vs trusted line counts) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ~85 lines of Rust (5 composition fns) -> ~151 lines of ProVerif verified core; full lib.pvl is 372 lines (rest = leaf redirects + auto type machinery); trusted hand-written side (vendored crypto + queries + SD crypto/user model) ~1150 lines. The translated core is ~2% of the crate's ~3,730 src lines — the intended 2%. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../proofs/proverif/VERIFICATION.md | 34 +++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md b/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md index 5f367824..79190294 100644 --- a/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md +++ b/securedrop-protocol/protocol-minimal/proofs/proverif/VERIFICATION.md @@ -218,6 +218,40 @@ the enrollment process wiring + per-domain tags (§5b.3); the fetch DH clue (§5 confirms these compositions extract with ~10 clean leaves; completing it requires modeling the HPKE-AuthPsk + ML-KEM leaves and a hybrid-key harness (`PLAN.md`). +#### Coverage in numbers + +The **translated-and-verified core** (category ①) is compact — 5 functions: + +| Rust function | ~Rust src lines | → ProVerif lines | +|---|---|---| +| `encrypt_decrypt::encrypt` | ~34 | 52 | +| `encrypt_decrypt::decrypt_with_sender` | ~25 | 63 | +| `sign` + `verify` + `tagged_preimage` | ~25 | 7 + 10 + 19 | +| **total translated** | **~85** | **~151** | + +The full generated model `extraction/lib.pvl` is **372 lines** (258 code; 25 `letfun`s): +the ~151 composition lines above, plus ~15 one-line **leaf redirects** (crypto/ +serialization abstracted) and the rest **auto-generated type machinery** (struct +constructors + field accessors). + +The **trusted, hand-written side** (categories ② and ③ — *assumed*, not translated) is +~8× larger: + +| File group | lines | +|---|---| +| `lib/*.pvl` — vendored generic crypto + prelude (§4a) | 627 | +| `queries/*.pv` — roles, events, security queries (§4c) | 409 | +| `handwritten/*.pvl` — SecureDrop crypto + honest-user model (§4a/§4c) | 114 | +| **total trusted hand-written ProVerif** | **~1150** | + +For scale, the analyzed crate (`protocol-minimal/src`) is ~3,730 lines of Rust, so the +~85 translated lines are **~2%** of it. That is the *intended* 2%: the remainder is +crypto-primitive wrappers (the leaf boundary — abstracted by design), serde / +serialization (excluded), key-type boilerplate, and tests — none of which are targets of +symbolic protocol analysis. The lever to raise this figure is lowering the leaf boundary +on the message crypto (SD-APKE / SD-PKE), which would move those constructions from +one-line redirects into translated compositions. + ### 5b. Specific assumptions 1. **SD-APKE is modeled atomically.** HPKE-AuthPsk = DH-AKEM (sender auth) ⊕ ML-KEM (PSK)