eIDAS 2.0 and the EU Digital Identity Wallet: Formal Verification for EUDIW Security

Regulation (EU) 2024/1183, amending eIDAS (Regulation (EU) No 910/2014), entered into force on 20 May 2024. It mandates that every EU Member State offer citizens a European Digital Identity Wallet (EUDIW) — a state-issued mobile application capable of proving identity, holding verifiable credentials (driving licences, diplomas, professional qualifications), and authenticating to public and private services. Member States must deploy functional EUDIW solutions by 2026.

For developers building authentication services, identity verification APIs, banking portals, healthcare systems, or public administration platforms across the EU, eIDAS 2 creates a new infrastructure compliance layer: the wallet backend, credential issuance infrastructure, and relying party integration must all satisfy security requirements that cannot be met with US-domiciled cloud infrastructure without CLOUD Act exposure.

The formal verification community has been directly involved in eIDAS 2.0 security analysis since early drafts. Tamarin Prover (ETH Zurich / University of Basel), ProVerif (INRIA Paris), and EasyCrypt (IMDEA Madrid / INRIA Paris) have been applied to EUDIW protocol security proofs. Understanding this toolchain is essential for developers building or auditing EUDIW-adjacent systems.

eIDAS 2.0: What Changed from eIDAS 1.0

eIDAS 1.0 (2014) established a baseline for electronic identification and trust services — electronic signatures, seals, timestamps, and cross-border recognition. Its practical uptake was limited: the identification schemes were voluntary for private sector relying parties, and national implementations were fragmented and incompatible.

eIDAS 2.0 (Regulation 2024/1183) introduces mandatory obligations:

Article 5a: EU Digital Identity Wallet obligation. Member States must offer at least one EUDIW to any natural or legal person who wishes to use it. The wallet must be free of charge to individuals, issued by or on behalf of the Member State, available on common mobile platforms, and technically interoperable across all Member States.

Article 5b: Attributes and selective disclosure. EUDIW must support selective disclosure of attributes — a user presenting age verification to a bar may share only the age attribute, not their full national identity document. This requires cryptographic proofs of partial attribute disclosure, typically implemented using Zero-Knowledge Proofs (ZKPs) or SD-JWT (Selective Disclosure JWT, IETF RFC 7519 extension).

Article 5c: Qualified Electronic Attestations of Attributes (QEAAs). Trust service providers can issue QEAAs — qualified attestations of attributes from authoritative sources — analogous to qualified certificates for signatures. Medical councils can issue digital credentials for licensed physicians. Universities can issue verifiable diplomas. Transport authorities can issue digital driving licences.

Article 12a: Common framework and specifications. The European Commission publishes implementing acts specifying the technical architecture, reference implementation, and interoperability requirements for EUDIW. The Architecture and Reference Framework (ARF) is maintained as a living specification by the EU EUDIW Consortium.

Wallet-relying party obligations: Online platforms and services subject to eIDAS 2 must accept EUDIW authentication from users who choose to use it. This applies to banks (already covered by PSD2/DORA), healthcare providers (NIS2), public services (mandatory for e-government), and large online platforms (DSA).

The EUDIW Technical Architecture

The EUDIW reference architecture, as specified in the Architecture and Reference Framework (ARF) v1.4+ documents, consists of:

Wallet Instance: A mobile application installed on the user's device. It holds a wallet attestation (issued by the wallet provider, attesting that the instance is genuine and uncompromised), personal identification data (PID) issued by the Member State's PID Provider, and QEAAs from trust service providers.

PID Provider: A government-authorised entity that issues the Personal Identification Data credential to the wallet. In Germany, this is the Bundesdruckerei (issuer of national identity documents) operating under BSI oversight. In France, ANSSI and the Agence Nationale des Titres Sécurisés (ANTS). In the Netherlands, Rijksdienst voor Identiteitsgegevens (RvIG).

Trust Service Providers (TSPs): Qualified entities that issue QEAAs — verifiable credentials for specific attribute categories. A university TSP issues academic credentials. A medical council TSP issues physician licences. Each TSP must be registered on the EU Trusted List.

Verifier / Relying Party: Any service that requests presentation of EUDIW credentials. A bank onboarding a new customer, a hospital system verifying a physician's licence, an e-government portal authenticating a citizen.

Issuer-Holder-Verifier Model: The core interaction follows the W3C Verifiable Credentials Data Model (VCDM) 2.0 and ISO 18013-5 (mDL — mobile Driving Licence) protocols. Credentials are issued to the wallet, held by the user, and presented to verifiers. The issuer never learns about presentations; the verifier cannot correlate presentations to the issuer.

The protocol-level security of this architecture — particularly the selective disclosure, unlinkability, and forward secrecy properties — is what formal verification tools analyse.

Tamarin Prover: Formal Security Analysis for EUDIW Protocols

Tamarin Prover (developed at ETH Zurich by David Basin, Cas Cremers, and Jannik Dreier; now also at University of Bern and CISPA Helmholtz Centre) is a symbolic security protocol verifier using multiset rewriting rules and a term algebra with equational theories.

Tamarin has been applied to eIDAS-related protocols:

• OpenID Connect 4 Verifiable Presentations (OID4VP): The primary protocol for EUDIW credential presentation. Tamarin models verify authentication, authorisation, and presentation binding properties under the Dolev-Yao adversary model.
• Self-Issued OpenID Provider v2 (SIOPv2): The protocol for self-issued identity assertions from the wallet. Tamarin analysis of key binding and replay attack prevention.
• ISO 18013-5 (mDL): The mobile driving licence protocol which forms the foundation for EUDIW PID and credential issuance. Tamarin and ProVerif analyses published in academic literature.
• SD-JWT security: Selective disclosure JWT analysis covering linkability attacks under selective presentation.

A Tamarin model for an eIDAS-adjacent protocol uses multiset rewriting rules to specify protocol steps:

rule Wallet_PID_Present [color=#8080ff]:
  let
    pid = <'PID', country, name, dob, nationality>
    pid_cred = <pid, sign(pid, ~sk_pidprovider)>
    selective = <name, dob>
    proof = zkp_select(selective, pid_cred)
    presentation = <selective, proof, sign(<selective, proof, ~nonce>, ~sk_wallet)>
  in
  [ !WalletPID($Wallet, pid_cred, ~sk_wallet)
  , !VerifierSession($Verifier, ~nonce, selective_attr) ]
  --[ WalletPresents($Wallet, $Verifier, selective_attr, ~nonce) ]->
  [ Out(<presentation, ~nonce>) ]

Tamarin properties for EUDIW include:

• Authentication: A verifier accepting a credential is guaranteed it was issued by an authentic PID provider or TSP to the claiming wallet.
• Unlinkability: Two presentations from the same wallet to different verifiers cannot be linked by an adversary (critical for preventing correlating surveillance).
• Selective disclosure: A verifier learns only the attributes included in the presentation request, not the full credential contents.
• Replay prevention: A nonce-based mechanism prevents replaying a valid presentation to a second verifier.

Tamarin Prover is developed at:

• ETH Zurich (David Basin — chair of Information Security, Zurich CH; Cas Cremers — now CISPA Saarbrücken DE)
• University of Bern (Jannik Dreier, now Université de Lorraine FR / LORIA)
• CISPA Helmholtz Centre for Information Security (Saarbrücken DE — federal funding, Helmholtz Association)

All primary development institutions are EU-domiciled. Tamarin is released under GPLv3.

ProVerif: Cryptographic Protocol Verification for EUDIW

ProVerif (Bruno Blanchet, INRIA Paris — Équipe Prosecco at Institut national de recherche en sciences et technologies du numérique) is a formal verification tool for cryptographic protocols based on applied pi-calculus. Unlike Tamarin's symbolic rewriting approach, ProVerif reasons about probabilistic polynomial-time adversaries through abstract interpretation.

ProVerif is directly applicable to the EUDIW credential issuance and presentation flows:

mDL/ISO 18013-5 session encryption: ProVerif verifies the session-layer encryption used in proximity-based EUDIW presentations (where the verifier device is physically nearby — a border guard's reader, a bar's age-verification terminal). The protocol uses ECDH-based session keys with HKDF derivation.

OpenID4VP nonce binding: ProVerif analysis of whether the nonce mechanism in OID4VP presentations prevents cross-verifier replay attacks.

EUDIW registration protocol: ProVerif analysis of the wallet attestation issuance flow, where the PID provider authenticates a wallet instance before issuing PID credentials.

Example ProVerif query for EUDIW unlinkability:

(* Unlinkability: two sessions produce computationally indistinguishable traces *)
query attacker(session_id_1) ==> attacker(session_id_2).

(* Authentication: verifier only accepts presentations from legitimate wallets *)
query x: bitstring, y: wallet_id;
  event(VerifierAccepted(x, y)) ==>
  event(WalletPresented(x, y)).

(* Selective disclosure: verifier does not learn unrequested attributes *)
query x: attribute, y: session;
  attacker(x) ==>
  event(AttributeRequested(x, y)).

ProVerif is developed at INRIA Paris (Institut national de recherche en sciences et technologies du numérique — French national research institute, Paris). Bruno Blanchet has led ProVerif development since 2001. INRIA is entirely EU-funded (French Ministry of Higher Education, Research and Innovation; ANR; ERC Horizon Europe grants). No US funding or CLOUD Act exposure in the development chain.

EasyCrypt: Computational Security Proofs for EUDIW Cryptography

EasyCrypt (Gilles Barthe — Max Planck Institute for Security and Privacy, Bochum DE; previously IMDEA Madrid ES; now also ETH Zurich CH; with François Dupressoir, University of Bristol UK/EU) provides machine-checked proofs for cryptographic constructions — the lower layer that formal protocol verifiers assume but do not prove.

For EUDIW, EasyCrypt proofs are relevant for:

• SD-JWT cryptographic security: Proof that the selective disclosure mechanism achieves unlinkability and unforgeability under standard cryptographic assumptions (collision resistance of the hash function, EUF-CMA security of the signature scheme).
• ZKP schemes for attribute proof: Proof of zero-knowledge and soundness for the ZKP constructions used in selective attribute disclosure.
• ECDSA/EdDSA signature security: Machine-checked proofs that the signature schemes used for wallet attestation signing (ECDSA P-256 or Ed25519) achieve EUF-CMA security.

EasyCrypt is developed at MPI-SP (Bochum DE — Max Planck Society, publicly funded German federal research), IMDEA (Madrid ES — Instituto Madrileño de Estudios Avanzados, Spanish Ministry of Science funding), and ETH Zurich (Zurich CH). All EU-domiciled.

The CLOUD Act Problem for EUDIW Backends

eIDAS 2.0 creates a sovereign identity infrastructure. The EUDIW is intended to be the EU's answer to "Big Tech controls your digital identity" — a state-issued, citizen-controlled alternative to Apple ID, Google Account, or Facebook Login. The technical architecture is designed to ensure that:

1. Only the citizen controls their identity credentials
2. No single entity can surveil citizen authentication patterns across services
3. The infrastructure operates under EU law, not US corporate or government jurisdiction

This sovereignty intent is directly undermined when EUDIW backend infrastructure runs on US-domiciled cloud platforms.

The CLOUD Act exposure chain for EUDIW:

The last point is critical: a EUDIW-compliant authentication flow where the relying party runs on AWS/Azure/GCP creates a US-observable audit trail of citizen authentication events — the exact pattern eIDAS 2's unlinkability requirement is designed to prevent at the protocol layer.

For developers building EUDIW-enabled banking portals (DORA + eIDAS 2 overlap), healthcare platforms (NIS2 + eIDAS 2 overlap), or e-government services, the infrastructure layer creates a compliance contradiction: the protocol provides unlinkability, but US-hosted backends hand that data to US government on request.

Germany: BSI TR-02102 mandates cryptographic standards for electronic identity. The NIS2UmsuCG implementation ties into KRITIS infrastructure requirements. EUDIW backends handling German Personalausweis (national ID) digital credentials must operate under BSI oversight — functionally requiring German or EU-native infrastructure.

France: ANSSI actively discourages CLOUD Act-exposed infrastructure for government IT, particularly for identity systems. France's SecNumCloud label (maintained by ANSSI) requires hosting providers to be immune to non-EU laws — explicitly excluding US parent-company structures like AWS Europe or Microsoft Azure DE.

Netherlands: Dutch NCSC publications on digital identity infrastructure explicitly address third-country law exposure. The Dutch government's Rijksoverheid digital identity platform (DigiD successor integrating EUDIW) is required to use Dutch or EU-native hosting.

The EU Formal Verification Stack for EUDIW Security

The EUDIW security ecosystem draws on an entirely EU-native formal methods toolchain:

No CLOUD Act exposure in any development organisation. All tools are EU-funded through national research agencies (ANR FR, DFG DE, NWO NL, SNF CH) and EU-level programmes (ERC, Horizon Europe).

EUDIW and the NIS2 / DORA Intersection

eIDAS 2.0 does not operate in isolation. The EUDIW deployment timeline intersects with two other major EU regulatory frameworks:

NIS2 + EUDIW: Critical infrastructure operators (essential entities under NIS2 Annex I) that integrate EUDIW authentication into their operational systems become relying parties under eIDAS 2 while also subject to NIS2 supply chain security requirements (Art. 21(2)(d)). A hospital integrating EUDIW for physician authentication has a NIS2 supply chain obligation for the EUDIW infrastructure it depends on — which must itself be covered by an EU-native ICT provider.

DORA + EUDIW: Financial institutions (banks, insurers, investment firms under DORA) integrating EUDIW for customer authentication face dual compliance: DORA Art. 28 third-party ICT risk assessment + eIDAS 2 relying party requirements. Both require documented sovereignty chains for the authentication infrastructure.

For a German bank integrating EUDIW:

• DORA Art. 28/30: Document ICT provider sovereignty chains for all critical functions
• eIDAS 2 Art. 5a: Accept EUDIW presentations from customers
• NIS2UmsuCG: Supply chain security for ICT infrastructure
• BSI TR-02102-1: Cryptographic standards for authentication

Running the EUDIW relying party integration on AWS violates DORA Art. 28 (CLOUD Act = undocumented third-country jurisdiction access), creates a NIS2 supply chain documentation gap, and undermines the sovereignty intent of eIDAS 2.

Developer Implementation: EUDIW Integration on EU Infrastructure

For developers building EUDIW-compliant services, the implementation path:

Relying Party (Verifier) Integration: The EUDIW relying party integration uses the OpenID Connect 4 Verifiable Presentations (OID4VP) protocol:

// EUDIW OID4VP Authorization Request
const authorizationRequest = {
  response_type: "vp_token",
  client_id: "https://service.example.eu/eudiw-callback",
  response_uri: "https://service.example.eu/eudiw-callback",
  nonce: crypto.randomUUID(), // Must be single-use, server-side bound
  presentation_definition: {
    id: "age-verification",
    input_descriptors: [{
      id: "pid-age",
      format: { "vc+sd-jwt": { alg: ["ES256"] } },
      constraints: {
        fields: [{
          path: ["$.age_over_18"],
          filter: { type: "boolean", const: true }
        }]
      }
    }]
  }
}

The server-side nonce binding is where CLOUD Act exposure occurs: the nonce validation state, the accepted presentation log, and the session binding must be stored server-side. If that server runs on AWS/Azure/GCP, those records are subject to US legal orders.

EU-native deployment path:

• EU PaaS: Scalingo (FR), Clever Cloud (FR), sota.io (EU-native)
• EU IaaS: OVHcloud (FR), Hetzner (DE), Infomaniak (CH)
• Avoiding: AWS EU Region (Delaware-domiciled, CLOUD Act applicable), Azure DE (Microsoft Ireland, CLOUD Act applicable), GCP EU (Google LLC Delaware, CLOUD Act applicable)

Credential Verification Implementation: SD-JWT verification for EUDIW PID credentials:

import { SDJwt, SdJwtVcVerifier } from "@sd-jwt/core"

// EU-native: sd-jwt library maintained by open consortium
// NO US-domiciled dependency chain for identity verification
const verifier = new SdJwtVcVerifier({
  // Tamarin-verified protocol: selective disclosure only
  allowedAlgorithms: ["ES256", "EdDSA"],
  trustedIssuers: euTrustedList, // EU Trust Service Status List
})

const result = await verifier.verify(vpToken, {
  nonce: expectedNonce,
  audience: relyingPartyId,
  requiredClaims: ["age_over_18"] // SD-JWT: only disclosed attributes
})

Formal Verification on EU Infrastructure: The Deployment Case

If you are building EUDIW-adjacent tooling — a EUDIW integration library, a relying party SDK, a credential issuance service, or a wallet attestation service — the formal verification tools require their own infrastructure:

Tamarin Prover Docker deployment on EU PaaS:

# docker-compose.yml — deploy on sota.io (EU-native)
services:
  tamarin:
    image: tamarin-prover/tamarin-prover:latest
    command: ["server", "--port=3001", "--interface=0.0.0.0"]
    ports:
      - "3001:3001"
    volumes:
      - ./eudiw-models:/models
    # EU-native compute: no CLOUD Act exposure for protocol analysis results

ProVerif CI/CD integration:

# GitHub Actions — runs on EU-native runner or sota.io
- name: Verify EUDIW Protocol Security
  run: |
    proverif eudiw-oid4vp.pv | tee proverif-results.txt
    grep -c "RESULT true" proverif-results.txt | [ $(cat) -eq 3 ] && echo "All security properties verified"

The case for EU-native infrastructure for formal verification CI/CD is structural: protocol analysis results for EUDIW security properties are legally relevant for TSP compliance certification and relying party security attestations. Those results must be generated in an auditable, CLOUD Act-free environment.

See Also

• EU NIS2 Directive 2024: Critical Infrastructure Security and Formal Verification Compliance — Supply chain security for NIS2 essential entities; NIS2 + eIDAS 2 intersection for critical infrastructure
• EU DORA 2025: ICT Risk Management and Formal Verification for Financial Infrastructure — Third-party ICT risk for banks integrating EUDIW; DORA + eIDAS 2 dual compliance
• CryptoVerif: Computational Protocol Verification for EU Cryptographic Standards — Bruno Blanchet's complementary tool to ProVerif for computational security proofs
• ProVerif: Applied Pi-Calculus Protocol Verification — ProVerif detail for cryptographic protocol analysis
• EasyCrypt: Machine-Checked Cryptographic Proofs — Computational security proofs for SD-JWT and ZKP cryptography

eIDAS 2.0 and the EUDIW represent the EU's most ambitious sovereignty project in digital infrastructure. By mandating state-issued wallets with protocol-level unlinkability and formal verification standards built directly into the security analysis ecosystem, the EU is building identity infrastructure that is structurally incompatible with US surveillance-on-demand. But that sovereignty only holds if the infrastructure hosting the wallet backends, relying party integrations, and credential issuance services is itself outside US legal jurisdiction. The formal verification toolchain — Tamarin at ETH Zurich, ProVerif at INRIA Paris, EasyCrypt at MPI-SP and IMDEA — is already EU-native. The compute layer must follow.