CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
- URL: http://arxiv.org/abs/2305.12173v2
- Date: Fri, 5 Apr 2024 14:45:53 GMT
- Title: CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
- Authors: Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson,
- Abstract summary: We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic.
Key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations.
On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness.
- Score: 8.838422697156195
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Cryptographic protocols are hard to design and prove correct, as witnessed by the ever-growing list of attacks even on protocol standards. Symbolic models of cryptography enable automated formal security proofs of such protocols against an idealized model, which abstracts away from the algebraic properties of cryptographic schemes and thus misses attacks. Computational models yield rigorous guarantees but support at present only interactive proofs and/or restricted classes of protocols. A promising approach is given by the computationally complete symbolic attacker (CCSA), formalized in the BC Logic, which aims at bridging and getting the best of the two worlds, obtaining cryptographic guarantees by symbolic analysis. The BC Logic is supported by a recently developed interactive theorem prover, Squirrel, which enables machine-checked interactive security proofs, as opposed to automated ones, thus requiring expert knowledge. We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. The key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. We overcome the burden of interactive proving in higher-order (HO) logic and automatically establish soundness of cryptographic protocols using only FO reasoning. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness. On the practical side, CryptoVampire integrates dedicated proof techniques using FO saturation algorithms and heuristics, which enable leveraging the state-of-the-art Vampire FO theorem prover as the underlying proving engine. Our experimental results show CryptoVampire's effectiveness of as a standalone verifier and in terms of automation support for Squirrel.
Related papers
- The Latency Price of Threshold Cryptosystem in Blockchains [52.359230560289745]
We study the interplay between threshold cryptography and a class of blockchains that use Byzantine-fault tolerant (BFT) consensus protocols.
Existing approaches for threshold cryptosystems introduce a latency overhead of at least one message delay for running the threshold cryptographic protocol.
We propose a mechanism to eliminate this overhead for blockchain-native threshold cryptosystems with tight thresholds.
arXiv Detail & Related papers (2024-07-16T20:53:04Z) - Defending Large Language Models against Jailbreak Attacks via Semantic
Smoothing [107.97160023681184]
Aligned large language models (LLMs) are vulnerable to jailbreaking attacks.
We propose SEMANTICSMOOTH, a smoothing-based defense that aggregates predictions of semantically transformed copies of a given input prompt.
arXiv Detail & Related papers (2024-02-25T20:36:03Z) - A Modular Approach to Unclonable Cryptography [4.336971448707467]
We propose unclonable puncturable obfuscation (UPO) and study its implications for unclonable cryptography.
We present modular (and arguably, simple) constructions of many primitives in unclonable cryptography.
We show that any cryptographic functionality can be copy-protected as long as this functionality satisfies a notion of security.
arXiv Detail & Related papers (2023-11-20T16:22:52Z) - CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels) [2.06682776181122]
This document presents the security protocol verifier CryptoVerif.
It does not rely on the symbolic, Dolev-Yao model, but on the computational model.
It can work automatically, or the user can guide it with manual proof indications.
arXiv Detail & Related papers (2023-10-23T07:53:38Z) - CryptoBap: A Binary Analysis Platform for Cryptographic Protocols [6.514727189942011]
We introduce CryptoBap, a platform to verify weak secrecy and authentication for cryptographic protocols.
We achieve this by first transpiling the binary of protocols into an intermediate representation and then performing a crypto-aware symbolic execution.
We prove the soundness of the proposed approach and used CryptoBap to verify multiple case studies ranging from toy examples to real-world protocols.
arXiv Detail & Related papers (2023-08-28T09:41:45Z) - Perfectly Secure Steganography Using Minimum Entropy Coupling [60.154855689780796]
We show that a steganography procedure is perfectly secure under Cachin 1998's information-theoretic model of steganography.
We also show that, among perfectly secure procedures, a procedure maximizes information throughput if and only if it is induced by a minimum entropy coupling.
arXiv Detail & Related papers (2022-10-24T17:40:07Z) - Cryptography with Certified Deletion [16.354530084834863]
We propose a new, unifying framework that yields an array of cryptographic primitives with certified deletion.
primitives enable a party in possession of a quantum ciphertext to generate a classical certificate that the encrypted plaintext has been information-theoretically deleted.
arXiv Detail & Related papers (2022-07-05T00:48:06Z) - Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
We construct the first fully homomorphic encryption scheme with certified deletion.
Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
arXiv Detail & Related papers (2022-03-03T10:07:32Z) - Post-Quantum VRF and its Applications in Future-Proof Blockchain System [13.386254282693335]
A verifiable random function (VRF) is a powerful pseudo-random function that provides a non-interactively public verifiable proof for the correctness of its output.
We propose a generic compiler to obtain the post-quantum VRF from the simple VRF solution using symmetric-key primitives.
We show potential applications of a quantum-secure VRF, such as quantum-secure decentralized random beacon and lottery-based proof of stake consensus blockchain protocol.
arXiv Detail & Related papers (2021-09-05T07:10:41Z) - Spotting adversarial samples for speaker verification by neural vocoders [102.1486475058963]
We adopt neural vocoders to spot adversarial samples for automatic speaker verification (ASV)
We find that the difference between the ASV scores for the original and re-synthesize audio is a good indicator for discrimination between genuine and adversarial samples.
Our codes will be made open-source for future works to do comparison.
arXiv Detail & Related papers (2021-07-01T08:58:16Z) - Fast End-to-End Speech Recognition via a Non-Autoregressive Model and
Cross-Modal Knowledge Transferring from BERT [72.93855288283059]
We propose a non-autoregressive speech recognition model called LASO (Listen Attentively, and Spell Once)
The model consists of an encoder, a decoder, and a position dependent summarizer (PDS)
arXiv Detail & Related papers (2021-02-15T15:18:59Z)
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.