Assurance
EUDI-grade engineering beneath a global runtime: machine-checked proofs, explicit threat models, native assurance, and profile-specific conformance.
Formal verification
Claims, assumptions, proofs.
Two complementary tracks. Lean 4 is an interactive theorem prover whose kernel checks proof terms — used here for machine-checked state-machine invariants and safety properties of the wallet's protocol machines. Tamarin analyses the protocols in a symbolic (Dolev–Yao) adversary model and supports both attack discovery and unbounded verification — and it did find a real attack here before it could ship.
Lean 4 — machine-checked invariants
Verified66 theorems across 8 models, 0 sorry — toolchain Lean 4 v4.32.0 (formal/lean/lean-toolchain). lake build PASS for all eight repository models — local verification, 2026-08-10. This explorer details the six EUDI protocol models plus app-shell navigation; the isolated hybrid-PQ model is outside this catalogue. Zero `sorry`; no additional axioms declared in the models.
Model-to-code binding Each Lean model doubles as an executable oracle: `lake exe` emits transition traces that crates/{oid4vp,payment,iso18013-5,oid4vci,qes,w2w}/tests/conformance.rs replay against the production Rust machines. CI regenerates the traces and fails if the checked-in traces are stale (job tier2-lean-oracle), so the model and the shipped code cannot silently diverge.
Tamarin — symbolic protocol analysis
Verified30 lemmas proven across 7 models, 0 falsified — all automatic (no interactive steps). Local verification, 2026-08-10; this explorer details the six EUDI models while the isolated hybrid-PQ model is included in the aggregate result. Tool: tamarin-prover 1.12.0. Adversary: Dolev–Yao: the attacker fully controls the network (read, intercept, inject, replay); cryptography is ideal (symbolic); key compromise is modelled with explicit Reveal rules and each lemma states its exclusions.
Result wording For each lemma: no violating trace was found and the lemma was proven in the specified symbolic model. This is a statement about the modelled protocol under symbolic assumptions — not a claim that the implementation or its cryptographic primitives are unbreakable.
What the proofs cover — and what they do not
Covered
- – The six protocol state machines: their invariants, safety properties, and abort behaviour (Lean, kernel-checked).
- – The protocol designs under a Dolev–Yao network adversary with stated key-compromise exclusions (Tamarin, 30 lemmas across 7 models).
- – The correspondence between each Lean model and its production Rust machine, via oracle-trace replay gated in CI.
- – Codec robustness on hostile bytes: canonical-CBOR rejection tests, 5 fuzz targets, Kani bounded proofs on the mdoc crate.
Trusted computing base & gaps
- – The Lean kernel and Tamarin's semantics/equational theories are trusted, not verified here.
- – Cryptographic primitives (aws-lc-rs), the OS, the Secure Enclave, and randomness sources are assumed correct; symbolic models treat cryptography as ideal.
- – The model-to-code mapping covers the state machines — not the shell UI, FFI serialization gadgets, or network transport (TLS is the platform's).
- – Side channels, unlinkability/observational equivalence, and multi-session interleavings beyond the models are not analysed yet.
- – No independent assessment (audit, pentest, certification) has been performed to date.
Verification coverage map
Which assurance instrument covers which component. Symbols carry the meaning (not colour): covered · partial · planned · assumed (TCB) · none.
| Component | Lean proofs | Tamarin lemmas | Unit / state tests | Integration / E2E | Fuzz / Kani | External conformance | Independent assessment |
|---|---|---|---|---|---|---|---|
| oid4vp (presentation machine) | covered | covered | covered | covered | none | planned | none |
| oid4vci (issuance machine) | covered | covered | covered | covered | none | planned | none |
| iso18013-5 (proximity machine)BLE/NFC transports not on device yet | covered | covered | covered | partial | none | planned | none |
| payment (SCA authorization)PSD2 RTS suite; TS12 envelope pending | covered | covered | covered | covered | none | planned | none |
| qes (signing authorization)QTSP/CSC integration planned | covered | covered | covered | covered | none | planned | none |
| w2w (credential transfer) | covered | covered | covered | covered | none | none | none |
| Format codecs (sdjwt · mdoc · cose · x509)Kani bounded proofs on mdoc in CI | none | none | covered | covered | covered | planned | none |
| Trust & status (trust · status · wua) | none | none | covered | covered | none | planned | none |
| Consent & audit (presenter · txnlog)consent hash appears in payment/QES models | partial | partial | covered | covered | none | none | none |
| wallet-core facade + UniFFI contract | none | none | covered | covered | none | planned | none |
| iOS shell (SwiftUI · executor · adapters)24 Swift tests; navigation statechart formally verified (Lean) + exhaustively conformance-checked; visual rendering itself untested | partial | none | covered | partial | none | none | none |
| Android shell (Kotlin · executor · adapters)Hosted unit/lint/release gates pass; Android-specific formal model and exhaustive Kotlin model conformance remain open | planned | none | covered | partial | none | planned | none |
| Crypto backend (aws-lc-rs)TCB: primitives assumed correct; KATs pending | assumed (TCB) | assumed (TCB) | partial | covered | none | none | none |
| Secure Enclave / OS / platformTrusted computing base | assumed (TCB) | assumed (TCB) | none | none | none | none | none |