AI summaryⓘ
The authors address the challenge of verifying complex cryptographic protocols that involve things like state changes, time-based behavior, and unlimited steps, which are hard for current automated tools to handle. They created a new approach that mixes two techniques—type-based and trace-based reasoning—to verify these protocols in parts, making it easier to manage complex features. Their method is implemented in a tool called LeanDY, built on the Lean proof assistant, allowing a good balance between automation and the ability to handle detailed protocol logic. They show that their framework can handle advanced security properties and use it to formally verify sophisticated blockchain components like payment channels.
cryptographic protocol verificationstateful protocolstype-based reasoningtrace-based reasoningLean proof assistantautomationSegWit blockchainpayment channelsconditional secrecyformal methods
Authors
Simon Jeanteur, Lorenzo Veronese, Magdalena Soltiro, Matteo Maffei
Abstract
Computer-aided formal verification is a widely used approach for the symbolic analysis of cryptographic protocols. However, many modern protocols rely on features that remain challenging for existing techniques. In particular, reasoning about state, time-dependent behavior, inductively defined data structures, unbounded executions, and conditional secrecy requires a level of expressiveness that is difficult to reconcile with effective automation. As a result, protocol verification has largely followed two disjoint paths: fully automated methods with limited expressiveness, or interactive proofs in general-purpose theorem provers that offer flexibility but only limited, non-specialized automation. We present an orthogonal approach that bridges this gap by combining compositional type-based reasoning with trace-based reasoning, enabling modular verification of stateful and unbounded protocols. Guided by the language-and-automation co-design (LAC) principle, our approach delivers protocol-specific automation while retaining high expressiveness. We implement this framework as the LeanDY library for the Lean proof assistant, building on and extending the design of DY*, and combining protocol-specific automation with interactive proofs. Our framework supports, in a unified setting, a broad class of functional and security requirements, including secrecy and authentication for stateful protocols, as well as recursive conditional secrecy for protocols using XOR. We formalize SegWit-style blockchain primitives in LeanDY and demonstrate its expressiveness by carrying out an in-depth formalization of payment channels on top of this blockchain model, verifying punishment mechanisms and properties that depend on chain liveness.