DyLean is a framework for the symbolic analysis of cryptographic protocols in Lean.

With DyLean, you can specify cryptographic protocols, write their expected security properties in the symbolic model, prove that these security properties indeed hold (!), and check that your protocol specifications capture intended behaviors (e.g. honest executions or known attacks exist).

Disclaimer. We are actively working on DyLean, expect breaking changes. If you want to use DyLean, please contact us.

Papers linked to DyLean

Papers about DyLean:

• Bob DyLean: A Framework for the Symbolic Analysis of Cryptographic Protocols in Lean (eprint)

Papers related to DyLean:

• Introduction to the proof methodology: A Verification Framework for Secure Group Messaging (Chapter 2)
• Composing security proofs: DY* Unchained: Now with Composable Security Proofs and Precise Compromise Scenarios (Section 3)