Feedback-ID: i6d3949ed:Fastmail
From: Nadim Kobeissi <nadim@symbolic.software>
Content-Type: multipart/alternative;
	boundary="Apple-Mail=_B67F673B-18AD-4BFE-8981-5A3A45CDE615"
Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3864.700.51.1.1\))
Message-Id: <DE297422-C54E-4C29-9FB7-15F5A97E6489@symbolic.software>
Date: Mon, 7 Sep 2026 11:12:42 +0200
To: cfrg@ietf.org,
 ufmrg@irtf.org
Message-ID-Hash: U5R3254U2TNVMTW23EBWE2X2GPRKGBAZ
Precedence: list
Subject: =?utf-8?q?=5BUfmrg=5D_A_Verifpal_milestone=3A_TLS_1=2E3_modeled_and_verified?=
 =?utf-8?q?_with_concurrent_sessions_and_staged_compromise?=
Archived-At: 
 <https://mailarchive.ietf.org/arch/msg/ufmrg/AmqTd58KwC6ISYyBiJ2pad9h8fE>


--Apple-Mail=_B67F673B-18AD-4BFE-8981-5A3A45CDE615
Content-Transfer-Encoding: quoted-printable
Content-Type: text/plain;
	charset=utf-8

Hi everyone,

I=E2=80=99m 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=E2=80=99m =
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=E2=80=99s CertificateVerify, while =
the analysis searches for attacks on the honest connection. The binding =
of client authentication to the server=E2=80=99s certificate and =
handshake transcript is therefore directly relevant.

3. Queries conditioned on protocol progress. Verifpal=E2=80=99s =
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=E2=80=99s=
 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=E2=80=99 long-term =
signing keys. Phase 2 discloses the server=E2=80=99s 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=E2=80=99s 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=E2=80=99s 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=E2=80=99s record under the previous key generation.

C. The client=E2=80=99s 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=E2=80=99s 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, "=46rom Toy to Instrument: Seven Years =
of Verifpal=E2=80=9D [5].

For me, the exciting part is being able to turn this many of TLS=E2=80=99s=
 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=20
[2] https://www.rfc-editor.org/info/rfc9846/
[3] https://www.rfc-editor.org/info/rfc9846/#appendix-F=20
[4] https://verifpal.com/res/examples/tls13.pdf =20
[5] https://eprint.iacr.org/2026/1654=20

Nadim Kobeissi
Symbolic Software =E2=80=A2 https://symbolic.software


--Apple-Mail=_B67F673B-18AD-4BFE-8981-5A3A45CDE615
Content-Transfer-Encoding: quoted-printable
Content-Type: text/html;
	charset=utf-8

<html aria-label=3D"message body"><head><meta http-equiv=3D"content-type" =
content=3D"text/html; charset=3Dutf-8"></head><body =
style=3D"overflow-wrap: break-word; -webkit-nbsp-mode: space; =
line-break: after-white-space;"><div>Hi =
everyone,</div><div><br></div><div>I=E2=80=99m 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.</div><div><br></div><div>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=E2=80=99m particularly happy about how much we could express =
in one model.</div><div><br></div><div>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.</div><div><br></div><div>Several Verifpal features made =
this analysis especially interesting:</div><div><br></div><div>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.</div><div><br></div><div>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=E2=80=99s CertificateVerify, while the analysis =
searches for attacks on the honest connection. The binding of client =
authentication to the server=E2=80=99s certificate and handshake =
transcript is therefore directly relevant.</div><div><br></div><div>3. =
Queries conditioned on protocol progress. Verifpal=E2=80=99s =
preconditions let a query apply only to executions that reach a =
particular send. For example:</div><div><br></div><div>&nbsp; =
confidentiality? sApTraffic[</div><div>&nbsp; &nbsp; &nbsp; =
precondition[Server -&gt; Client: appData2]</div><div>&nbsp; =
]</div><div><br></div><div>&nbsp; Here, the server sends appData2 only =
after checking the client=E2=80=99s authentication and Finished. The =
key-agreement query carries preconditions for both endpoints. This lets =
us express the completion qualifications attached to the security =
claims.</div><div><br></div><div>4. Compromise at different times. The =
handshake and application exchange happen in phase 0. Phase 1 discloses =
both endpoints=E2=80=99 long-term signing keys. Phase 2 discloses the =
server=E2=80=99s 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.</div><div><br></div><div>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=E2=80=99s XOR construction. Nonces are computed =
locally rather than sent alongside =
ciphertexts.</div><div><br></div><div>The three reported confidentiality =
failures are useful illustrations of the boundaries being =
tested:</div><div><br></div><div>A. The server=E2=80=99s 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.</div><div><br></div><div>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=E2=80=99s record under =
the previous key generation.</div><div><br></div><div>C. The client=E2=80=99=
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.</div><div><br></div><div>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=E2=80=99s PSK also remains confidential despite =
disclosure of the first.</div><div><br></div><div>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.</div><div><br></div><div>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, "=46rom Toy to Instrument: Seven Years of =
Verifpal=E2=80=9D [5].</div><div><br></div><div>For me, the exciting =
part is being able to turn this many of TLS=E2=80=99s 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!</div><div><br></div><div>[1] =
https://verifpal.com&nbsp;</div><div>[2] =
https://www.rfc-editor.org/info/rfc9846/</div><div>[3] =
https://www.rfc-editor.org/info/rfc9846/#appendix-F&nbsp;</div><div>[4] =
https://verifpal.com/res/examples/tls13.pdf &nbsp;</div><div>[5] =
https://eprint.iacr.org/2026/1654&nbsp;</div><div>
<meta charset=3D"UTF-8"><br>Nadim Kobeissi<br>Symbolic Software =
=E2=80=A2&nbsp;https://symbolic.software<br>
</div>

<br></body></html>=

--Apple-Mail=_B67F673B-18AD-4BFE-8981-5A3A45CDE615--