Part of the EPSRC-funded Communications Hub for Empowering Distributed Cloud Computing Applications and Research (CHEDDAR) project, Pillar 3 is about human-centric design with trust, security, privacy, resilience, interpretability, transparency, and equitability. In project 3.2, Dr Kangfeng Ye is investigating the formal verification challenges for security protocols used for future 6G and developing corresponding approaches to address these issues.

Research challenges:

  • Accessibility of formal verification to wide stakeholders
  • Integration of different formal verification techniques and tools for security protocols
  • Integration of symbolic and computational verification of security protocols
  • Security across different domains: physical, network, users, application, or service-based etc.
  • Diverse network infrastructures (physical layer security, sensor networks, O-RAN, Cellular network, …) requires flexible attack models.
  • Trustworthy AI/ML components (safeguard AI), AI targeted attacks etc.

Objectives

1. The development of accessible formal verification techniques (sound animation) for security protocols

Sound Animation

2. Integration of different formal verification approaches for security protocol using semantics unification and model-based transformation

3. Collaborated with researchers from University of Glasgow and Imperial College London in the Safeguard AI components and quantitative analysis of O-RAN xApps

A scenario of O-RAN xApp

Publications

  • (Paper) User-Guided Verification of Security Protocols via Sound Animation. Accepted by SEFM2024, to appear.

  • (Preprint) Formal Verification as a Key Enabler for AI-Driven Energy Efficiency and Service Availability in O-RAN Networks. Submitted to DataMod2024 and under review.

Codebase

  • RandallYe/Animation_of_Security_Protocols (GitHub): the repository for the SEFM2024 paper “User-Guided Verification of Security Protocols via Sound Animation”, containing the verification/animation of two basic security protocols: the Needham-Schroeder public key protocol and Diffie–Hellman key exchange protocol.