AProVer Front-End Modelling Language for Designing Security Protocols

In the rapidly evolving field of cybersecurity, the design and verification of secure communication protocols are essential to protect data across a wide range of platforms, devices, and networks. To ensure these protocols remain effective and resilient against attacks, it is crucial to strengthen the principle of security by design, and therefore provide protocol designers with a simple and intuitive notation that simplifies both the construction of secure protocols and their translation into input models for verifying key security protocols. This paper presents a comprehensive metamodel for specifying security protocols, serving as the foundation for both a textual (KANT) and a visual notation. The metamodel was designed to offer a clear and unambiguous language for describing the components and behaviours of security protocols, enabling accurate modelling, analysis, and verification. It facilitates seamless transitions between textual and graphical representations, enhancing both clarity and flexibility. This dual-notation language significantly improves usability, accessibility, and in-depth protocol analysis. It serves as the front-end language for AProVer, a comprehensive framework that supports various types of security protocol analysis designed to be user-friendly, bridging the gap between designers’ varying backgrounds and formal notations.