Cryptis: Cryptographic Reasoning in Separation Logic

• URL: http://arxiv.org/abs/2502.21156v1
• Date: Fri, 28 Feb 2025 15:33:37 GMT
• Title: Cryptis: Cryptographic Reasoning in Separation Logic
• Authors: Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi,
• Abstract summary: We introduce Cryptis, an extension of the Iris separation logic that can be used to verify cryptographic components using the symbolic model of cryptography.<n>The combination of separation logic and cryptographic reasoning allows us to prove the correctness of a protocol and later reuse this result to verify larger systems that rely on the protocol.
• Score: 6.965792280784777
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce Cryptis, an extension of the Iris separation logic that can be used to verify cryptographic components using the symbolic model of cryptography. The combination of separation logic and cryptographic reasoning allows us to prove the correctness of a protocol and later reuse this result to verify larger systems that rely on the protocol. To make this integration possible, we propose novel specifications for authentication protocols that allow agents in a network to agree on the use of system resources. We evaluate our approach by verifying various authentication protocols and a key-value store server that uses these authentication protocols to connect to clients. Our results are formalized in Coq.

Related papers

• Thetacrypt: A Distributed Service for Threshold Cryptography [0.0]
  Thetacrypt is a versatile library for integrating many threshold schemes into one language.<n>It offers a way to easily build distributed systems using threshold cryptography and is agnostic to their implementation.<n>The library currently includes six cryptographic schemes that span ciphers, signatures, and randomness generation.
  arXiv  Detail & Related papers  (2025-02-05T15:03:59Z)
• 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.<n>These algorithms can be readily applied in an audit setting to evaluate the robustness of a cryptosystem.<n>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)
• Secure Semantic Communication With Homomorphic Encryption [52.5344514499035]
  This paper explores the feasibility of applying homomorphic encryption to SemCom.<n>We propose a task-oriented SemCom scheme secured through homomorphic encryption.
  arXiv  Detail & Related papers  (2025-01-17T13:26:14Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  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.
  arXiv  Detail & Related papers  (2024-11-20T14:16:55Z)
• 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)
• Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
  SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems.
  arXiv  Detail & Related papers  (2024-05-09T19:57:59Z)
• 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)
• LpiCT: A logic security analysis framework for protocols [1.4852249222037588]
  This paper introduces logic rules and proofs, binary tree and the KMP algorithm, and proposes a new extension the pi calculus theory, a logic security analysis framework and an algorithm. Empirical results show that the new extension theory, the logic security analysis framework and the algorithm can effectively analyze whether there are logic flaws in the design and the implementation of a cryptographic protocol.
  arXiv  Detail & Related papers  (2023-11-01T12:06:47Z)
• Revocable Anonymous Credentials from Attribute-Based Encryption [0.0]
  We introduce a credential verification protocol leveraging on Ciphertext-Policy Attribute-Based Encryption.<n>The protocol supports anonymous proof of predicates and revocation through accumulators.
  arXiv  Detail & Related papers  (2023-08-13T15:45:23Z)
• 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)
• Secure access system using signature verification over tablet PC [62.21072852729544]
  We describe a highly versatile and scalable prototype for Web-based secure access using signature verification. The proposed architecture can be easily extended to work with different kinds of sensors and large-scale databases.
  arXiv  Detail & Related papers  (2023-01-11T11:05:47Z)

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.