CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection

• URL: http://arxiv.org/abs/2411.13627v1
• Date: Wed, 20 Nov 2024 14:16:55 GMT
• Title: CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection
• Authors: Cristian Curaba, Denis D'Ambrosi, Alessandro Minisini, Natalia Pérez-Campanero Antolín,
• Abstract summary: We introduce a benchmark to assess the ability of Large Language Models to autonomously identify vulnerabilities in new cryptographic protocols. We created a dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents.
• Score: 41.94295877935867
• License:
• Abstract: 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.

Related papers

• Automating Prompt Leakage Attacks on Large Language Models Using Agentic Approach [9.483655213280738]
  This paper presents a novel approach to evaluating the security of large language models (LLMs) We define prompt leakage as a critical threat to secure LLM deployment. We implement a multi-agent system where cooperative agents are tasked with probing and exploiting the target LLM to elicit its prompt.
  arXiv  Detail & Related papers  (2025-02-18T08:17:32Z)
• Cryptanalysis via Machine Learning Based Information Theoretic Metrics [58.96805474751668]
  We propose two novel applications of machine learning (ML) algorithms to perform cryptanalysis on any cryptosystem. These algorithms can be readily applied in an audit setting to evaluate the robustness of a cryptosystem. We show that our classification model correctly identifies the encryption schemes that are not IND-CPA secure, such as DES, RSA, and AES ECB, with high accuracy.
  arXiv  Detail & Related papers  (2025-01-25T04:53:36Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach [3.9155346446573502]
  This paper introduces Auto-modeling of Formal Verification with Real-world Prompting for 5G and NextG protocols (AVRE) AVRE is a novel system designed for the formal verification of Next Generation (NextG) communication protocols.
  arXiv  Detail & Related papers  (2023-12-28T20:41:24Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  We provide a framework to encode system specifications and define corresponding certificates. We present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
  arXiv  Detail & Related papers  (2023-09-12T09:37:26Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  This paper aims to improve model-based anomaly detection in CPPS by combining the learned timed automaton with a formal knowledge graph about the system. Both the model and the detected anomalies are described in the knowledge graph in order to allow operators an easier interpretation of the model and the detected anomalies.
  arXiv  Detail & Related papers  (2023-08-25T15:25:57Z)
• SoK: Realistic Adversarial Attacks and Defenses for Intelligent Network Intrusion Detection [0.0]
  This paper consolidates and summarizes the state-of-the-art adversarial learning approaches that can generate realistic examples. It defines the fundamental properties that are required for an adversarial example to be realistic. It provides guidelines for researchers to ensure that their future experiments are adequate for a real communication network.
  arXiv  Detail & Related papers  (2023-08-13T17:23:36Z)
• A Security Verification Framework of Cryptographic Protocols Using Machine Learning [0.0]
  We propose a security verification framework for cryptographic protocols using machine learning. We create arbitrarily large datasets by automatically generating random protocols and assigning security labels to them. We evaluate the proposed method by applying it to verification of practical cryptographic protocols.
  arXiv  Detail & Related papers  (2023-04-26T02:37:43Z)
• CC-Cert: A Probabilistic Approach to Certify General Robustness of Neural Networks [58.29502185344086]
  In safety-critical machine learning applications, it is crucial to defend models against adversarial attacks. It is important to provide provable guarantees for deep learning models against semantically meaningful input transformations. We propose a new universal probabilistic certification approach based on Chernoff-Cramer bounds.
  arXiv  Detail & Related papers  (2021-09-22T12:46:04Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.