Add hax→ProVerif symbolic analysis for protocol-minimal - #2
Open
karthikbhargavan wants to merge 6 commits into
Open
Add hax→ProVerif symbolic analysis for protocol-minimal#2karthikbhargavan wants to merge 6 commits into
karthikbhargavan wants to merge 6 commits into
Conversation
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) <noreply@anthropic.com>
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) <noreply@anthropic.com>
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) <noreply@anthropic.com>
- 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) <noreply@anthropic.com>
- 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) <noreply@anthropic.com>
… counts) ~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) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Symbolic (Dolev–Yao) security analysis of
protocol-minimalvia the hax ProVerif backend.Verified (13 properties,
make proverif-check, engine-free):Drives the extracted Rust (
encrypt,decrypt_with_sender,auth_enc/auth_dec, metadata enc/dec,sign/verify). The 3-party DH fetch clue is hand-modeled with an idealized algebra (see limitations in VERIFICATION.md).Scope:
cfg(hax_backend_proverif)-gated;cargo build,cargo test, and the F* pipeline (proofs/fstar/) are unaffected (byte-identical).proofs/proverif/(driver, sha-pinned model snapshot, queries, vendored libs, docs) and.github/workflows/proverif.yml(engine-free lane). Re-extract withmake proverif-extract.Docs:
proofs/proverif/VERIFICATION.md(status, threat model, trust assumptions, limitations);proofs/proverif/PLAN.md(history).🤖 Generated with Claude Code