Email Gateway (May 24 2026 at 19:07): Email Gateway (May 24 2026 at 19:07):From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle is at the centre of Apple's verification chain for cryptography:
https://security.apple.com/blog/formal-verification-corecrypto/
Email Gateway (Jun 04 2026 at 14:25):From: Tassilo Lemke <cl-isabelle-users@lists.cam.ac.uk>
Hi all,
I was wondering if anybody knows if similar verifications have been done for protocol implementations, particularly linking them with the inductive security analysis model (see L. Paulsons works), or other information-flow models. While the verification here certainly looks interesting, it is (as far as I can tell) primarily focusing on using FIPS specifications (and their respective Isabelle models) to verify implementations of cryptographic algorithms, but protocols (like TLS) don't seem to be covered in this.
Are there any verifications of concrete implementations of protocols that anybody knows of? Or at least some approaches towards that? Also, are there possibly other information-flow models which are used to bridge the model-vs-implementation gap? I assume modelling information (and its content and flow) on an implementation-level is a great challenge. I'm currently a bit lost and can't seem to find anything concrete on this, so any insights or further reading tips would be much appreciated (I'd like to stick to Isabelle, I'm aware of tools like Tamarin/ProVerif/etc.)!
Best,
Tassilo Lemke
Von: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> im Auftrag von Lawrence Paulson <lp15@cam.ac.uk>
Gesendet: Sonntag, 24. Mai 2026 21:07:01
An: isabelle-users
Betreff: [isabelle] A blueprint for formal verification of Apple corecrypto
Isabelle is at the centre of Apple's verification chain for cryptography:
https://security.apple.com/blog/formal-verification-corecrypto/
Email Gateway (Jun 04 2026 at 15:45):From: "Achim D. Brucker" <adbrucker@0x5f.org>
Hi,
in addition to Larry's excellent work (which you seem to know already),
* Hess, A. V., Mödersheim, S. A., Brucker, A. D., & Schlichtkrull, A.
(2025). PSPSP: A tool for automated verification of stateful protocols
in Isabelle/HOL. Journal of Computer Security, 33(6), 425–469.
https://doi.org/10.1177/0926227x251358741 - the Isabelle formalisation
and implementation is also in the AFP:
https://isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html
Best,
Achim
On 04/06/2026 15:25, Tassilo Lemke (via cl-isabelle-users Mailing List)
wrote:
Hi all,
I was wondering if anybody knows if similar verifications have been
done for protocol implementations, particularly linking them with the
inductive security analysis model (see L. Paulsons works), or other
information-flow models. While the verification here certainly looks
interesting, it is (as far as I can tell) primarily focusing on using
FIPS specifications (and their respective Isabelle models) to verify
implementations of cryptographic algorithms, but protocols (like TLS)
don't seem to be covered in this.Are there any verifications ofconcrete implementations of protocols
that anybody knows of? Or at least some approaches towards that? Also,
are there possibly other information-flow models which are used to
bridge the model-vs-implementation gap? I assume modelling information
(and its content and flow) on an implementation-level is a great
challenge. I'm currently a bit lost and can't seem to find anything
concrete on this, so any insights or further reading tips would be
much appreciated (I'd like to stick to Isabelle, I'm aware of tools
like Tamarin/ProVerif/etc.)!Best,
Tassilo Lemke
Von: cl-isabelle-users-request@lists.cam.ac.uk
<cl-isabelle-users-request@lists.cam.ac.uk> im Auftrag von Lawrence
Paulson <lp15@cam.ac.uk>
Gesendet: Sonntag, 24. Mai 2026 21:07:01
An: isabelle-users
Betreff: [isabelle] A blueprint for formal verification of Apple
corecrypto
Isabelle is at the centre of Apple's verification chain for cryptography:https://security.apple.com/blog/formal-verification-corecrypto/
Email Gateway (Jun 05 2026 at 10:22):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm afraid I haven't done any recent work on protocol verification. My inductive method is flexible but the proof obligations are tricky to prove. There has been a lot of progress since. Given the difficulty of such work, one would expect the verification of an implementation to involve refinement from an abstract protocol to executable code, but refinement (at least if done naïvely) does not preserve security properties: refinement steps that look correct can nevertheless introduced vulnerabilities.
Larry
On 4 Jun 2026, at 15:25, Tassilo Lemke <tassilo.lemke@tum.de> wrote:
I was wondering if anybody knows if similar verifications have been done for protocol implementations, particularly linking them with the inductive security analysis model (see L. Paulsons works), or other information-flow models. While the verification here certainly looks interesting, it is (as far as I can tell) primarily focusing on using FIPS specifications (and their respective Isabelle models) to verify implementations of cryptographic algorithms, but protocols (like TLS) don't seem to be covered in this.
Last updated: Jun 12 2026 at 04:13 UTC