York Researchers Present New Framework for Verifying Physical Layer Security at ICFEM2025

Researchers from the University of York presented their recently published paper, Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks, at the 26th International Conference on Formal Engineering Methods (ICFEM2025) on 11 November 2025.

Background

Physical Layer Security (PLS) is gaining traction as an additional security layer for future communication systems. Unlike traditional cryptographic approaches, PLS secures wireless communication by leveraging the physical characteristics of the wireless channel itself such as noise, interference, fading, and dispersion.

While cryptographic protocols have long benefited from formal verification tools that can identify vulnerabilities and rigorously validate security guarantees, PLS mechanisms have not received the same level of formal analysis. Current PLS verification attempts are either:

• Only accessible to formal methods experts (e.g., the ProVerif-based analysis by Costa et al. — https://doi.org/10.1016/j.cose.2023.103133), or
• User-friendly but incomplete, lacking PLS support (e.g., Ye et al.’s sound animation framework — https://doi.org/10.1007/978-3-031-77382-2).

This creates a clear gap between cryptographic verification tools and PLS prototypes that designers could use.

The work presented at ICFEM2025 addresses this gap by introducing a designer-friendly framework that adds PLS to a sound animation workflow, enabling formal verification of PLS protocols for 6G and beyond.

Research Aim

The paper proposes the first unified, sound framework capable of modelling:

• Watermarking
• Selective jamming
• A PLS-aware attacker model
• The traditional Dolev–Yao attacker

This enables protocol designers without formal methods expertise to verify PLS protocols rigorously.

Research Questions

The study is structured around four key questions:

1. Extensibility:
   Can the framework be extended to model PLS primitives and a PLS-aware attacker?
2. Generality:
   Can both traditional cryptographic and PLS-based protocols be expressed within one unified modelling foundation?
3. Case Studies & Diffie–Hellman:
   What insights emerge from a deeper verification of NSWJ, and can PLS enable a Diffie–Hellman–style authenticated key exchange?
4. Accessibility:
   How can the approach be made more usable (e.g., sound animation, generated tools, browser-based UI)?

Key Contributions

1. A unified mechanised framework supporting sound animation for both cryptographic and PLS-based protocols.
2. A detailed verification study of NSWJ, evaluating secrecy, authenticity, passive vs active attackers, and geometry-dependent eavesdropping.
3. A newly proposed DHWJ protocol, which restores secrecy and achieves authentication using WBPLSec mechanisms.
4. A browser-based, designer-friendly user interface for formal verification without deep modelling expertise.

System Models

Proposed Approach

Intruder Inference Rules

Results

Current Limitations

• Simplified radio model (static geometry, ideal cancellation, no fading/beamforming/mobility).
• Some expert knowledge still required for encoding protocols and selecting properties.
• Performance scaling is slower than specialised crypto-only tools and requires benchmarking on larger topologies.

For full details, please read the complete paper:
👉 https://doi.org/10.1007/978-981-95-4213-0_1

Previous work referenced:

• Costa et al. (Watermark-based PLS model): https://doi.org/10.1016/j.cose.2023.103133
• Ye et al. (Sound animation framework): https://doi.org/10.1007/978-3-031-77382-2