Verifpal Takes on TLS 1.3

The TLS 1.3 analysis finally finished overnight. Verifpal 1.4.6 checked nineteen security queries against an active attacker, with two concurrent sessions per principal. Sixteen queries found no attack. Three produced the confidentiality counterexamples we expected. Every verdict matched the expectations written into the model before the run.

I have been looking forward to this result for a while. This year’s work on Verifpal has included a Rust rewrite, a redesigned analysis engine, concurrent sessions, configurable peers, injective authentication, and much more. TLS gave us a chance to put those features to work together. The model outgrew my local machine with 64 GB of RAM, so I rented an EC2 instance with 256 GB and let it run.

Verifpal is a symbolic protocol verifier built around an accessible modeling language and readable attack explanations. This is a milestone for what we can express and analyze with it. The result remains a bounded search: a passing query means that this search found no attack, and Verifpal can miss attacks even within the session bound.

The complete report includes the model, all nineteen verdicts, and the counterexample traces. The most interesting part is how a few lines of the model turn a qualification in the TLS specification into something the engine can actually check.

Our TLS model follows the certificate-authenticated handshake in RFC 9846, with certificates on both sides. It includes the transcript-dependent key schedule, CertificateVerify and Finished, application records in both directions, exporter and resumption secrets, two session tickets, and a server KeyUpdate. Here are its four network flights after certificate provisioning, with the local computations between them omitted:

Client -> Server: gce
Server -> Client: gse, serverFlight
Client -> Server: clientFlight, appData1
Server -> Client: newSessionTicket1, newSessionTicket2, appData2, keyUpdate, appData3

These are symbolic flights, with several TLS messages bundled into encrypted terms. gce and gse are the fresh ephemeral key shares. serverFlight contains the server’s Certificate, CertificateVerify, and Finished; clientFlight contains the client’s corresponding authentication messages. The model begins with attacker[active], and none of these four flights is guarded. The attacker gets to interfere with them.

The server’s key schedule starts directly from the share it receives:

generates se
gse = PUBKEY(se)
dhe = DH_KEX(gce, se)
earlySecret = HKDF(nil, nil, nil)
derivedES = HKDF(earlySecret, labelDerived, nil)
handshakeSecret = HKDF(derivedES, dhe, nil)
transcriptSH = HASH(gce, gse)
cHsTraffic = HKDF(handshakeSecret, labelCHsTraffic, transcriptSH)
sHsTraffic = HKDF(handshakeSecret, labelSHsTraffic, transcriptSH)

generates se gives each server session its own fresh secret. The early secret is public in this handshake without a PSK; secrecy enters through the ephemeral Diffie–Hellman exchange. Different labels separate the client and server traffic secrets, and both derivations include the transcript at ServerHello. The model uses one symbolic HKDF primitive to represent extraction and labeled derivation, with the argument patterns distinguishing their uses.

There is already enough here to explain the first counterexample. The server computes sHsTraffic before authenticating the client. An attacker that supplies a share corresponding to a secret it knows can compute the same Diffie–Hellman result. In the report, it replaces gce with PUBKEY(nil) and derives the shared value as DH_KEX(gse, nil). Here nil is an attacker-known symbolic value; the trace expresses the attacker choosing its own ephemeral secret.

The model deliberately asks both of these questions:

confidentiality? sHsTraffic
confidentiality? sHsTraffic[
    precondition[Server -> Client: appData2]
]

The first query produces a counterexample. The second finds no attack. The difference is the precondition: it restricts the query to executions in which the server actually sends appData2. That send comes after the server has checked the client’s certificate, CertificateVerify, Finished, and first application record. Merely deriving a handshake secret is insufficient to reach it.

This is why preconditions matter so much for protocol modeling. They let us ask about a secret at the point where the endpoint has authenticated its peer. They do not remove the earlier execution from the model or prevent the attacker from opening a connection.

Key agreement uses the same idea on both sides:

equivalence? sApTraffic, sApTraffic_c[
    precondition[Server -> Client: appData2]
    precondition[Client -> Server: clientFlight]
]

The _c value is the client’s independently derived copy of the server application traffic secret. This query compares the two values in executions reaching both sends. It gives an executable interpretation of Appendix F’s qualification, “provided that it completes successfully on each endpoint”. Verifpal’s equivalence? here means equality of the queried values; it is not an observational-equivalence claim about whole protocols.

Peer identity adds another dimension. The client can talk to the honest server, but it can also talk to a server the attacker controls. That second server has a real certificate issued by the same CA. Its private signing key is explicitly disclosed:

principal Mallory[
    knows private mkey
    knows public mallName
    gmSigKey = PUBKEY(mkey)
    leaks mkey
]

The CA signs identity/key pairs for all three participants:

serverCertSig = SIGN(caKey, CONCAT(serverName, gSigKey))
clientCertSig = SIGN(caKey, CONCAT(clientId, clientPk))
mallCertSig = SIGN(caKey, CONCAT(mallName, gmSigKey))

Certificate provisioning and the trust anchor are delivered through guarded messages. For example, CA -> Client: [caPk], [clientCertSig] prevents the network attacker from replacing those provisioned values. The TLS handshake itself still runs over the open network.

Verifpal’s scenarios block supplies the two client configurations:

scenarios[
    Client[peerCert = serverCert]
    Client[peerCert = mallCert]
]

The configured certificate stands for the site the client intends to reach. Using a certificate as the configuration also lets Verifpal track its connection to the compromised key. The client extracts the expected name with expectedName, _, _ = SPLIT(peerCert). After opening the received server flight, it checks the CA signature against that expected name and the received key:

_ = SIGNVERIF(caPk, CONCAT(expectedName, certKey), certSig)?
transcriptCert_c = HASH(transcriptSH_c, certName, certKey, certSig)
_ = SIGNVERIF(certKey, CONCAT(ctxServerCV, transcriptCert_c), serverCV_c)?
transcriptCV_c = HASH(transcriptCert_c, serverCV_c)
sFinishedKey_c = HKDF(sHsTraffic_c, labelFinished, nil)
expectedServerFinished = MAC(sFinishedKey_c, transcriptCV_c)
_ = ASSERT(serverFinished_c, expectedServerFinished)?

The ? makes each operation a check: an unsuccessful check halts the run. The certificate check uses the identity the client intended to contact, while the transcript incorporates the received fields. CertificateVerify is checked using the key from that certificate. Finally, the client computes the expected Finished MAC and checks that it matches what arrived. The server also checks the expected client identity; this model represents a deployment that authorizes a particular certified client.

Once the client has checked the server’s Finished, it prepares its own authentication:

transcriptCCert = HASH(transcriptSFin_c, clientId, clientPk, clientCertSig)
clientCV = SIGN(clientSigKey, CONCAT(ctxClientCV, transcriptCCert))
transcriptCCV = HASH(transcriptCCert, clientCV)
cFinishedKey_c = HKDF(cHsTraffic_c, labelFinished, nil)
clientFinished = MAC(cFinishedKey_c, transcriptCCV)

That first line carries a lot of the protocol’s meaning. transcriptSFin_c already covers the shares, the server’s certificate, CertificateVerify, and Finished. The client’s signature therefore depends on which server it talked to and which handshake it completed. A connection to Mallory gives the attacker client authentication material for that connection, and the analysis can search for ways to reuse it against the honest server.

It also explains another expected confidentiality failure:

confidentiality? clientId

The client sends its identity inside its encrypted authentication flight. In the second scenario it intends to communicate with the compromised certified peer, which can learn that identity. clientId is a private value shared across the client’s runs, so disclosing it there answers the unconditional confidentiality query. This is the boundary between authenticating the recipient and trusting the recipient to keep what it receives secret, consistent with the endpoint-identity discussion in Appendix F.

The same scenarios coexist with two concurrent sessions per principal. An attacker can route values between runs, so the authentication queries need to account for an honestly produced message being accepted twice. Verifpal’s authentication queries are injective: each acceptance must correspond to a distinct sending event. The model asks about both handshake flights and all three application records:

authentication? Server -> Client: serverFlight
authentication? Client -> Server: clientFlight
authentication? Client -> Server: appData1
authentication? Server -> Client: appData2
authentication? Server -> Client: appData3

All five find no attack in this run. Sessions intentionally configured with compromised peers do not inherit the security claims made for honest peer configurations. Their outputs can still give the attacker material to try against an honest connection.

Records make the interplay between replay, key derivation, and protocol state especially concrete. The server derives a write IV and encrypts its first application message like this:

sApIv = HKDF(sApTraffic, labelIv, nil)

generates appMsg2
appData2 = AEAD_ENC(sApTraffic, HASH(sApIv, seq2), appMsg2, recordHeader)

Why seq2 for the first application message? The server has already used records zero and one for the two session tickets. The additional data is the public record header. The nonce depends on the write IV and the record’s position, and the receiver computes the corresponding nonce locally.

TLS combines the padded sequence number and IV with XOR. Verifpal has no XOR theory, so the model explicitly abstracts this as HASH(iv, seq). It also uses each traffic secret to stand for its derived record write key. These choices preserve the modeled dependencies while leaving algebraic properties of the concrete nonce construction outside the analysis.

This detail helped make the run practical. An earlier version of the model generated a fresh nonce for each record and sent it beside the ciphertext. Computing the nonce locally brought the model closer to TLS and removed extra attacker-controlled wire values that had widened the search.

The two tickets derive their PSKs separately from the resumption secret:

generates ticketNonce1, ticketNonce2
resPsk1 = HKDF(resumptionSecret, labelResumption, ticketNonce1)
resPsk2 = HKDF(resumptionSecret, labelResumption, ticketNonce2)
newSessionTicket1 = AEAD_ENC(
    sApTraffic, HASH(sApIv, seq0), ticketNonce1, recordHeader
)
newSessionTicket2 = AEAD_ENC(
    sApTraffic, HASH(sApIv, seq1), ticketNonce2, recordHeader
)

The ticket messages are reduced to the encrypted ticket nonces needed for this derivation. The fresh nonces distinguish the PSKs even though both come from one connection’s resumption secret. That gives us a specific separation property to test by leaking one PSK and querying the other. The run covers ticket issuance and PSK derivation; a resumed handshake belongs to a separate model.

Next, the server sends KeyUpdate under the current key, derives the next traffic secret and IV, and restarts the sequence number:

keyUpdate = AEAD_ENC(
    sApTraffic, HASH(sApIv, seq3), updateNotRequested, recordHeader
)
sApTraffic1 = HKDF(sApTraffic, labelTrafficUpd, nil)
sApIv1 = HKDF(sApTraffic1, labelIv, nil)
generates appMsg3
appData3 = AEAD_ENC(sApTraffic1, HASH(sApIv1, seq0), appMsg3, recordHeader)

The client checks the encrypted update and computes the same next-generation secret before opening appData3. We can now express key compromise at two different times. All handshakes and application records happen in phase zero. Phase one hands both long-term signing keys to the attacker:

phase[1]

principal Server[
    leaks sigKey
]

principal Client[
    leaks clientSigKey
]

Phase two discloses the server’s updated sending secret and the first ticket’s PSK:

phase[2]

principal Server[
    leaks sApTraffic1, resPsk1
]

This is a useful feature of Verifpal’s phase model: knowledge becomes available when the disclosure happens. A signing key leaked after the handshake cannot be spent retroactively to forge a signature at an earlier check. But recorded ciphertexts remain available for decryption if a later disclosure supplies what the attacker needs.

The application-data and ticket queries make the consequences visible:

confidentiality? appMsg1
confidentiality? appMsg2
confidentiality? appMsg3
confidentiality? resPsk2

Only appMsg3 produces a counterexample. Its trace is particularly direct: the attacker observes appData3, receives sApTraffic1 from the leak, derives sApIv1, computes HASH(sApIv1, seq0), and decrypts the record. Every ingredient is accounted for.

The earlier application messages remain confidential in this search. Leaking the signing keys does not provide the ephemeral Diffie–Hellman secrets. Leaking the updated server traffic secret does not give the attacker an inverse of the derivation from the previous generation. The second ticket’s PSK also remains confidential despite disclosure of the first.

The direction of the key-update claim matters. Appendix F.2 discusses protection of earlier traffic after a key change and deletion of the previous key. It also explains that a compromised traffic secret allows computation of future traffic secrets on that connection. This model tests the former direction by leaking the updated secret. It does not model recovery after compromise or an endpoint compromise that hands over every old secret still in memory.

Across the nineteen queries, the result is:

Every passing verdict is labeled “search exhausted at 2 sessions.” The engine has explored the search space it defines for these parameters. That space remains incomplete, and the session bound is explicit. A reported counterexample is a witness against the symbolic model as written. The paper describing the redesigned engine explains how backward search proposes attacker actions and a separate validator checks their derivability and re-executes the affected roles before a violation is recorded.

The model’s scope is equally explicit. It fixes one cipher suite and group. It omits negotiation and downgrade protection, HelloRetryRequest, PSK and 0-RTT handshakes, post-handshake client authentication, the exporter interface, alerts, and record padding. Hello randoms, EncryptedExtensions, and CertificateRequest are omitted from the transcript abstraction. Record ordering is represented through the fixed record positions and nonces. Key-compromise impersonation is not tested: that would require a handshake after a long-term key leaks, while these handshakes all run in phase zero.

These are concrete choices a reader can inspect in the model source, alongside the queries they support. The generated report preserves the full source used in the run, so the verdicts and the model can be reviewed together.

That is what makes this result exciting to me. We can follow a requirement from the TLS specification into a few lines of Verifpal, change the point at which a secret is queried or the peer a client contacts, and see why the answer changes. The same model exercises concurrent sessions, authentication, identity binding, key updates, and carefully timed disclosures. Getting it to finish has given us a substantial new example to teach from, scrutinize, and improve.

I have shared the result with the TLS Working Group and would welcome feedback, especially on the abstractions and the correspondence between the queries and Appendix F. The model and report are there to be read, and I hope others find them as interesting to work through as I did.