euwallet · sans-IO Rust core · Lean 4 · Tamarin
An interoperable digital-identity architecture for credential issuance, privacy-preserving presentation, signature authorization, and payment SCA — built around explicit trust boundaries, machine-checked invariants, symbolic protocol analysis, and a reproducible, versioned evidence pipeline.
Every claim on this page names its scope, tool, version, date, and artifact. Evidence refreshed 2026-07-19 · commit f5b2ef0.
Last evidence refresh: 2026-07-19 — tools/evidence/generate.sh — reproducible from a clean checkout; regenerates Tier 0–3 results into the verification report.
Architecture
The wallet is a sans-IO Rust behaviour core driven by thin native shells. Responsibility boundaries — not frameworks — are the design: protocol logic cannot touch the network, the shell cannot make trust decisions, and keys cannot leave secure hardware. Assessed against the pinned EUDI specification register: ARF v2.9.0 · PID Rulebook v1.6 · FCAF v0.0.7 (snapshot 2026-07-17) — never an unversioned "latest ARF".
The core is a pure state machine: events in, effects out. No network, clock, radio, or disk access exists inside protocol logic — the shell executes effects and feeds results back.
Why it matters Protocol decisions are deterministic and testable without mocking the world; the same core binary logic runs under tests, fuzzing, oracle replay, and on device.
crates/wallet-core/src/lib.rs (Event/Effect contract)
Each protocol (presentation, issuance, proximity, payment, QES, transfer) is an explicit state machine with exhaustive matches; every guard maps 1:1 to a named abort reason.
Why it matters Same state + same event ⇒ same effects. This is what makes the Lean models faithful and the oracle-replay conformance suites meaningful.
crates/oid4vp/src/lib.rs · formal/lean/*.lean · crates/*/tests/conformance.rs
All cryptography goes through the crypto-traits interface; the production backend is aws-lc-rs. Protocol crates cannot reach a crypto library directly.
Why it matters Cryptographic agility: the backend can be swapped or FIPS-pinned without touching protocol logic; the allow-list of algorithms is auditable in one place.
crates/crypto-traits/ · crates/crypto-backend/
Signing is an effect carrying bytes-to-sign and a key reference. The Secure Enclave (non-exportable, biometric-gated) fulfils it on device.
Why it matters A compromised UI process cannot exfiltrate key material it never holds.
ios/Sources/WalletShell/SecureEnclaveSigner.swift · Effect::Sign contract
The core renders fully-resolved screens (exact claims, amount, payee, document) and records a committing consent hash in the tamper-evident audit log.
Why it matters What the user approved is cryptographically bound to what is signed — the basis of the dynamic-linking and WYSIWYS proofs.
crates/presenter/ · crates/txnlog/
RP registration and issuer trust are decided in-core by X.509 path validation against operator-signed trusted lists; status lists gate presentation fail-closed. The shell only fetches bytes.
Why it matters A buggy or malicious shell cannot inject 'trusted: true'.
crates/trust/ · crates/x509/ · crates/status/
All 21 workspace crates are #![forbid(unsafe_code)]; the pinned toolchain is Rust 1.97.1.
Why it matters Entire vulnerability classes (spatial/temporal memory errors) are excluded at compile time in wallet code.
crates/*/src/lib.rs · rust-toolchain.toml
One Rust core serves iOS today (UniFFI bindings + Swift shell) and is the same artifact an Android shell would embed. The reference shell-io crate drives the identical core over real sockets.
Why it matters Behaviour reviewed and verified once, shipped everywhere; shells stay thin and auditable.
crates/wallet-core/ · ios/ · crates/shell-io/
Select any component (click or keyboard) to open its evidence panel — responsibilities, trust assumptions, threats, proofs, tests, and source path. Static SVG artifacts: ecosystem-context.svg · wallet-components.svg
Protocol journeys
The implementation role is the wallet. OpenID4VCI 1.0 is the OAuth-protected issuance API; OpenID4VP 1.0 is the presentation mechanism — each journey below names its standards, the security decision at every step, the negative cases that are tested, and where the evidence lives.
Wallet role in OpenID4VCI 1.0 (pre-authorized + authorization-code with PAR/PKCE)
An issuer offer starts a fresh issuance session. The core decides issuer trust against the operator-signed trusted list, requires a sender-bound token and a fresh c_nonce, gates on the Wallet Unit Attestation binding the device key, has the Secure Enclave sign the proof-of-possession, validates the returned credential's structure, and stores it as a holding — recorded in the audit log.
An issuer's credential offer reaches the shell (QR or deep link) and is fed to the core with the issuer's certificate chain. The core decides issuer trust by X.509 path validation to a PID/attestation anchor on the operator-signed trusted list; an untrusted issuer aborts. The shell exchanges the token (sender-bound, fresh c_nonce); the core refuses to sign the proof-of-possession unless the Wallet Unit Attestation binds the device key; the Secure Enclave signs; the credential response is validated for format and structure, stored as a holding, and the issuance is recorded in the audit log.
abort_untrusted_issuercrates/oid4vciabort_c_nonce_replayedcrates/oid4vciabort_format_mismatch_on_responsecrates/oid4vciunattested_proof_key_is_rejected_in_corecrates/wallet-core/tests/e2e_issuance.rscrates/shell-io/tests/e2e_live_lifecycle.rsformal/lean/IssuanceModel.leanformal/tamarin/oid4vci_issuance.spthyHonest scope Machine + wire flow tested in-repo including over live TCP. On-device orchestration against a real external issuer (browser/eID step, metadata-driven endpoints, mso_mdoc formats) is in progress.
Formal verification
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.
37 theorems across 6 models, 0 sorry — toolchain Lean 4 v4.32.0 (formal/lean/lean-toolchain). lake build PASS for all six models — verification report, 2026-07-19. 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.
23 lemmas proven across 6 models, 0 falsified — all automatic (no interactive steps). Verification report, 2026-07-19. 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.
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)22 Swift tests; UI itself untested | none | none | covered | partial | none | none | 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 |
Security & privacy
The threat model comes first; every control links to a proof, a test, or an architecture element that exists in the repository.
| Adversary | Controls | Evidence | Status |
|---|---|---|---|
| Malicious / compromised verifierOver-asks for claims, replays old requests, or spoofs another RP's identity. |
|
| Verified |
| Network attacker (read / inject / replay / relay)Controls the channel between wallet, issuer, verifier, or a proximity reader. |
|
| Verified |
| Malicious or untrusted issuerTries to plant credentials from outside the trust framework. |
|
| Verified |
| Transaction-data tamperer (payments / signing)Changes amount, payee, or the document between user confirmation and signing. |
|
| Verified |
| Replay attackerRe-submits a previous presentation, payment, signing, or issuance proof. |
|
| Verified |
| Lost / stolen deviceAttacker with physical possession attempts to present or authorize. |
|
| Partial |
| Stale trust: expired, revoked, or mis-chained certificates & credentialsPresents after revocation; issuer/RP certs expired or chained to the wrong anchor. |
|
| Tested |
| Malformed / hostile input (CBOR, COSE, JOSE, JSON, QR)Parser exploitation via crafted credentials, requests, or QR payloads. |
|
| Tested |
| Dependency / build-pipeline compromiseA malicious or vulnerable dependency enters the build. |
|
| Tested |
| Overlay / UI-redressing, phishing verifierTricks the user into consenting to something other than what is displayed. |
|
| 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.
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
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/
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
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
None. The core is sans-IO; no analytics or logging endpoints exist in this codebase.
crates/ (no telemetry dependency in the dependency budget)
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)
Conformance & standards
One row per standard or profile, with its exact version, the wallet's implementation role, the suite that exercised it, the result, the date, and the artifact. External certification has not been performed for any row — planned rows claim nothing.
Signed request objects, DCQL query parsing, type-aware credential selection (meta.vct_values / meta.doctype_value), data-minimised consent, KB-JWT holder binding for SD-JWT VC, and an ISO 18013-5 mdoc DeviceResponse vp_token whose device authentication is signed over the OpenID4VP SessionTranscript — direct_post form response with DCQL-keyed vp_token + echoed state, all exercised, including a full presentation over a live TCP relying-party endpoint and an mdoc presentation verified by an independent party from wire data.
Evidence: crates/oid4vp/ · crates/wallet-core/tests/e2e_mdoc_flow.rs · crates/shell-io/tests/e2e_live_presentation.rs
Notes & limitations mdoc-over-OpenID4VP (DeviceResponse as vp_token) is now implemented and tested end-to-end through wallet-core; direct_post.jwt (JWE) response encryption is not implemented yet. OIDF conformance suite not yet run (see row below); a reachability/wire-shape interop probe against the reference environment does pass.
Pre-authorized and authorization-code (PAR + PKCE S256) machines; in-core issuer-trust decision; Wallet Unit Attestation key gate; device-signed proof-of-possession; c_nonce replay rejection; credential stored exactly as received over a live socket.
Evidence: crates/oid4vci/ · crates/shell-io/tests/e2e_live_lifecycle.rs
Notes & limitations Browser/eID authorization UX and issuer-metadata-driven endpoint discovery on device are in progress. mso_mdoc issuance is wired in-core (a received mso_mdoc credential is parsed into an mdoc holding on receipt); a live external mso_mdoc issuer round-trip is pending.
HAIP-aligned guards are enforced in-core (signed request objects, grant-type allow-list, PKCE S256, sender-bound tokens, attested proof keys).
Evidence: crates/oid4vci/src/lib.rs · crates/oid4vp/src/lib.rs
Notes & limitations Not the full profile: direct_post.jwt response encryption remains (the mdoc-over-OpenID4VP presentation variant is now implemented and tested). No profile-level test run has been executed.
Parse/verify, selective disclosure with digest checking, KB-JWT issuance & verification, alg:none and malformed-input rejection; fuzz target sdjwt_parse.
Evidence: crates/sdjwt/
Notes & limitations Test vectors are repo-generated; alignment against published external vectors is planned.
IssuerSigned/MSO build+verify, DeviceResponse assembly, SessionTranscript binding, reader authentication, session-encryption state machine; canonical-CBOR negative tests; fuzz targets mdoc_cbor and cose_cbor; Kani bounded proofs on the mdoc crate in CI.
Evidence: crates/mdoc/ · crates/iso18013-5/
Notes & limitations BLE/NFC transports are shell adapters not yet implemented on device. The mdoc-over-OpenID4VP handover (the OID4VPHandover SessionTranscript that device authentication signs over) is now wired and tested end-to-end — see crates/oid4vp/tests/mdoc_presentation.rs and crates/wallet-core/tests/e2e_mdoc_flow.rs.
Notes & limitations Not yet executed. The suite is the intended external interop bar once the remaining wire-fidelity item (direct_post.jwt response encryption) lands. No result is claimed.
180 of 684 harmonized requirements mapped to implementation symbols AND named tests; the remaining 504 are explicitly recorded as unassigned (provider-side backends, governance, and P2 credential types not built).
Evidence: traceability/requirements.csv · docs/certification-evidence/verification-report.md
Notes & limitations Mapping coverage, not conformance testing. Kept deliberately high-precision (no keyword inflation).
Notes & limitations FCAF defines harmonized functional test cases; it is not itself an automated executable suite. A pinned FCAF run + report directory exists in the evidence set (docs/certification-evidence/fcaf-reports/, currently empty). No result is claimed.
Article-by-article traceability: authentication-code generation & verification (Art. 4), forgery resistance, payer awareness of amount+payee (Art. 5(1)), dynamic linking to amount, payee name, payee IBAN and currency (Art. 5(1)(c)/5(3)), code integrity (Art. 5(2)), replay rejection, possession-factor requirement.
Evidence: docs/certification-evidence/payment-sca.md
Notes & limitations TS12 wire envelope is approximated pending the published schema; transport confidentiality is the shell's TLS; SCA exemptions (Arts. 10–18) out of wallet scope.
The WYSIWYS authorization core is implemented and formally analysed (Lean QesModel; Tamarin qes.spthy: what_you_see_is_what_you_sign, no_document_substitution).
Evidence: crates/qes/ · formal/tamarin/qes.spthy
Notes & limitations No QTSP integration yet: CSC API v2.0 alignment and a remote-QSCD flow against a qualified trust service are planned. No signature produced today is a qualified signature.
Signed status-list verification, bit-level status lookup, fail-closed policy for remote presentation (unresolvable status blocks presentation).
Evidence: crates/status/
Notes & limitations Fetch-and-refresh scheduling is a shell concern; core decides on verified lists only.
WUA JWT verification binding the device public key at the stated assurance level; issuance proof-of-possession is refused in-core when the key is not attested.
Evidence: crates/wua/
Notes & limitations Wallet-provider WUA issuance service is out of scope of this repository.
Notes & limitations Certification is performed by an accredited CAB under the national scheme; this project maintains the evidence set (docs/certification-evidence/) but has not entered certification. No certification is claimed.
Testing & software quality
205 Rust workspace tests and 22 Swift shell tests pass against real aws-lc-rs cryptography (no mocks), run 2026-07-19. Organised below by assurance purpose, not framework.
Domain rules, guard functions, transitions, encoding/decoding, boundary conditions — every protocol guard maps 1:1 to a named abort reason and has a test.
transitions.rs (per-machine transition tables)crates/oid4vp · oid4vci · payment · qes · w2w · iso18013-5rejects_non_canonical / rejects_duplicate_map_keys / rejects_trailing_bytescrates/cosebinding_is_specific_to_receiver_and_credentialcrates/w2wThe Lean models emit transition traces; six Rust suites replay them against the production machines, byte-for-byte. CI regenerates traces and fails on staleness — the formal model and shipped code cannot silently diverge.
conformance.rs × 6crates/{oid4vp,payment,iso18013-5,oid4vci,qes,w2w}/testsFull flows through the sans-IO core with real aws-lc-rs cryptography: issue → hold → present over live TCP sockets; payment SCA; QES; wallet-to-wallet; status blocking; export integrity; FFI JSON contract.
e2e_live_presentation.rs / e2e_live_lifecycle.rs (real sockets, RP verifies)crates/shell-io/testse2e_flow / e2e_issuance / e2e_payment / e2e_status / qes_flow / w2w_flow / add_credentialcrates/wallet-core/tests22 Swift tests: effect executor, QR classifier, DER→JOSEios/Tests/WalletShellTests51named cases
Every important failure mode becomes a test: replay, wrong nonce/audience, untrusted issuer, revoked/expired credentials, tampered transactions, forged codes, malformed input, misdirected transfers, alg:none.
Distinct test functions whose names encode a rejection/attack case (rejects_*, *replay*, *tamper*, *forged*, *mismatch*, *untrusted*, *revoked*, *invalid*, *malformed*), counted by grep on 2026-07-19 — a subset of the 205 workspace tests.
rts_art4_code_cannot_be_forgedcrates/crypto-backend/tests/regulatory_sca.rsrejects_a_misdirected_transfer_in_corecrates/wallet-core/tests/w2w_flow.rsexport_round_trips_and_detects_tamperingcrates/wallet-core/tests/export.rsrejects_alg_nonecrates/sdjwt4fuzz targets
Coverage-guided fuzzing of the four codec attack surfaces; Kani bounded model checking on the mdoc codec. Both run in CI (bounded time per run).
cargo-fuzz targets in fuzz/fuzz_targets/.
cose_cbor · mdoc_cbor · sdjwt_parse · x509_parsefuzz/fuzz_targets/Kani bounded proofs (cargo kani -p mdoc).github/workflows/ci.yml (tier1-fuzz-kani)clippy -D warnings across the workspace (PASS, 2026-07-19); rustfmt gate; cargo-deny (licenses/bans/sources/advisories) with a written dependency budget; cargo-audit; and a PUBLISHED CycloneDX SBOM (21 crates; wallet-core = 111 runtime components).
clippy PASS — verification reportdocs/certification-evidence/verification-report.mddeny.toml (2 documented build-time-only ignores)deny.tomlPublished SBOM (CycloneDX 1.3)docs/certification-evidence/sbom/73viable mutants caught
cargo-mutants mutates the security-critical OpenID4VP presentation crate and checks the tests catch each change — measuring whether tests constrain behaviour, not just execute it. The initial run caught 52/73 viable mutants (71%); the 21 misses were real test gaps, closed by adding crate-local tests. Re-run: 73/73 viable caught, 0 missed.
Viable mutants caught / total viable, cargo-mutants v27.1.0 on crates/oid4vp with the crate-local test suite (2026-07-19). 8 unviable (non-compiling) mutants excluded per standard practice. Scope: oid4vp only — a test-adequacy measure, not a correctness proof.
cargo mutants -p oid4vpdocs/certification-evidence/mutation-testing.mdDependency-free micro-benchmarks of the hot paths against the real aws-lc-rs backend (ES256 sign ~28.7µs / verify ~83.6µs, SHA-256 ~58ns, SD-JWT parse ~430ns; release, Apple Silicon, 2026-07-19). A flow is dominated by one or two ES256 ops plus one TLS round trip.
cargo run -p benches --releasedocs/certification-evidence/perf-benchmarks.mdA reproducible probe of the EUDI reference environment over platform TLS: the reference issuer's live OpenID4VCI metadata (HTTP 200, 27 configurations — 11 in the SD-JWT VC format this wallet implements) and reference-verifier reachability. Reachability + wire-shape, NOT a conformance pass.
tools/interop/probe.shdocs/certification-evidence/interop.mdCoverage, honestly Code coverage (line/branch/function) has not been measured yet — the number is deliberately absent rather than implied. Coverage also would not prove correctness: the complementary assurance here is machine-checked invariants (Lean), symbolic protocol analysis (Tamarin), oracle-replay conformance binding model to code, adversarial tests, and fuzzing.
Requires an external party (not closeable by our code)
Planned (codeable) — not yet done, no result implied
Operational assurance
tools/evidence/generate.sh regenerates every tier (traceability, tests, Lean, Tamarin, lint) from a clean checkout into the verification report — the page you are reading quotes that artifact.
tools/evidence/generate.sh
Jobs: rust-core (fmt, clippy -D warnings, tests) · supply-chain (cargo-deny, cargo-audit, CycloneDX SBOM) · tier1 (bounded fuzz + Kani) · tier2 (Lean build + oracle-trace staleness gate + replay) · tier3 (Tamarin, advisory) · ios-shell (swift build + test) · traceability import.
.github/workflows/ci.yml
Rust 1.97.1, Lean v4.32.0 and the dependency graph are pinned; a written dependency budget bounds what may enter the build, enforced by cargo-deny (two documented build-time-only advisory ignores).
docs/dependency-budget.md · deny.toml
A reproducible harness fetches the reference issuer's live OpenID4VCI metadata over platform TLS (HTTP 200, 27 configurations — 11 in the SD-JWT VC format this wallet implements) and confirms the reference verifier is reachable. The iOS app runs the same fetch on its real URLSession stack. Reachability + wire-shape only — not a conformance pass.
tools/interop/probe.sh · docs/certification-evidence/interop.md
CycloneDX 1.3 SBOMs are published in-repo (21 crates; wallet-core = 111 runtime components), regenerable from a clean checkout — not just generated transiently in CI.
docs/certification-evidence/sbom/ · tools/evidence/sbom.sh
Published hot-path numbers against the real backend (ES256 sign ~28.7µs / verify ~83.6µs, SHA-256 ~58ns, SD-JWT parse ~430ns; release, 2026-07-19), reproducible with one command.
docs/certification-evidence/perf-benchmarks.md · crates/benches/
Release signing, build provenance/reproducibility, and a published vulnerability-disclosure policy are planned. Threat model, DPIA, key-lifecycle and KAT documents remain stubs pending publication in the certification-evidence set.
docs/certification-evidence/
No published disclosure policy yet — planned alongside the certification evidence set.
docs/certification-evidence/ (pending)
Evidence
Review the architecture decisions, formal models, proof status, conformance mappings, and test artifacts behind the implementation — all in one repository, regenerated by one command.