Strands Rocq: Why is a Security Protocol Correct, Mechanically?

• URL: http://arxiv.org/abs/2502.12848v1
• Date: Tue, 18 Feb 2025 13:34:58 GMT
• Title: Strands Rocq: Why is a Security Protocol Correct, Mechanically?
• Authors: Matteo Busi, Riccardo Focardi, Flaminia L. Luccio,
• Abstract summary: StrandsRocq is a mechanization of the strand spaces in Coq. It incorporates new original proof techniques and a novel notion of maximal penetrator. It provides a compositional proof of security for two simple authentication protocols.
• Score: 3.6840775431698893
• License:
• Abstract: Strand spaces are a formal framework for symbolic protocol verification that allows for pen-and-paper proofs of security. While extremely insightful, pen-and-paper proofs are error-prone, and it is hard to gain confidence on their correctness. To overcome this problem, we developed StrandsRocq, a full mechanization of the strand spaces in Coq (soon to be renamed Rocq). The mechanization was designed to be faithful to the original pen-and-paper development, and it was engineered to be modular and extensible. StrandsRocq incorporates new original proof techniques, a novel notion of maximal penetrator that enables protocol compositionality, and a set of Coq tactics tailored to the domain, facilitating proof automation and reuse, and simplifying the work of protocol analysts. To demonstrate the versatility of our approach, we modelled and analyzed a family of authentication protocols, drawing inspiration from ISO/IEC 9798-2 two-pass authentication, the classical Needham-Schroeder-Lowe protocol, as well as a recently-proposed static analysis for a key management API. The analyses in StrandsRocq confirmed the high degree of proof reuse, and enabled us to distill the minimal requirements for protocol security. Through mechanization, we identified and addressed several issues in the original proofs and we were able to significantly improve the precision of the static analysis for the key management API. Moreover, we were able to leverage the novel notion of maximal penetrator to provide a compositional proof of security for two simple authentication protocols.

Related papers

• Formal Verification of Permission Voucher [1.4732811715354452]
  The Permission Voucher Protocol is a system designed for secure and authenticated access control in distributed environments. The analysis employs the Tamarin Prover, a state-of-the-art tool for symbolic verification, to evaluate key security properties. Results confirm the protocol's robustness against common attacks such as message tampering, impersonation, and replay.
  arXiv  Detail & Related papers  (2024-12-18T14:11:50Z)
• PriRoAgg: Achieving Robust Model Aggregation with Minimum Privacy Leakage for Federated Learning [49.916365792036636]
  Federated learning (FL) has recently gained significant momentum due to its potential to leverage large-scale distributed user data. The transmitted model updates can potentially leak sensitive user information, and the lack of central control of the local training process leaves the global model susceptible to malicious manipulations on model updates. We develop a general framework PriRoAgg, utilizing Lagrange coded computing and distributed zero-knowledge proof, to execute a wide range of robust aggregation algorithms while satisfying aggregated privacy.
  arXiv  Detail & Related papers  (2024-07-12T03:18:08Z)
• A consolidated and accessible security proof for finite-size decoy-state quantum key distribution [0.0]
  We provide a rigorous and comprehensive security proof for the finite-size 1-decoy and 2-decoy BB84 protocols against coherent attacks. We extensively consolidate and unify concepts from many works, thoroughly discussing the underlying assumptions and resolving technical inconsistencies.
  arXiv  Detail & Related papers  (2024-05-26T14:13:33Z)
• Protocols for Quantum Weak Coin Flipping [0.1499944454332829]
  Weak coin flipping is an important cryptographic primitive. We give exact constructions of related unitary operators. We illustrate the construction of explicit weak coin flipping protocols.
  arXiv  Detail & Related papers  (2024-02-24T16:52:54Z)
• 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)
• Performance-lossless Black-box Model Watermarking [69.22653003059031]
  We propose a branch backdoor-based model watermarking protocol to protect model intellectual property. In addition, we analyze the potential threats to the protocol and provide a secure and feasible watermarking instance for language models.
  arXiv  Detail & Related papers  (2023-12-11T16:14:04Z)
• Practical quantum secure direct communication with squeezed states [55.41644538483948]
  We report the first table-top experimental demonstration of a CV-QSDC system and assess its security. This realization paves the way into future threat-less quantum metropolitan networks, compatible with coexisting advanced wavelength division multiplexing (WDM) systems.
  arXiv  Detail & Related papers  (2023-06-25T19:23:42Z)
• Finite-Size Security for Discrete-Modulated Continuous-Variable Quantum Key Distribution Protocols [4.58733012283457]
  We present a composable finite-size security proof against independently and identically distributed collective attacks for a general DM CV-QKD protocol. We extend and apply a numerical security proof technique to calculate tight lower bounds on the secure key rate. Results show that our security proof method yields secure finitesize key rates under experimentally viable conditions up to at least 72km transmission distance.
  arXiv  Detail & Related papers  (2023-01-20T17:16:21Z)
• Is Vertical Logistic Regression Privacy-Preserving? A Comprehensive Privacy Analysis and Beyond [57.10914865054868]
  We consider vertical logistic regression (VLR) trained with mini-batch descent gradient. We provide a comprehensive and rigorous privacy analysis of VLR in a class of open-source Federated Learning frameworks.
  arXiv  Detail & Related papers  (2022-07-19T05:47:30Z)
• 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)
• Twin-field quantum digital signatures [4.503555294002338]
  Digital signature is a key technique in information security, especially for identity authentications. Quantum digital signatures (QDSs) provide a considerably higher level of security, i.e., information-theoretic security.
  arXiv  Detail & Related papers  (2020-03-25T08:04: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.