CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels)

• URL: http://arxiv.org/abs/2310.14658v1
• Date: Mon, 23 Oct 2023 07:53:38 GMT
• Title: CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels)
• Authors: Bruno Blanchet,
• Abstract summary: 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.
• Score: 2.06682776181122
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This document presents the security protocol verifier CryptoVerif.CryptoVerif does not rely on the symbolic, Dolev-Yao model, but on the computational model. It can verify secrecy, correspondence (which include authentication), and indistinguishability properties. It produces proofs presented as sequences of games, like those manually written by cryptographers; these games are formalized in aprobabilistic process calculus. CryptoVerif provides a generic method for specifying security properties of the cryptographic primitives.It produces proofs valid for any number of sessions of the protocol, and provides an upper bound on the probability of success of an attack against the protocol as a function of the probability of breaking each primitive and of the number of sessions. It can work automatically, or the user can guide it with manual proof indications.

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)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [54.27040631527217]
  We propose a novel framework called FoC to Figure out the Cryptographic functions in stripped binaries. FoC-BinLLM outperforms ChatGPT by 14.61% on the ROUGE-L score. FoC-Sim outperforms the previous best methods with a 52% higher Recall@1.
  arXiv  Detail & Related papers  (2024-03-27T09:45:33Z)
• Provably Secure Disambiguating Neural Linguistic Steganography [66.30965740387047]
  The segmentation ambiguity problem, which arises when using language models based on subwords, leads to occasional decoding failures. We propose a novel secure disambiguation method named SyncPool, which effectively addresses the segmentation ambiguity problem. SyncPool does not change the size of the candidate pool or the distribution of tokens and thus is applicable to provably secure language steganography methods.
  arXiv  Detail & Related papers  (2024-03-26T09:25:57Z)
• DT-SIM: Property-Based Testing for MPC Security [2.0308771704846245]
  Property-based testing is effective for detecting security bugs in secure protocols. We specifically target Secure Multi-Party Computation (MPC) We devise a test that can detect various flaws in a bit-level implementation of an MPC protocol.
  arXiv  Detail & Related papers  (2024-03-08T02:02:24Z)
• 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)
• 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)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  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.
  arXiv  Detail & Related papers  (2023-05-20T11:26:51Z)
• 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)
• Revocable Cryptography from Learning with Errors [61.470151825577034]
  We build on the no-cloning principle of quantum mechanics and design cryptographic schemes with key-revocation capabilities. We consider schemes where secret keys are represented as quantum states with the guarantee that, once the secret key is successfully revoked from a user, they no longer have the ability to perform the same functionality as before.
  arXiv  Detail & Related papers  (2023-02-28T18:58:11Z)
• 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)
• 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.