DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice

• URL: http://arxiv.org/abs/2211.03225v2
• Date: Mon, 11 Mar 2024 18:06:10 GMT
• Title: DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice
• Authors: Vincent Cheval, Steve Kremer, Itsaka Rakotonirina,
• Abstract summary: We contribute both to the theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity. Our procedure is the first to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives.
• Score: 8.735998284944436
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automated verification has become an essential part in the security evaluation of cryptographic protocols. In this context privacy-type properties are often modelled by indistinguishability statements, expressed as behavioural equivalences in a process calculus. In this paper we contribute both to the theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and provide a decision procedure for these equivalences in the case of a bounded number of protocol sessions. Our procedure is the first to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives -- those that can be represented by a subterm convergent destructor rewrite system. We also implemented the procedure in a new tool, DeepSec. We showed through extensive experiments that it is significantly more efficient than other similar tools, while at the same time raises the scope of the protocols that can be analysed.

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)
• Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
  We present a new formalism that combines the ability of object-centric Petri nets to capture one-to-many relations and the one of Petri nets with identifiers to compare and synchronize objects based on their identity. We propose a conformance checking approach for such nets based on an encoding in satisfiability modulo theories (SMT)
  arXiv  Detail & Related papers  (2023-12-13T21:53:32Z)
• Test Case Recommendations with Distributed Representation of Code Syntactic Features [2.225268436173329]
  We propose an automated approach which exploits both structural and semantic properties of source code methods and test cases. The proposed approach initially trains a neural network to transform method-level source code, as well as unit tests, into distributed representations. The model computes cosine similarity between the method's embedding and the previously-embedded training instances.
  arXiv  Detail & Related papers  (2023-10-04T21:42:01Z)
• Object Type Clustering using Markov Directly-Follow Multigraph in Object-Centric Process Mining [2.3351527694849574]
  This paper introduces a new approach to cluster similar case notions based on Markov Directly-Follow Multigraph. A threshold tuning algorithm is also defined to identify sets of different clusters that can be discovered based on different levels of similarity.
  arXiv  Detail & Related papers  (2022-06-22T12:36:46Z)
• Data post-processing for the one-way heterodyne protocol under composable finite-size security [62.997667081978825]
  We study the performance of a practical continuous-variable (CV) quantum key distribution protocol. We focus on the Gaussian-modulated coherent-state protocol with heterodyne detection in a high signal-to-noise ratio regime. This allows us to study the performance for practical implementations of the protocol and optimize the parameters connected to the steps above.
  arXiv  Detail & Related papers  (2022-05-20T12:37:09Z)
• FineDiving: A Fine-grained Dataset for Procedure-aware Action Quality Assessment [93.09267863425492]
  We argue that understanding both high-level semantics and internal temporal structures of actions in competitive sports videos is the key to making predictions accurate and interpretable. We construct a new fine-grained dataset, called FineDiving, developed on diverse diving events with detailed annotations on action procedures.
  arXiv  Detail & Related papers  (2022-04-07T17:59:32Z)
• Benchmarking Deep Models for Salient Object Detection [67.07247772280212]
  We construct a general SALient Object Detection (SALOD) benchmark to conduct a comprehensive comparison among several representative SOD methods. In the above experiments, we find that existing loss functions usually specialized in some metrics but reported inferior results on the others. We propose a novel Edge-Aware (EA) loss that promotes deep networks to learn more discriminative features by integrating both pixel- and image-level supervision signals.
  arXiv  Detail & Related papers  (2022-02-07T03:43:16Z)
• Quantum anonymous veto: A set of new protocols [0.41998444721319217]
  We propose protocols for quantum anonymous veto (QAV) based on different types of quantum resources. The proposed schemes are analyzed for all the requirements of a valid QAV scheme. A trade-off between correctness and robustness of the probabilistic QAV schemes is observed.
  arXiv  Detail & Related papers  (2021-09-13T18:56:09Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
  arXiv  Detail & Related papers  (2021-03-18T20:22:50Z)
• Efficient Conformance Checking using Approximate Alignment Computation with Tandem Repeats [0.03222802562733786]
  Conformance checking aims to find and describe the differences between a process model capturing the expected process behavior and a corresponding event log recording the observed behavior. Alignments are an established technique to compute the distance between a trace in the event log and the closest execution trace of a corresponding process model. We propose a novel approximate technique that uses pre- and post-processing steps to compress the length of a trace and recompute the alignment cost.
  arXiv  Detail & Related papers  (2020-04-02T03:50:32Z)
• Certified Robustness to Label-Flipping Attacks via Randomized Smoothing [105.91827623768724]
  Machine learning algorithms are susceptible to data poisoning attacks. We present a unifying view of randomized smoothing over arbitrary functions. We propose a new strategy for building classifiers that are pointwise-certifiably robust to general data poisoning attacks.
  arXiv  Detail & Related papers  (2020-02-07T21:28:30Z)

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.