Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version)

• URL: http://arxiv.org/abs/2508.19430v2
• Date: Thu, 28 Aug 2025 08:14:44 GMT
• Title: Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version)
• Authors: Kangfeng Ye, Roberto Metere, Jim Woodcock, Poonam Yadav,
• Abstract summary: We re-model the Needham-Schroeder protocol using an Isabelle formalism that generates sound animation.<n>Our findings reveal an uncommon but expected outcome: authenticity is preserved across all examined scenarios.<n>We have proposed a PLS-based Diffie-Hellman protocol that integrates watermarking and jamming.
• Score: 1.5997757408973357
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification is crucial for ensuring the robustness of security protocols against adversarial attacks. The Needham-Schroeder protocol, a foundational authentication mechanism, has been extensively studied, including its integration with Physical Layer Security (PLS) techniques such as watermarking and jamming. Recent research has used ProVerif to verify these mechanisms in terms of secrecy. However, the ProVerif-based approach limits the ability to improve understanding of security beyond verification results. To overcome these limitations, we re-model the same protocol using an Isabelle formalism that generates sound animation, enabling interactive and automated formal verification of security protocols. Our modelling and verification framework is generic and highly configurable, supporting both cryptography and PLS. For the same protocol, we have conducted a comprehensive analysis (secrecy and authenticity in four different eavesdropper locations under both passive and active attacks) using our new web interface. Our findings not only successfully reproduce and reinforce previous results on secrecy but also reveal an uncommon but expected outcome: authenticity is preserved across all examined scenarios, even in cases where secrecy is compromised. We have proposed a PLS-based Diffie-Hellman protocol that integrates watermarking and jamming, and our analysis shows that it is secure for deriving a session key with required authentication. These highlight the advantages of our novel approach, demonstrating its robustness in formally verifying security properties beyond conventional methods.

Related papers

• SLIP-SEC: Formalizing Secure Protocols for Model IP Protection [3.519970512407396]
  Large Language Models (LLMs) represent valuable intellectual property (IP)<n>deploying these models on partially trusted or insecure devices introduces substantial risk of model theft.<n>We present the formal framework and security foundations of SLIP, a hybrid inference protocol that splits computation between a trusted and an untrusted resource.
  arXiv  Detail & Related papers  (2025-10-28T21:59:11Z)
• Deep Learning Models for Robust Facial Liveness Detection [56.08694048252482]
  This study introduces a robust solution through novel deep learning models addressing the deficiencies in contemporary anti-spoofing techniques.<n>By innovatively integrating texture analysis and reflective properties associated with genuine human traits, our models distinguish authentic presence from replicas with remarkable precision.
  arXiv  Detail & Related papers  (2025-08-12T17:19:20Z)
• Design and analysis of a set of discrete variable protocols for secure quantum communication [0.0]
  quantum identity authentication (QIA) protocols have been proposed over the past three decades.<n>This thesis presents two novel QKD protocols that eliminate the need for entanglement or ideal single-photon sources.<n>These protocols are rigorously proven to be secure against various attacks, including intercept-resend and certain collective attacks.
  arXiv  Detail & Related papers  (2025-08-08T15:12:29Z)
• Quantum-Safe Identity Verification using Relativistic Zero-Knowledge Proof Systems [3.8435472626703473]
  Identity verification is essential in sectors like finance, healthcare, and online services to ensure security and prevent fraud.<n>Current password/PIN-based identity solutions are susceptible to phishing or skimming attacks.<n>We explore identity verification through graph coloring-based relativistic zero-knowledge proofs.
  arXiv  Detail & Related papers  (2025-07-18T18:59:19Z)
• Strands Rocq: Why is a Security Protocol Correct, Mechanically? [3.6840775431698893]
  StrandsRocq is a mechanization of the strand spaces in Coq.<n>It incorporates new original proof techniques and a novel notion of maximal penetrator.<n>It provides a compositional proof of security for two simple authentication protocols.
  arXiv  Detail & Related papers  (2025-02-18T13:34:58Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  Large language models (LLMs) are increasingly integrated into real-world personalized applications.<n>The valuable and often proprietary nature of the knowledge bases used in RAG introduces the risk of unauthorized usage by adversaries.<n>Existing methods that can be generalized as watermarking techniques to protect these knowledge bases typically involve poisoning or backdoor attacks.<n>We propose name for harmless' copyright protection of knowledge bases.
  arXiv  Detail & Related papers  (2025-02-10T09:15:56Z)
• 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)
• Formal Verification of Permission Voucher [1.4732811715354452]
  The Permission Voucher Protocol is a system designed for secure and authenticated access control in distributed environments.<n>The analysis employs the Tamarin Prover, a state-of-the-art tool for symbolic verification, to evaluate key security properties.<n>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)
• ACRIC: Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
  Recent security incidents in safety-critical industries exposed how the lack of proper message authentication enables attackers to inject malicious commands or alter system behavior.<n>These shortcomings have prompted new regulations that emphasize the pressing need to strengthen cybersecurity.<n>We introduce ACRIC, a message authentication solution to secure legacy industrial communications.
  arXiv  Detail & Related papers  (2024-11-21T18:26:05Z)
• Excavating Vulnerabilities Lurking in Multi-Factor Authentication Protocols: A Systematic Security Analysis [2.729532849571912]
  Single-factor authentication (SFA) protocols are often bypassed by side-channel and other attack techniques. To alleviate this problem, multi-factor authentication (MFA) protocols have been widely adopted recently.
  arXiv  Detail & Related papers  (2024-07-29T23:37:38Z)
• 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)
• 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)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)

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.