Evidence-led EUDI credential issuance

Issue trusted credentials.Prove every decision.

A from-scratch German PID and attestation issuer with a small Rust decision kernel, machine-checked safety invariants, and wallet-ready SD-JWT VC and mdoc issuance.

New: hybrid post-quantum issuance
Experimental
The live development issuer now signs an atomic ES256 AND ML-DSA-65 wrapper, backed by shared EUWallet vectors and downgrade-rejection evidence. Not an EUDI credential.
13
Lean 4 theorems
7
Tamarin lemmas
10
Hybrid codec/vector tests
5
Credential profiles

Live issuer

Choose a credential

Each QR code is generated by the running issuer as a short-lived OpenID4VCI credential offer. Nothing below is a static demo token.

Identity proofing

PID Capture: prove it's really you, then get your Personalausweis

Before this issuer mints person-identification data, it has to know the holder is a real, present human bound to a genuine identity document. PID Capture is the front door — a lightweight iOS app, and an install-free App Clip, that reads your ID document's chip, confirms a live face, and hands verified evidence to the issuer, which mints the PID straight into your wallet.

Preview · development

Read the ID chip

Scans the document's machine-readable zone with the camera, then reads the eMRTD chip in a passport or German eID over NFC — the same chip data a border gate trusts.

Confirm a live person

An iProov Genuine Presence Assurance check proves a real, present human — not a photo, mask, or replay — and ties that face to the scanned document.

No install required

Opens instantly from an App Clip Code or QR. The clip links only the shared capture framework — never wallet code or keys — to stay under Apple's 15 MB App Clip budget.

Issued into your wallet

A signed capture session binds the verified evidence to the wallet that requested it, so the issuer mints the PID straight into your EUDI wallet — even a different wallet on another device.

How a capture becomes a credential

01

Open

Tap an App Clip Code or scan a QR — PID Capture launches with no App Store install.

02

Read

Scan the machine-readable zone, then read the document chip over NFC.

03

Prove

Pass an iProov liveness check that binds your live face to the document.

04

Verify

The issuer's capture-session backend checks the chip's authenticity and the liveness result.

05

Issue

VCIssuer mints your PID and offers it to your wallet over OpenID4VCI.

Start a capture

Scan to get a PID issued to your wallet

Point your wallet's scanner at this code. The wallet opens a capture session bound to its own key, launches PID Capture to read your document and confirm a live face, and the issuer mints the PID straight back into that wallet — no account, nothing typed.

Works today with the PID Test Wallet; PID Capture must be installed on the device.

https://pid.advatar.systems

Live today: the capture-session backend, the App Clip domain association, and the cross-wallet correlation that routes an issued PID to the wallet that requested it. In progress: on-device chip reading on physical hardware — the iOS Simulator cannot emulate NFC.

Machine-checked assurance

The signing gate is the proof boundary

The pure Rust authorization kernel mirrors the Lean transition model. Network adapters may prepare a request; only the kernel can authorize a signing command.

Lean 4 · EudiIssuer.Model
authorizeSign_soundproved
disabled_profile_cannot_signproved
authorizeSign_security_gatesproved
pid_authorizeSign_requires_loa_highproved
authorizeSign_respects_wallet_maintenance_boundproved
hybrid_accept_requires_both_componentsproved
hybrid_accept_same_tbsproved
hybrid_accept_generation_agreementproved
classical_downgrade_cannot_hybrid_acceptproved

Checked with the repository-pinned Lean toolchain. Proofs cover the model and its explicit assumptions—not arbitrary adapter code.

7 / 7

Protocol security

Tamarin proves the three issuance properties plus atomic hybrid issuance, same-TBS signatures, downgrade rejection, and generation agreement.

10 / 10

Hybrid executable checks

Issuer tests cover the strict codec, shared TBS vectors, real dual signatures, and the component and credential-wrapper mutation corpora consumed by both repositories.

Keychain

Hybrid key custody

P-256 remains non-exportable. The ML-DSA-65 key is AES-256-GCM wrapped by a Keychain-protected key and its transient plaintext buffer is zeroized.

4 layers

Traceable scope

Normative rules, semantic proofs, protocol analysis, and implementation checks stay distinct.

Experimental hybrid-PQ proof ledger

ES256 AND ML-DSA-65, with no classical downgrade

Development · non-EUDI
13 Lean theorems

AND acceptance, same signed bytes, generation binding, missing-component and downgrade rejection.

7 Tamarin lemmas

Atomic dual signing and same-message agreement under a symbolic perfect-signature model.

Frozen wrapper corpus

HybridCredentialWrapperV1 is jointly frozen; VCIssuer signs with p256/libcrux and EUWallet independently verifies with AWS-LC/RustCrypto, rejecting all twenty-one wrapper mutations.

Proof boundary: Lean checks the explicit acceptance model; Tamarin checks the symbolic protocol; Rust tests connect those conditions to the codec. This is not a proof of cryptographic hardness, side-channel resistance, or external certification. The credential wrapper is jointly frozen as HybridCredentialWrapperV1 (EUWallet issue #119) with a shared wrapper and component corpus consumed byte-identically in both repositories; wallet-side physical-device evidence remains tracked by EUWallet issue #91. Reproduce the issuer evidence with tools/evidence/verify-hybrid-pq.sh and inspect docs/hybrid-pq-verification-report.md.

German EUDI profile

Conformance is an evidence chain

Implemented behavior targets the European Architecture and Reference Framework and German issuer roles. External certification remains a separate legal and assessment milestone.

01
Evidence available

Implemented now

  • OpenID4VCI issuer + authorization metadata
  • PAR, PKCE S256, DPoP and proof JWT
  • SD-JWT VC selective disclosure
  • ISO mdoc MSO + COSE Sign1
02
Evidence available

Verified evidence

  • Lean signing-gate invariants
  • Tamarin issuance properties
  • Hybrid-PQ TBS vector parity
  • Closed credential profile allow-list
  • Replay and one-shot nonce defenses
03
Required

Certification gates

  • Official conformance test suites
  • German authority and CAB assessment
  • Production trust lists and certificates
  • HSM/qualified signing deployment

Accurate status: this is a formally analysed, conformance-targeted development issuer. It is not yet a certified German PID Provider, Attestation Provider, or QEAA Provider, and local Keychain certificates are not production trust anchors.

Inspect the live protocol surface

Metadata is part of the evidence.