[Ufmrg] A Verifpal milestone: TLS 1.3 modeled and verified with concurrent sessions and staged compromise

[Nadim Kobeissi <[e-mail]>]

Hi everyone,

I’m excited to share a milestone for Verifpal [1]: after an overnight run, Verifpal 1.4.6 has completed the analysis of a substantial TLS 1.3 model, checking nineteen security queries against an active attacker. Sixteen queries returned no attack, and three produced the expected confidentiality counterexamples. The results match the expectations documented in the model before the run.

For those unfamiliar with Verifpal, it is a symbolic protocol verification tool built around an accessible modeling language and readable attack explanations. This analysis brings together much of the work that has gone into its redesigned engine this year, and I’m particularly happy about how much we could express in one model.

The model follows the certificate-authenticated TLS 1.3 handshake in RFC 9846 [2], with mutual authentication. It includes CA-issued certificates and expected-identity checks, CertificateVerify with distinct client/server contexts, Finished verification, the transcript-dependent key schedule, application records in both directions, exporter and resumption secrets, two session tickets, and a server KeyUpdate followed by application data under the updated key.

Several Verifpal features made this analysis especially interesting:

1. Concurrent sessions and injective authentication. Each principal runs two concurrent sessions. The attacker can route values between runs, and authentication queries look for duplicate acceptance as well as forgery. This lets the model ask whether an honestly produced message can be accepted more times than it was sent.

2. Different peers across runs. A `scenarios` block configures the client to communicate either with the honest server or with a legitimately certified server whose signing key the attacker holds. This gives the attacker access to client behavior in a connection to a malicious peer, including the client’s CertificateVerify, while the analysis searches for attacks on the honest connection. The binding of client authentication to the server’s certificate and handshake transcript is therefore directly relevant.

3. Queries conditioned on protocol progress. Verifpal’s preconditions let a query apply only to executions that reach a particular send. For example:

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

  Here, the server sends appData2 only after checking the client’s authentication and Finished. The key-agreement query carries preconditions for both endpoints. This lets us express the completion qualifications attached to the security claims.

4. Compromise at different times. The handshake and application exchange happen in phase 0. Phase 1 discloses both endpoints’ long-term signing keys. Phase 2 discloses the server’s updated application traffic secret and the PSK associated with the first ticket. One analysis therefore exercises forward secrecy, protection of earlier traffic after a key update, and separation between ticket PSKs.

5. Nonce-aware records. AEAD calls explicitly include the nonce and additional data. Record nonces depend on the write IV and sequence number, with the sequence number restarting under the updated key. The model represents the IV/sequence-number combination as `HASH(iv, seq)`, a symbolic abstraction of TLS’s XOR construction. Nonces are computed locally rather than sent alongside ciphertexts.

The three reported confidentiality failures are useful illustrations of the boundaries being tested:

A. The server’s handshake traffic secret is obtainable before client authentication. The attacker supplies its own ephemeral key share and derives the corresponding handshake secret. The unconditional query therefore fails. The same query, conditioned on the server reaching its application-data send after authenticating the client, finds no attack.

B. Compromising the updated traffic secret exposes the record encrypted under it. The trace shows the attacker taking the explicitly leaked secret, deriving the write IV and nonce, and decrypting appData3. The earlier application messages remain confidential in this search, including the server’s record under the previous key generation.

C. The client’s identity is disclosed in its connection to the compromised certified peer. The client is explicitly configured to contact that peer, so unconditional secrecy of its identity is too strong a requirement. This illustrates the distinction between authenticating a server and trusting that server with the identity disclosed to it.

These outcomes align with the qualifications discussed in Appendix F [3]. The remaining results include all five injective authentication queries, both traffic-secret freshness queries, agreement on the server application traffic secret under the completion preconditions, and confidentiality of the appropriately conditioned handshake, application, and exporter secrets. The second ticket’s PSK also remains confidential despite disclosure of the first.

Every passing verdict is explicitly labeled "search exhausted at 2 sessions." This means that Verifpal found no attack in the search it performed. Its search is bounded and incomplete, including within the session bound. The model also makes specific abstractions: it fixes one cipher suite and group, uses traffic secrets to stand for record write keys, and excludes negotiation, HelloRetryRequest, resumed/0-RTT handshakes, and post-handshake client authentication.

The generated LaTeX report [4] contains the complete model, every verdict, and the counterexample traces. The engine and its guarantees are described in my recent paper, "From Toy to Instrument: Seven Years of Verifpal” [5].

For me, the exciting part is being able to turn this many of TLS’s carefully qualified security claims into an executable model that remains approachable enough to read alongside the specification. I would very much welcome feedback from the WG, especially on the modeling abstractions and the correspondence between the queries and Appendix F. Thank you!

[1] https://verifpal.com 
[2] https://www.rfc-editor.org/info/rfc9846/
[3] https://www.rfc-editor.org/info/rfc9846/#appendix-F 
[4] https://verifpal.com/res/examples/tls13.pdf  
[5] https://eprint.iacr.org/2026/1654 

Nadim Kobeissi
Symbolic Software • https://symbolic.software