2026-04-05·10 min read·sota.io team

Deploy ProVerif to Europe — Bruno Blanchet 🇫🇷 (INRIA Paris), the Cryptographic Protocol Verifier that Formally Proved TLS 1.3, on EU Infrastructure in 2026

In 2016, before RFC 8446 was published, the IETF TLS working group faced a question that years of interoperability testing could not answer: is TLS 1.3 actually secure? The protocol was designed to eliminate the vulnerabilities that made TLS 1.2 — and its predecessors — targets of POODLE, BEAST, DROWN, FREAK, and Logjam. But "designed to be secure" and "proved to be secure" are different claims.

The answer came from ProVerif — an automated cryptographic protocol verifier developed by Bruno Blanchet at INRIA Paris. In a landmark analysis conducted jointly by Karthikeyan Bhargavan 🇮🇳 (INRIA Paris 🇫🇷), Bruno Blanchet 🇫🇷 (INRIA Paris 🇫🇷), Nadim Kobeissi 🇱🇧, and colleagues, ProVerif was used to formally verify the security properties of the TLS 1.3 handshake and record layer against a symbolic Dolev-Yao adversary. The results, published as the Verified Models and Reference Implementations for the TLS 1.3 Standard (IEEE S&P 2017), provided the IETF TLS working group with formal evidence that the new protocol achieved its security goals — and caught a subtle flaw in an earlier draft that was corrected before standardisation.

TLS 1.3 protects virtually every HTTPS connection on the internet. Every time a user's browser loads a web page over HTTPS, a TLS 1.3 handshake occurs — and that handshake has been formally proved secure by a tool built at INRIA Paris, France's national computer science research institute.

Bruno Blanchet: Applied Pi-Calculus and Automated Protocol Verification

Bruno Blanchet 🇫🇷 is a senior researcher (Directeur de Recherche) at INRIA Paris (Institut National de Recherche en Informatique et en Automatique). He completed his PhD at the École Normale Supérieure Paris in 2001, supervised by François Fages 🇫🇷 (INRIA Rocquencourt).

ProVerif grew from Blanchet's doctoral work on type-based verification of cryptographic protocols. The first public version appeared at CSFW 2001 (IEEE Computer Security Foundations Workshop) as An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. The theoretical foundation was formalised jointly with Martín Abadi 🇦🇷 (DEC Systems Research Center, later UC Santa Cruz and Google) in the applied pi-calculus: a process calculus for cryptographic protocols that extends Milner's π-calculus with equational theories over cryptographic terms.

The applied pi-calculus paper — Mobile Values, New Names, and Secure Communication (Abadi + Blanchet, POPL 2001, predecessor to the full theory in JACM 2018) — established the theoretical basis. Where Milner's CCS/π-calculus (Blog #133/#136) reasons about process communication abstractly, the applied pi-calculus adds the ability to reason about cryptographic operations (encryption, signatures, MACs, Diffie-Hellman) under equational theories that capture what an adversary can compute.

The INRIA institutional context matters: INRIA Paris is home to the Prosecco project team (now Cascade), which has produced ProVerif, the miTLS reference implementation of TLS, the HACL* formally verified cryptographic library (used in Firefox and the Linux kernel), and the tls13-spec ProVerif models. This is a single institution — a French national research institute — providing the formal foundations for internet security at global scale.

The Dolev-Yao Model and Applied Pi-Calculus

ProVerif works in the symbolic model of cryptography (also called the Dolev-Yao model, after Danny Dolev and Andrew Yao's 1983 paper). In this model:

Cryptographic primitives are black boxes with algebraic properties (equational theories)
The adversary is Dolev-Yao: can intercept, replay, modify, and inject messages, but cannot break well-formed cryptography
Protocol messages are symbolic terms over a signature (constructors for encryption, signatures, nonces, etc.)

This abstraction trades computational guarantees (which require the computational model — reduction to hard mathematical problems) for automation: ProVerif can decide security properties automatically for a wide class of protocols, while computational proofs require significant manual effort.

Applied Pi-Calculus Syntax

A TLS 1.3 client process in applied pi-calculus notation:

(* Cryptographic primitives *)
fun encrypt(bitstring, key): bitstring.
fun decrypt(bitstring, key): bitstring.
equation forall m: bitstring, k: key;
  decrypt(encrypt(m, k), k) = m.

fun sign(bitstring, skey): bitstring.
fun verify(bitstring, bitstring, pkey): bool.
equation forall m: bitstring, sk: skey;
  verify(m, sign(m, sk), pk(sk)) = true.

(* Diffie-Hellman *)
fun exp(G, exponent): G.
equation forall a: exponent, b: exponent;
  exp(exp(g, a), b) = exp(exp(g, b), a).

(* TLS 1.3 client hello *)
let TLSClient(serverPK: pkey, csk: skey) =
  new clientNonce: nonce;
  new clientDH: exponent;
  let clientShare = exp(g, clientDH) in
  out(net, (clientNonce, clientShare));  (* ClientHello *)
  
  in(net, (serverNonce: nonce, serverShare: G, serverCert: bitstring, serverFinished: bitstring));
  
  (* Verify server certificate *)
  if verify(serverShare, serverCert, serverPK) = true then
  
  (* Derive handshake keys via HKDF (modelled as PRF) *)
  let dhSecret = exp(serverShare, clientDH) in
  let hs_secret = HKDF_extract(dhSecret, clientNonce, serverNonce) in
  let server_hs_key = HKDF_expand(hs_secret, label_s_hs) in
  let client_hs_key = HKDF_expand(hs_secret, label_c_hs) in
  
  (* Verify server finished *)
  if verify(hs_secret, serverFinished, server_hs_key) = true then
  
  (* Derive application keys *)
  let master_secret = HKDF_extract(hs_secret, zero) in
  let server_app_key = HKDF_expand(master_secret, label_s_ap) in
  let client_app_key = HKDF_expand(master_secret, label_c_ap) in
  
  (* Application data — secrecy goal *)
  new appData: bitstring;
  out(net, encrypt(appData, client_app_key));
  event ClientFinished(serverPK, server_app_key, client_app_key).

Horn Clause Resolution

ProVerif translates process terms into Horn clauses — logical rules of the form H1 ∧ … ∧ Hn → C — and uses resolution to derive what an adversary can compute. The derivation procedure is a sound (and often complete) decision procedure for reachability of adversary-controlled states.

(* ProVerif internally generates Horn clauses like: *)
(* If adversary knows encrypted(m, k) and k, adversary knows m *)
attacker(decrypt(x, k)) :- attacker(x), attacker(k).

(* If attacker can compute all inputs to encrypt, can compute output *)
attacker(encrypt(x, k)) :- attacker(x), attacker(k).

(* Protocol rule: server sends encrypted response *)
attacker(encrypt(response, server_key)) :- 
  attacker(clientHello),
  ... (* server process derivation *)

The secrecy query asks: can the adversary derive the secret term? ProVerif answers this by checking if the Horn clause derivation reaches a clause of the form attacker(secret). For TLS 1.3, the query is: can the adversary derive the session application keys? ProVerif proves: no.

Security Properties ProVerif Can Verify

Secrecy

(* Is appData secret from the adversary? *)
query attacker(appData).
(* Expected result: false — ProVerif cannot find a derivation *)

For TLS 1.3: ProVerif proved that the application data keys cannot be derived by a Dolev-Yao adversary, even with full control of the network — including replay attacks, man-in-the-middle on unverified connections, and compromise of earlier session keys (forward secrecy).

Authentication via Correspondence Assertions

(* Injective agreement: server finished ↔ client sees matching keys *)
event ServerFinished(pkey, key, key).
event ClientFinished(pkey, key, key).

query pk: pkey, sk: key, ck: key;
  inj-event(ClientFinished(pk, sk, ck)) ==>
  inj-event(ServerFinished(pk, sk, ck)).
(* Each client completion corresponds to exactly one server completion *)

Injective correspondence captures authentication with replay protection: every client completion of the handshake corresponds to a unique server completion with the same keys. Non-injective correspondence captures weaker authentication that permits replay.

Equivalence Properties

ProVerif can also verify observational equivalence — whether two processes are indistinguishable to an adversary. This captures privacy properties:

(* Are two users' sessions indistinguishable? Captures anonymity/unlinkability *)
let ProcessA = ... (* session with user A *)
let ProcessB = ... (* session with user B *)

query ProcessA ≈ ProcessB.
(* If true: adversary cannot distinguish A from B — privacy holds *)

This is the property needed to verify 5G authentication privacy (IMSI/SUPI concealment) and eIDAS 2.0 selective disclosure (ZKP-based credentials where the verifier cannot link presentations).

Industrial Applications

TLS 1.3 (RFC 8446)

The tls13-spec project (INRIA Paris Prosecco team, 2016–2018) modelled the TLS 1.3 specification in ProVerif + the F* proof assistant. The ProVerif models verified:

Handshake secrecy: session keys are secret
Forward secrecy: past sessions are secure even if long-term keys are compromised later (DHE and PSK+DHE modes)
Mutual authentication: certificate-based authentication in both directions
Session resumption (0-RTT mode): security under weaker assumptions (replay-safe only for idempotent requests)

A subtle cross-protocol attack was found in an early TLS 1.3 draft via the ProVerif analysis and corrected before standardisation. The IETF TLS working group cited the formal analysis in the RFC 8446 Security Considerations section.

Signal Protocol

The Signal Protocol — used by Signal, WhatsApp, and iMessage — was formally verified using ProVerif. The Double Ratchet algorithm and X3DH (Extended Triple Diffie-Hellman) key agreement were modelled in applied pi-calculus and verified for:

Secrecy of message content
Post-compromise security (future secrecy after key compromise — the "ratchet" property)
Deniability (messages cannot be attributed to sender by a third party)

5G Authentication (EAP-AKA′)

The 5G NR (New Radio) authentication protocols — 5G-AKA and EAP-AKA′ — were formally analysed using ProVerif by Jannik Basin 🇩🇪 (ETH Zurich 🇨🇭), Jannik Dreier 🇩🇪 (Université de Lorraine 🇫🇷 / INRIA Nancy 🇫🇷), Lucca Hirschi 🇫🇷 (INRIA Saclay 🇫🇷), Sasa Radomirovic 🇷🇸 (University of Dundee 🇬🇧), Ralf Sasse 🇩🇪 (ETH Zurich 🇨🇭), and Vincent Stettler 🇨🇭 (ETH Zurich 🇨🇭) — the TAMARIN tool was the primary vehicle (using similar symbolic methods), but ProVerif models were also developed.

The analysis found that 5G-AKA had a linkability flaw: an adversary could track a user's location without breaking cryptography, just by replaying authentication messages. The 3GPP standardisation body corrected the 5G-AKA specification before finalisation. This is the kind of subtle privacy flaw — not a cryptographic break, but a protocol design error — that symbolic model checkers like ProVerif are specifically designed to find.

European Regulatory Context

NIS2 Directive (EU 2022/2555)

The NIS2 Directive requires operators of essential services (energy, transport, banking, health, water, digital infrastructure) to implement "appropriate and proportionate technical and organisational measures" including cryptographic protocols. ProVerif-verified protocols provide auditable evidence that the cryptographic protocols protecting critical infrastructure have been formally analysed — evidence that NIS2 Article 21 risk management documentation can reference directly.

French critical infrastructure operators (EDF 🇫🇷 nuclear, SNCF 🇫🇷 railway, Thales 🇫🇷 defence communications) are NIS2-regulated entities. The INRIA/ANSSI (Agence Nationale de la Sécurité des Systèmes d'Information 🇫🇷) ecosystem — ProVerif + ATSEC evaluations + Common Criteria — provides a complete French-government-backed formal verification chain for NIS2-regulated cryptographic protocols.

DORA (Digital Operational Resilience Act, EU 2022/2554)

The Digital Operational Resilience Act requires financial sector firms (banks, insurance, asset managers, CCPs) to maintain ICT risk management frameworks including cryptographic protocol resilience. DORA Article 9 requires "state-of-the-art" cryptographic protocols — and ProVerif formal analysis is increasingly cited as evidence of "state-of-the-art" in DORA compliance documentation for financial sector firms under ECB and EBA supervision.

eIDAS 2.0 (EU 910/2014 revised)

The European Digital Identity Wallet (EUDI Wallet, ARF 1.4) uses OpenID4VP (Verifiable Presentations) and SD-JWT (Selective Disclosure JWTs) for credential exchange. The privacy properties of the EUDI Wallet — selective disclosure (present only required attributes), unlinkability (presentations from the same credential are not linkable), holder binding (only the legitimate holder can present credentials) — are exactly the kind of observational equivalence properties that ProVerif can formally verify.

ANSSI 🇫🇷 (Agence Nationale de la Sécurité des Systèmes d'Information) is the French national cybersecurity authority and ENISA partner. ANSSI has contributed to eIDAS 2.0 security analysis using ProVerif-based formal methods, making ProVerif directly relevant to the EU digital identity infrastructure rollout.

EU AI Act (Article 9) + CRA 2027

The EU AI Act Article 9 requires "state-of-the-art" risk management for high-risk AI systems. AI systems that communicate over network protocols (API security, model-serving authentication) can use ProVerif-verified protocol stacks as evidence that the communication layer meets the "state-of-the-art" bar. The Cyber Resilience Act (CRA) 2027 requires CE-marked software products to "handle, store and transmit only data, commands, functions or scripts that are necessary for the intended purpose" — ProVerif verification of the protocol stack supports this requirement.

EU Verification Ecosystem

ProVerif is not isolated: it is part of a broader European ecosystem of cryptographic protocol verification tools:

TAMARIN Prover (ETH Zurich 🇨🇭 + Universität Erlangen-Nürnberg 🇩🇪 + INRIA Nancy 🇫🇷 + Universitat Pompeu Fabra 🇪🇸): Schmidt + Meier + Cremers + Basin (ETH). Multiset rewriting + temporal logic. Used for 5G-AKA analysis, EMV payment protocol, WPA3 Wi-Fi. Handles unbounded sessions and stateful protocols that ProVerif approximates.

CryptoVerif (Bruno Blanchet 🇫🇷, INRIA Paris 🇫🇷): Blanchet's computational model companion to ProVerif. Proves protocols secure against probabilistic polynomial-time adversaries — cryptographic hardness reductions rather than Dolev-Yao. Used to verify TLS 1.3 in the computational model (IEEE S&P 2017, joint with ProVerif symbolic analysis).

EasyCrypt (IMDEA Software Institute 🇪🇸 Madrid + INRIA 🇫🇷 + ETH Zurich 🇨🇭): Gilles Barthe 🇫🇷 (IMDEA / MPI-SP Bochum) + François Dupressoir 🇫🇷 + Pierre-Yves Strub 🇫🇷 (École Polytechnique 🇫🇷). Proof assistant for computational cryptography. Used to verify HACL* (formally verified cryptographic implementations in F*).

HACL* (INRIA Paris Prosecco/Cascade 🇫🇷): Karthikeyan Bhargavan 🇮🇳 + Jonathan Protzenko 🇩🇪 (Microsoft Research). Formally verified implementations of ChaCha20-Poly1305, Curve25519, ECDSA, AES-GCM, BLAKE2, SHA-2 and SHA-3 in F* 🇫🇷 (Nikhil Swamy + Catalin Hritcu 🇷🇴 INRIA, MSR). Deployed in Firefox, the Linux kernel, and the WireGuard VPN protocol.

The geography: Paris (INRIA) → ProVerif + CryptoVerif + HACL* + F* + miTLS. Zurich (ETH) → TAMARIN + EasyCrypt + Gobra + Nagini. Madrid (IMDEA) → EasyCrypt + formal crypto. This is a coherent EU cluster, funded through EU Horizon projects and French/Swiss national research programmes — with no US Cloud Act exposure.

Deploying a ProVerif Analysis Service on sota.io

A protocol verification service that runs ProVerif analyses and stores results in EU PostgreSQL:

FROM debian:bookworm-slim AS builder

RUN apt-get update && apt-get install -y \
    ocaml ocaml-findlib \
    libocamlgraph-ocaml-dev \
    wget make git \
    && apt-get clean

# Build ProVerif from source (OCaml — same stack as CompCert/Why3/Coq/Frama-C)
RUN wget https://bblanche.gitlabpages.inria.fr/proverif/proverif2.05.tar.gz && \
    tar xzf proverif2.05.tar.gz && \
    cd proverif2.05 && \
    ./build && \
    cp proverif /usr/local/bin/proverif

FROM debian:bookworm-slim

RUN apt-get update && apt-get install -y \
    postgresql-client \
    libocamlgraph-ocaml-dev \
    && apt-get clean

COPY --from=builder /usr/local/bin/proverif /usr/local/bin/proverif
COPY analyze_protocol.sh /usr/local/bin/analyze_protocol
RUN chmod +x /usr/local/bin/analyze_protocol

CMD ["analyze_protocol"]

#!/bin/bash
# analyze_protocol.sh — ProVerif analysis + sota.io PostgreSQL result storage

PROTOCOLS_DIR="${PROTOCOLS_DIR:-/workspace/protocols}"
DATABASE_URL="${DATABASE_URL:-}"

for pv_file in "$PROTOCOLS_DIR"/*.pv; do
  protocol_name=$(basename "$pv_file" .pv)
  
  # Run ProVerif analysis
  output=$(proverif "$pv_file" 2>&1)
  exit_code=$?
  
  # Parse results
  if echo "$output" | grep -q "RESULT.*true"; then
    verdict="VERIFIED"
    details=$(echo "$output" | grep "RESULT" | head -20)
  elif echo "$output" | grep -q "RESULT.*false"; then
    verdict="ATTACK_FOUND"
    details=$(echo "$output" | grep "RESULT\|Attack\|trace" | head -20)
  else
    verdict="INCONCLUSIVE"
    details=$(echo "$output" | tail -20)
  fi
  
  # Count verified and falsified queries
  verified=$(echo "$output" | grep -c "RESULT.*true" || echo "0")
  falsified=$(echo "$output" | grep -c "RESULT.*false" || echo "0")
  
  # Store in EU PostgreSQL on sota.io
  psql "$DATABASE_URL" -c "
    INSERT INTO protocol_verification_results (
      protocol_name,
      pv_file_hash,
      verdict,
      verified_queries,
      falsified_queries,
      proverif_output,
      analyzed_at
    ) VALUES (
      '${protocol_name}',
      '$(sha256sum "$pv_file" | cut -d' ' -f1)',
      '${verdict}',
      ${verified},
      ${falsified},
      \$\$${details}\$\$,
      NOW()
    ) ON CONFLICT (protocol_name, pv_file_hash) DO UPDATE SET
      verdict = EXCLUDED.verdict,
      verified_queries = EXCLUDED.verified_queries,
      falsified_queries = EXCLUDED.falsified_queries,
      analyzed_at = EXCLUDED.analyzed_at;"
  
  echo "=== ${protocol_name}: ${verdict} (${verified} verified, ${falsified} attacks found) ==="
done

Protocol verification results — including attack traces for falsified queries — stored in EU-jurisdiction PostgreSQL. Protocol models, cryptographic design decisions, and security evidence remain under French/EU jurisdiction. NIS2 Article 21 compliance documentation, DORA ICT risk management evidence, and eIDAS 2.0 protocol security analysis all remain Cloud Act-free.

ProVerif is open source (GPLv2), maintained by Bruno Blanchet at INRIA Paris (bblanche.gitlabpages.inria.fr/proverif). Binaries and source available. CryptoVerif (computational model companion) is also maintained by Blanchet at INRIA. sota.io has a free tier — deploy your first ProVerif analysis pipeline in minutes and generate formally verified cryptographic protocol evidence for NIS2, DORA, and eIDAS 2.0 compliance on EU infrastructure.