Email Gateway (Jun 13 2023 at 12:48): Email Gateway (Jun 13 2023 at 12:48):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a new entry, Cryptographic Standards, by A Whitley.
From the abstract:
In this set of theories, we express well-known crytographic standards in the language of Isabelle. The intention is that these translations will be used to prove that any particular implementation matches the relevant standard. With that in mind, the overriding principle is to adhere as closely as possible, given the syntax of HOL, to the written standard. It should be obvious to any reader, regardless of their past experience with Isabelle, that these translations exactly match the standards. Thus we use the same function and variable names as in the written standards whenever possible and explain in the comments the few times when that is not possible.
This looks like a valuable resource for anybody wanting to model or verify cryptographic protocols and software down to the bit level.
It’s online at https://www.isa-afp.org/entries/Crypto_Standards.html
Larry Paulson
Last updated: Apr 28 2024 at 20:16 UTC