The Electronic Passport, Modeled in Verifpal

Suppose someone records the radio traffic while your passport’s chip is being read at an airport. They can’t decrypt it. A month later, they get a copy of your passport’s photo page from a hotel that kept a scan. If the recording was protected only by the older passport protocol, that page gives them enough information to decrypt it.

The password used by that protocol is made from your passport number, date of birth and expiry date. All three are printed on the page. The idea is that a reader should have to see the document before it can read the chip, but a saved scan keeps working after you’ve taken your passport back. A newer protocol uses the same password and still manages to protect old recordings. The difference is in how the reader and chip agree on their encryption keys.

We worked through this example, and twelve others, in Verifpal, our tool for analyzing cryptographic protocols. The starting point was Joop van de Pol’s article on electronic passports, published by Trail of Bits in October 2025. In each model we describe what the passport and reader send and what an attacker can hear or change. Verifpal then looks for a way to read something private or persuade a reader to accept the wrong message.

The password on the page

The two lines of letters, numbers and < symbols below the photograph are the machine-readable zone, or MRZ. A reader scans the passport number and the two dates from those lines, including their check digits. The chip already knows the same values. Neither side needs to send this password over the radio.

The older protocol is called Basic Access Control, usually shortened to BAC. It turns the password into encryption keys, then uses those keys to exchange some fresh random material. The chip contributes one value and the reader contributes another. They combine the two to make new keys for the rest of the conversation. Protected messages also carry a message authentication code, or MAC: a tag computed with a shared secret key that lets the recipient check whether a message has been altered.

Those random contributions are also in the recording, encrypted under keys derived from the printed password. Someone who learns that password can decrypt the contributions, combine them exactly as the chip and reader did, and recover the conversation’s keys. Everything they need is in the recording.

Our bac.vp model lets the inspection finish before giving the attacker the password. This is the part that represents the later leak:

phase[1]

principal Passport[
	leaks mrz
]

phase[1] advances the model beyond the completed inspection, and leaks mrz adds the password to the attacker’s knowledge. Verifpal can then reconstruct the keys and decrypt the recorded passport data, including the facial image. This is what it means for BAC to lack forward secrecy: losing a long-term secret exposes earlier conversations too. Here we are considering traffic protected by BAC; some passports switch to another set of keys later in the inspection.

An attacker might also guess the password. Dates and document numbers have limited uncertainty, and check digits help catch typing mistakes rather than add secrecy. A recorded BAC exchange gives the attacker a way to test guesses without contacting the chip again. Verifpal does not attempt that guessing process. Giving it the password models what happens after a successful guess, or after obtaining the scan.

When a search finds no attack, we cannot conclude that the protocol is secure. We checked each model with one and two concurrent sessions per participant, and Verifpal can miss attacks even within that limit. A passing result means no attack was found in those runs.

The same password, different keys

The replacement is PACE, short for Password Authenticated Connection Establishment. It still lets the reader use information printed on the passport, but the keys for the conversation also depend on secrets created for that particular exchange.

PACE uses Diffie-Hellman key agreement. The reader and chip each choose a private value and exchange a corresponding public value. From their own private value and the other’s public one, they can compute the same shared secret. An eavesdropper sees the public values but cannot recover that secret. The private values are ephemeral, meaning they are chosen afresh for each conversation.

The password is involved in setting up this exchange so that the two sides can check that they know it. In the PACE variant we modeled, called Generic Mapping, there are two Diffie-Hellman exchanges. The first shared secret and a random value encrypted under the password determine the starting point for the second exchange. The second produces the secret from which the conversation’s keys are derived.

In pace.vp, we disclose the password afterward, just as we did for BAC. This time the search finds no way to decrypt the recording. The attacker can open the initial encrypted random value, but still lacks the private values from the Diffie-Hellman exchanges. Verifpal simplifies the mathematics of Generic Mapping, so this checks the modeled dependence on those secrets; it does not verify PACE’s curve arithmetic or analyze password guessing.

The distinction is useful outside passports too. A password can help two participants recognize each other without becoming the secret that protects every past conversation. Someone who already knows it can still connect to the chip as a reader, provided they can reach it. PACE cannot tell how they obtained the password.

ICAO is now retiring BAC. The February 2026 amendment to Doc 9303 Part 11, §4.1, requires PACE in newly issued electronic travel documents from 1 January 2027 and excludes BAC from newly issued documents from 1 January 2028. That changes what countries issue on those dates. Older passports will still be in use afterward.

Copying the chip

Encryption is only part of the reader’s job. It also needs to establish that the name and photograph came from the country that issued the passport. Someone could put invented details on a chip and encrypt them just as successfully.

The issuing country digitally signs the passport’s contents. The reader checks that signature using a public key it trusts, then checks that the contents have not changed. The passport standard calls this Passive Authentication. It works on stored data, without asking the chip to perform a new cryptographic operation.

The files have names that appear throughout the models. DG1 contains the MRZ information and DG2 the facial image. A file called EF.SOD contains a signed list of hashes, one for each data group. A hash acts as a fingerprint of the file’s contents: the reader computes it and compares it with the one the country signed. Doc 9303 Part 10 defines these files, and Part 12 explains how the reader establishes trust in the signing key.

Copy the files, though, and you copy the valid signature with them. Passive Authentication will still succeed. There has been no forgery: the country really did sign those details.

In inspect_pa.vp, the attacker already knows the printed password and can talk to both the chip and the reader. It runs PACE separately with each, reads the genuine passport data on one connection, and sends it again on the other. The reader accepts the country’s signature even though the encrypted response came from the attacker.

This is why the model reports an authentication failure without finding a forged photograph or name. The contents are genuine; the reader has not established who supplied them. If the attacker saves those signed files, it can present them again without the original chip. A photograph of the page alone does not contain the signed files: it supplies the password that lets the attacker read them when the chip is within reach.

Asking the chip to do something a copy cannot

To detect a copied chip, the reader needs a test that cannot be answered from its readable files. Active Authentication gives the passport its own private signing key, designed to remain inside the chip. The corresponding public key is stored in DG15 and covered by the country’s signature, so the reader can check which public key it should trust.

The reader sends a newly chosen random challenge and asks the chip to sign it. An old response will not answer a new challenge. Copying all the readable files will not help either, as long as the private key stays secret.

In inspect_aa.vp, the passport’s part is one line:

aaSig = SIGN(aaKey, chal)

The reader checks it with:

_ = SIGNVERIF(dg15_t, chal, aaSig)?

Here dg15_t is the public key the reader checked against the country’s signed data. The ? tells Verifpal that a failed check stops the run. The search finds no way for the attacker to supply a signature that the passport did not make.

The attacker can still ask the real passport for help. It forwards the reader’s challenge to the chip, gets the signature, and forwards it back. The original passport must be reachable, but the attacker does not need its private key. It can continue reading and sending the other data through the two PACE connections it controls. A fresh signature establishes that the chip took part somewhere; it does not establish that the reader’s encrypted connection ends at that chip.

Chip Authentication addresses that gap by using the chip’s private key to establish the encrypted connection itself. The reader supplies a fresh Diffie-Hellman public key, and the chip uses its own private key to compute their shared secret. The reader can compute the same secret using the chip’s public key, stored in DG14. They switch to new encryption keys, and the chip demonstrates that it has the private key by producing responses protected with those keys.

There is still a check to finish. A fake chip could supply its own public key and complete that exchange too. The reader must verify that the key in DG14 is one the issuing country signed. The standard is explicit about this: TR-03110 Part 1 §3.4.2 says to treat the chip as genuine only after that verification succeeds.

Our inspect_ca.vp query therefore counts only inspections that reach the final acceptance step. It finds no way to substitute the encrypted data response in those completed inspections. The attacker can still forward the entire exchange without decrypting it, so this does not establish physical proximity. And an attacker with the printed password can still open its own connection to the real chip and read the facial image. So far, we have checked the passport’s credentials without demanding any credentials from the reader.

Giving the reader permission to see fingerprints

A passport may also store fingerprints, in DG3, or iris data, in DG4. These have stricter access rules than the photograph. Knowing the printed password should not be enough to read them.

Terminal Authentication lets the chip check the reader’s permission. The reader presents certificates that authorize it to access particular data, then proves that it holds the private key named in its certificate by signing a fresh challenge from the chip. Countries use a separate certificate hierarchy for this permission: the Country Verifying Certification Authority delegates to Document Verifiers, which certify individual readers. This is separate from the authority that signs the passport’s contents. TR-03110 Part 1 §§2.2 and 3.5 specifies both the hierarchy and the checks.

The reader signs more than the challenge. It also signs an identifier for the passport and the public key it used to establish the Chip Authentication connection. Including that key lets the chip check that the reader being granted permission is the one that will be able to decrypt the fingerprints.

In inspect_ta.vp, the attacker can read the photograph, but the search finds no disclosure of the fingerprints. We then isolate the public-key check in two smaller models using BAC. In these, the passport identifier is its document number and check digit, which the attacker already knows.

eac_bac.vp includes the public key, caPkT, in the reader’s signature:

taSig = SIGN(termKey, CONCAT(docNumber, rPicc_t, caPkT))

eac_bac_unbound.vp removes it. The attacker can now establish separate encrypted connections with the passport and a legitimate reader, carry the passport’s challenge to the reader, and bring the signed answer back. The passport sees a valid signature from an authorized reader and releases the fingerprints over a connection the attacker can decrypt.

Put caPkT back, and the search no longer finds that disclosure. The legitimate reader signs its own public key, but the chip’s connection was established using the attacker’s public key. The mismatch stops the release of the fingerprints.

These three Terminal Authentication models deliberately leave out the reader’s check of DG14 against the country’s signature, so that we can give the attacker this opportunity. The full inspection procedure performs that check before Terminal Authentication and rejects the substituted chip key. PACE’s dynamic binding also uses the chip’s ephemeral PACE public key as its identifier, providing another connection between the signature and the current exchange. The unbound example demonstrates the purpose of a required field, rather than a flaw in the standard.

Recognizing a passport without reading it

An eavesdropper might be interested in whether the same person passed two readers, even if it cannot learn their name. Our tracking models put the same passport at a hotel desk and an airport gate. The attacker records both conversations and tries to find a relationship between them.

For BAC, knowing the printed password is enough. The chip’s initial responses carry MACs made with a key derived from that password. In track_bac.vp, the attacker computes those tags for both recordings and confirms that the same key works. Without the password, the search finds no such link, although it does not attempt to guess the password.

PACE makes this harder for someone who is only listening. Its authentication tags use fresh keys from the Diffie-Hellman exchanges. The attacker cannot compute those keys, even with the printed password, and track_pace.vp finds no link between the recordings.

The encrypted random value at the start of PACE deserves a closer look. An attacker can try decrypting it with a password, but what would a wrong answer look like? The plaintext is just a random block, with no recognizable structure. A wrong password also produces a plausible random block. There is no success or failure signal to confirm the guess. Hirschi, Baelde and Delaune explain how an observable failure at this step would create a tracking opportunity.

All three of our tracking models describe a passive listener. Someone who sends messages to the passport has more options. In Chothia and Smirnov’s 2010 attack, the attacker sends a passport a BAC message recorded earlier. The original passport recognizes the MAC but rejects the old challenge inside it. A different passport rejects the MAC. If those failures produce different errors or take different amounts of time, the attacker can recognize the original passport without knowing its password.

Arapinis, Chothia, Ritter and Ryan analyzed the error-message attack formally; Horne and Mauw’s later work found further active tracking attacks against BAC and PACE. Those analyses compare observable behavior across whole conversations. Verifpal’s unlinkability? query looks for a relationship between values and does not capture those differences in how a check fails. Our results also say nothing about someone who knows the password and tries it on nearby passports to see which one answers successfully.

Using the passport online

A phone can read the passport chip and use its contents to identify the holder to a website. Some applications use zero-knowledge proofs to disclose less information: for example, proving that the holder is over eighteen without revealing their date of birth.

The signed passport data can support that claim, but a service may also want to know that someone has access to the chip now. Otherwise, anyone who saved the necessary signed files could keep using them. Active Authentication seems a natural addition: the website sends a fresh challenge, the phone asks the passport to sign it, and the website checks the answer.

Suppose you do this for a dishonest website. It can get the challenge from a bank where it is trying to identify itself as you, then send that challenge to your phone. Your passport signs it, your phone returns the answer, and the website passes it to the bank. You have kept your passport in your hands and used an encrypted connection throughout. The problem is that the chip was never told which service you intended to use.

remote_aa.vp models that sequence. We give the phone two possible destinations, the bank and a dishonest verifier, using Verifpal’s scenarios block:

scenarios[
	Phone[rpPub = bankPub]
	Phone[rpPub = evilPub]
]

The phone knows the public key of the service it connects to, and the phone–passport link is protected from interference. Even so, Verifpal finds that the bank accepts the signature relayed by the dishonest website. The attacker does not have to get near the passport.

In remote_aa_bound.vp, the phone combines the challenge with the identity of the service it actually connected to before asking the chip to sign:

toSign = HASH(rpPub, chal_p)

Now the signature obtained through the dishonest website covers that website’s key. The bank expects its own key and rejects the answer. With one session per participant, the search finds no attack in this model. The phone must obtain the service identity from the connection it authenticated: if it simply lets the website supply a name to include, the dishonest website can name the bank.

With two sessions per participant, Verifpal finds a different attack, which does not use the dishonest website. It exploits a simplification in our model of the connection between the phone and the bank. The phone chooses the connection key on its own and sends it encrypted to the bank. Each encrypted message also has a nonce, a value that must never be used twice with the same key, and in our model every challenge uses the same fixed nonce. The attacker opens its own session with the bank and receives a challenge. It also delivers a copy of the phone’s key message to a second bank session, so two bank sessions encrypt different challenges under the same key and nonce. That repetition lets the attacker forge a message on the phone’s connection, which it uses to pass along the challenge from its own session. The phone includes the bank’s key, as intended, and the passport signs. The attacker presents the signature in its own session, and the bank accepts it.

The binding cannot help here, because the phone really was connected to the bank. The weak point is the connection as we modeled it. In TLS, the server also contributes fresh values to the connection keys, so a copied key message would not give two server sessions the same keys. As written, though, remote_aa_bound.vp does not pass at two sessions.

WebAuthn uses this idea to protect browser logins. What the authenticator signs covers the challenge and the browser’s origin, along with a hash of the relying-party identifier. The service checks those values, as required by the WebAuthn Level 3 Recommendation published in August 2026. An authentication response obtained on one website should not become a usable answer on another.

There is a practical obstacle to applying our example directly to a passport: Active Authentication accepts an eight-byte challenge, as specified in §6.1.2.1. Verifpal’s idealized HASH does not have that size constraint. Fitting the binding into 64 bits would need a concrete design and an analysis of collisions and guessing. The one-session result shows how the intended binding works, but does not establish a deployable change to existing passports.

We have not modeled a zero-knowledge proof system here, and a particular application may have other protections or enrollment requirements. Hiding the data inside a proof does not, on its own, stop this relay. There is also a separate human question: having access to a passport’s chip does not establish that you are its rightful holder. NIST SP 800-63A-4 distinguishes checking that identity evidence is genuine from checking that it belongs to the applicant. The chip protocols address only part of that job.

Results and model details

The thirteen models follow ICAO Doc 9303 Part 11, including the February 2026 amendment, and BSI TR-03110 Part 1. Results agreed at one and two concurrent sessions per participant, except for remote_aa_bound.vp, discussed above. The three track_ models use a passive attacker; the other ten let the attacker interfere with messages. Every “no attack found” below refers to those bounded searches. In the files, Terminal means the passport reader.

Some simplifications deserve attention if you want to work with the files. Protocol-specific key derivations become HKDF. BAC combines its two random contributions with XOR; the model hashes them because Verifpal has no XOR theory. PACE’s Generic Mapping involves group operations that Verifpal cannot express directly, so a hash enters key derivation in place of the mapped generator. We model only that PACE variant, without algorithm negotiation or concrete public-key validation. PACE also supports a printed Card Access Number where available; our examples use the MRZ. In these files, mrz represents the access-control fields and dg1 the remaining MRZ information, such as name and nationality.

We also leave out the command framing and byte-level encodings. One detail we had to put back was the sequence counter in Secure Messaging, which protects the reads after access control. An early model omitted it, and Verifpal could swap the response containing the issuer’s signature with the response containing the passport data: both had valid MACs under the same key. The standard includes the counter in each MAC to protect the message’s position in the conversation. We represent those positions with distinct public labels. This was an error in our model, resolved by restoring a detail from the specification.

The Active Authentication signatures abstract the standardized encodings, including the extra chip-generated message component used with RSA. Certificate handling is simplified too: the terminal models collapse the Document Verifier level into the country authority directly certifying the reader. Certificate expiry, revocation and compromise of an issuer’s signing key are outside the analysis, as are physical proximity, timing and observable error responses.

Expiry is a particularly awkward problem for a chip without a clock. It cannot simply check today’s date. TR-03110 Part 3 §2.5 instead lets it advance its estimate using dates in specified certificates it has successfully verified. A reader’s signature is only one part of deciding whether its permission is still valid.

The files are in examples/epassport, with each model’s assumptions written at the top. To try them, start with bac.vp and pace.vp: both read the same data and disclose the same password afterward, so you can follow exactly where their treatment of a recorded conversation differs.