LpiCT: A logic security analysis framework for protocols

• URL: http://arxiv.org/abs/2312.02171v1
• Date: Wed, 1 Nov 2023 12:06:47 GMT
• Title: LpiCT: A logic security analysis framework for protocols
• Authors: Fusheng Wu, Jinhui Liu, Yanbing Li, Mingtao Ni,
• Abstract summary: 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.
• Score: 1.4852249222037588
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The pi calculus is a basic theory of mobile communication based on the notion of interaction, which, aimed at analyzing and modelling the behaviors of communication process in communicating and mobile systems, is widely applied to the security analysis of cryptographic protocol's design and implementation. But the pi calculus does not provide perfect logic security analysis, so the logic flaws in the design and the implementation of a cryptographic protocol can not be discovered in time. The aim is to analyze whether there are logic flaws in the design and the implementation of a cryptographic protocol, so as to ensure the security of the cryptographic protocol when it is encoded into a software and implemented. 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. This paper presents the logic security proof and analysis of TLS1.3 protocol's interactional implementation process. 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. The security of cryptographic protocols depends not only on cryptographic primitives, but also on the coding of cryptographic protocols and the environment in which they are implemented. The security analysis framework of cryptographic protocol implementation proposed in this paper can ensure the security of protocol implementation.

Related papers

• 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 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)
• Secure Synthesis of Distributed Cryptographic Applications (Technical Report) [1.9707603524984119]
  We advocate using secure program partitioning to synthesize cryptographic applications. This approach is promising, but formal results for the security of such compilers are limited in scope. We develop a compiler security proof that handles subtleties essential for robust, efficient applications.
  arXiv  Detail & Related papers  (2024-01-06T02:57:44Z)
• An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
  This approach allows for the computer-assisted analysis of abstract dialectical frameworks. Exemplary applications include the formal analysis and verification of meta-theoretical properties.
  arXiv  Detail & Related papers  (2023-12-08T09:32:26Z)
• SOCI^+: An Enhanced Toolkit for Secure OutsourcedComputation on Integers [50.608828039206365]
  We propose SOCI+ which significantly improves the performance of SOCI. SOCI+ employs a novel (2, 2)-threshold Paillier cryptosystem with fast encryption and decryption as its cryptographic primitive. Compared with SOCI, our experimental evaluation shows that SOCI+ is up to 5.4 times more efficient in computation and 40% less in communication overhead.
  arXiv  Detail & Related papers  (2023-09-27T05:19:32Z)
• 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)
• Evidential Transactions with Cyberlogic [0.6091702876917281]
  Cyberlogic is an enabling logical foundation for building and analyzing digital transactions. Key ideas underlying Cyberlogic are extremely simple, as (1) public keys correspond to authorizations, (2) transactions are specified as distributed logic programs, and (3) verifiable evidence is collected by means of distributed proof search.
  arXiv  Detail & Related papers  (2023-03-20T10:18:43Z)
• Neuro-Symbolic Causal Reasoning Meets Signaling Game for Emergent Semantic Communications [71.63189900803623]
  A novel emergent SC system framework is proposed and is composed of a signaling game for emergent language design and a neuro-symbolic (NeSy) artificial intelligence (AI) approach for causal reasoning. The ESC system is designed to enhance the novel metrics of semantic information, reliability, distortion and similarity.
  arXiv  Detail & Related papers  (2022-10-21T15:33:37Z)
• Towards Semantic Communication Protocols: A Probabilistic Logic Perspective [69.68769942563812]
  We propose a semantic protocol model (SPM) constructed by transforming an NPM into an interpretable symbolic graph written in the probabilistic logic programming language (ProbLog) By leveraging its interpretability and memory-efficiency, we demonstrate several applications such as SPM reconfiguration for collision-avoidance.
  arXiv  Detail & Related papers  (2022-07-08T14:19:36Z)
• Logical blocks for fault-tolerant topological quantum computation [55.41644538483948]
  We present a framework for universal fault-tolerant logic motivated by the need for platform-independent logical gate definitions. We explore novel schemes for universal logic that improve resource overheads. Motivated by the favorable logical error rates for boundaryless computation, we introduce a novel computational scheme.
  arXiv  Detail & Related papers  (2021-12-22T19:00:03Z)
• Security analysis method for practical quantum key distribution with arbitrary encoding schemes [7.321809883860193]
  We propose a security analysis method without restriction on encoding schemes. We illustrate its ability by analyzing source flaws and a high-dimensional asymmetric protocol. Our work has the potential to become a reference standard for the security analysis of practical QKD.
  arXiv  Detail & Related papers  (2021-09-10T09:53:33Z)

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.