Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols

• URL: http://arxiv.org/abs/2311.15189v3
• Date: Sun, 10 Nov 2024 03:51:42 GMT
• Title: Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols
• Authors: Nisansala P. Yatapanage, Cliff B. Jones,
• Abstract summary: Rely/guarantee provides a mechanism for abstractly reasoning about the interference from the environment. This paper investigates this approach on the Needham-Schroeder Public Key protocol. It shows that the technique can effectively uncover the assumptions under which the protocol can withstand attacks from intruders.
• Score: 0.0
• License:
• Abstract: The verification of security protocols is essential, in order to ensure the absence of potential attacks. However, verification results are only valid with respect to the assumptions under which the verification was performed. These assumptions are often hidden and are difficult to identify, making it unclear whether a given protocol is safe to deploy into a particular environment. Rely/guarantee provides a mechanism for abstractly reasoning about the interference from the environment. Using this approach, the assumptions are made clear and precise. This paper investigates this approach on the Needham-Schroeder Public Key protocol, showing that the technique can effectively uncover the assumptions under which the protocol can withstand attacks from intruders.

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)
• Structural Vulnerability in Y00 Protocols [0.0]
  This paper critically analyzes the Y00 protocol, a quantum noise-based stream cipher proposed to enhance classical cryptographic methods. We reveal a structural vulnerability that enables the leakage of secret information from measurement outcomes.
  arXiv  Detail & Related papers  (2024-12-10T08:29:44Z)
• 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)
• Device-independent certification of desirable properties with a confidence interval [0.0]
  We provide a versatile solution for rigorous device-independent certification. We show how the PBR protocol and the martingale-based protocol often offer similar performance. Our findings also show that the performance of the martingale-based protocol may be severely affected by one's choice of the witness.
  arXiv  Detail & Related papers  (2024-01-12T15:21:21Z)
• Tamper-Evident Pairing [55.2480439325792]
  Tamper-Evident Pairing (TEP) is an improvement of the Push-Button configuration (PBC) standard. TEP relies on the Tamper-Evident Announcement (TEA), which guarantees that an adversary can neither tamper a transmitted message without being detected, nor hide the fact that the message has been sent. This paper provides a comprehensive overview of the TEP protocol, including all information needed to understand how it works.
  arXiv  Detail & Related papers  (2023-11-24T18:54:00Z)
• Short Paper: Accountable Safety Implies Finality [10.589723476970443]
  Two key desiderata have been studied for Byzantine-fault tolerant (BFT) state-machine replication (SMR) consensus protocols. We show that accountable safety implies finality, thereby unifying earlier results.
  arXiv  Detail & Related papers  (2023-08-31T17:58:38Z)
• Information-Theoretic Safe Exploration with Gaussian Processes [89.31922008981735]
  We consider a sequential decision making task where we are not allowed to evaluate parameters that violate an unknown (safety) constraint. Most current methods rely on a discretization of the domain and cannot be directly extended to the continuous case. We propose an information-theoretic safe exploration criterion that directly exploits the GP posterior to identify the most informative safe parameters to evaluate.
  arXiv  Detail & Related papers  (2022-12-09T15:23:58Z)
• 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)
• Conformal Off-Policy Prediction in Contextual Bandits [54.67508891852636]
  Conformal off-policy prediction can output reliable predictive intervals for the outcome under a new target policy. We provide theoretical finite-sample guarantees without making any additional assumptions beyond the standard contextual bandit setup.
  arXiv  Detail & Related papers  (2022-06-09T10:39:33Z)
• Byzantine-Robust Federated Learning with Optimal Statistical Rates and Privacy Guarantees [123.0401978870009]
  We propose Byzantine-robust federated learning protocols with nearly optimal statistical rates. We benchmark against competing protocols and show the empirical superiority of the proposed protocols. Our protocols with bucketing can be naturally combined with privacy-guaranteeing procedures to introduce security against a semi-honest server.
  arXiv  Detail & Related papers  (2022-05-24T04:03:07Z)

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.