euwallet — The First Quantum-Safe EU Wallet Implementation

Assurance

EUDI-grade engineering beneath a global runtime: machine-checked proofs, explicit threat models, native assurance, and profile-specific conformance.

Security & privacy

Designed against the attacker, not just the happy path.

The threat model comes first; every control links to a proof, a test, or an architecture element that exists in the repository.

Threat model: adversary, scenario, controls, and the evidence backing each control.
Adversary	Controls	Evidence	Status
Malicious / compromised verifierOver-asks for claims, replays old requests, or spoofs another RP's identity.	– Signed request objects verified against RP keys resolved from the operator-signed trusted list (in-core decision, never a shell boolean) – Data minimisation: only requested-AND-held claims are disclosable; consent screen shows the exact set – Nonce replay set persisted; audience must match the wallet	Lean: disclose_requires_consent_and_validation`formal/lean/WalletModel.lean` Tamarin: injective_agreement, nonce_authentic`formal/tamarin/oid4vp_haip.spthy` Tests: abort_audience_mismatch, abort_nonce_replayed, minimum_claim_set`crates/oid4vp/`	Verified
Network attacker (read / inject / replay / relay)Controls the channel between wallet, issuer, verifier, or a proximity reader.	– All protocol decisions assume an untrusted channel (Dolev–Yao analysis) – Proximity: SessionTranscript binding + session encryption + reader authentication (anti-relay) – Remote: holder binding via KB-JWT over nonce + audience + presentation hash	Tamarin: session_binding, claim_secrecy (proximity)`formal/tamarin/iso18013_5_proximity.spthy` Tamarin: claim_secrecy (remote)`formal/tamarin/oid4vp_haip.spthy` Lean: response_requires_bound_session`formal/lean/ProximityModel.lean`	Verified
Malicious or untrusted issuerTries to plant credentials from outside the trust framework.	– Issuer trust decided in-core by X.509 path validation to PID/attestation anchors on the operator-signed trusted list – Untrusted issuer aborts the machine before any token request	Lean: issued_requires_issuer_trust, untrusted_issuer_is_rejected`formal/lean/IssuanceModel.lean` Tamarin: issuer_authentication`formal/tamarin/oid4vci_issuance.spthy` Tests: abort_untrusted_issuer, untrusted_issuer_is_rejected_in_core`crates/oid4vci/ · crates/wallet-core/tests/e2e_issuance.rs`	Verified
Transaction-data tamperer (payments / signing)Changes amount, payee, or the document between user confirmation and signing.	– Dynamic linking: the authentication code IS a device signature over (payee, IBAN, amount, currency, transaction id, nonce) – WYSIWYS: the QES authorization binds the confirmed document digest + consent hash	Tamarin: dynamic_linking, no_tampering`formal/tamarin/payment_sca.spthy` Tamarin: what_you_see_is_what_you_sign, no_document_substitution`formal/tamarin/qes.spthy` Tests: PSD2 RTS Art. 4–5 suite (10 named tests)`crates/crypto-backend/tests/regulatory_sca.rs`	Verified
Replay attackerRe-submits a previous presentation, payment, signing, or issuance proof.	– Per-flow nonce/c_nonce replay sets, persisted via shell effects – Replay rejection proven at model level and tested at implementation level per flow	Lean: replay_is_rejected (wallet, payment, QES)`formal/lean/` Tamarin: nonce_authentic, cnonce_authentic`formal/tamarin/` Tests: abort_nonce_replayed, abort_c_nonce_replayed, rts_transaction_uniqueness_replay_rejected`crates/`	Verified
Lost / stolen deviceAttacker with physical possession attempts to present or authorize.	– Device key in the Secure Enclave, non-exportable, biometric/passcode access control (.biometryCurrentSet) – Private key never crosses the FFI — the core only ever requests a signature by reference	SecureEnclaveSigner (device); keychain fallback only on Simulator`ios/Sources/WalletShell/SecureEnclaveSigner.swift` Signature-conversion unit tests (DER→JOSE)`ios/Tests/WalletShellTests/SecureEnclaveSignerTests.swift`	Partial
Stale trust: expired, revoked, or mis-chained certificates & credentialsPresents after revocation; issuer/RP certs expired or chained to the wrong anchor.	– Token Status List checked before presenting; fail-closed when status is unresolvable online – X.509 path validation with validity windows against the clock the shell supplies – Trusted-list signature + validity verified before any anchor is used	Tests: rejects_expired, rejects_expired_list, rejects_wrong_operator_signature, revoked-blocking e2e`crates/status/ · crates/trust/ · crates/x509/`	Tested
Malformed / hostile input (CBOR, COSE, JOSE, JSON, QR)Parser exploitation via crafted credentials, requests, or QR payloads.	– Canonical-CBOR enforcement (rejects non-canonical, duplicate keys, indefinite lengths, trailing bytes) – Coverage-guided fuzz targets for the four codec surfaces; Kani bounded proofs on the mdoc codec in CI – memory-safe Rust: all 21 crates are #![forbid(unsafe_code)]	Fuzz: cose_cbor, mdoc_cbor, sdjwt_parse, x509_parse`fuzz/fuzz_targets/` Tests: rejects_non_canonical, rejects_duplicate_map_keys, rejects_trailing_bytes …`crates/cose/ · crates/mdoc/` CI: tier1-fuzz-kani`.github/workflows/ci.yml`	Tested
Dependency / build-pipeline compromiseA malicious or vulnerable dependency enters the build.	– Pinned Rust toolchain (1.97.1) and locked dependency graph – cargo-deny (licenses, bans, sources, advisories) + cargo-audit in CI; documented dependency budget – CycloneDX SBOM published in-repo (21 crates; regenerable from a clean checkout)	deny.toml (2 documented build-time-only advisory ignores)`deny.toml` CI: supply-chain job`.github/workflows/ci.yml` Dependency budget`docs/dependency-budget.md`	Tested
Overlay / UI-redressing, phishing verifierTricks the user into consenting to something other than what is displayed.	– The core renders fully-resolved consent screens (exact claims, payee, amount, document) — the shell cannot display an unbound approximation – A committing consent hash is recorded in the audit log for every approval	presenter::consent_hash + ScreenDescription contract`crates/presenter/` Test: consent_hash_is_stable_and_tamper_evident`crates/presenter/`	Partial

The written threat-model document (TOE boundary, full asset/attacker matrices) is a stub pending publication — docs/certification-evidence/threat-model.md. The rows above are limited to adversaries the code and formal models demonstrably address today.

Privacy as architecture

What leaves the wallet

Only the requested-and-held disclosure subset, inside a holder-bound presentation. The minimum-claim-set computation is core logic with unit tests; family_name staying private while age_over_18 is disclosed is asserted end-to-end over a live socket.

crates/presenter/ · crates/shell-io/tests/e2e_live_presentation.rs

Issuer non-involvement at presentation

Presentation is wallet↔verifier only; the issuer is not contacted. Revocation is checked against issuer-published status lists the wallet fetches independently (fail-closed when unresolvable online).

crates/status/

Audit log without values

The transaction log records claim PATHS and a committing consent hash — never claim values. Entries can be redacted to chain-preserving tombstones; the whole log can be wiped; the activity report contains counts only.

crates/txnlog/ · crates/wallet-core/tests/txn_log.rs

Portable, integrity-protected export

Holder data export carries an integrity hash; the core's own verifier detects tampered bundles (asserted in tests).

crates/wallet-core/src/export.rs · crates/wallet-core/tests/export.rs

Telemetry

None. The core is sans-IO; no analytics or logging endpoints exist in this codebase.

crates/ (no telemetry dependency in the dependency budget)

Unlinkability limits — stated honestly

Unlinkability / observational equivalence is NOT yet modelled in Tamarin, and salted SD-JWT disclosure hashes are the only correlation reduction currently implemented. An experimental Ristretto Pedersen/Schnorr ZK predicate proof exists behind a non-default feature flag (6 tests) and is explicitly not production. DPIA pending publication.

crates/zkp/src/experimental.rs · docs/certification-evidence/dpia.md (stub)