CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection
This addresses the challenge of automating formal verification for cryptographic protocols, which is currently complex and time-consuming, though the work appears incremental as it focuses on benchmarking existing models rather than introducing new methods.
The paper tackles the problem of automating vulnerability detection in cryptographic protocols by creating a benchmark to assess LLMs' ability to identify flaws through interaction with the Tamarin theorem prover, achieving results that provide insights into integrating LLMs with symbolic reasoning systems for cybersecurity applications.
Cryptographic protocols play a fundamental role in securing modern digital infrastructure, but they are often deployed without prior formal verification. This could lead to the adoption of distributed systems vulnerable to attack vectors. Formal verification methods, on the other hand, require complex and time-consuming techniques that lack automatization. In this paper, we introduce a benchmark to assess the ability of Large Language Models (LLMs) to autonomously identify vulnerabilities in new cryptographic protocols through interaction with Tamarin: a theorem prover for protocol verification. We created a manually validated dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents. Our results about the performances of the current frontier models on the benchmark provides insights about the possibility of cybersecurity applications by integrating LLMs with symbolic reasoning systems.