Model-Driven Engineering for Formal Verification and Security Testing of Authentication Protocols

TL;DR

This paper presents a UML-based model-driven approach that automates the formal verification and security testing of authentication protocols, facilitating analysis from high-level models to formal notations for industrial applications.

Contribution

It introduces a comprehensive UML profiling and model transformation method enabling automatic analysis of authentication protocols from high-level models to formal verification tools.

Findings

Effective UML-based models can be transformed into formal notations for analysis.

Automated approach reduces errors in modeling authentication protocols.

Applicable to industrial systems like railway signaling and blockchain applications.

Abstract

Even if the verification of authentication protocols can be achieved by means of formal analysis, the modelling of such an activity is an error-prone task due to the lack of automated and integrated processes. This paper proposes a comprehensive approach, based on the Unified Modeling Language (UML) profiling technique and on model-transformation, to enable automatic analysis of authentication protocols starting from high-level models. In particular, a UML-based approach is able to generate an annotated model of communication protocols from which formal notations (e.g., AnBx, Tamarin) can be generated. Such models in lower-level languages can be analysed with existing solvers and/or with traditional testing techniques by means of test case generation approaches. The industrial impact of the research is high due to the growing need of security and the necessity to connect industrial processes and equipment to virtualised computing infrastructures. The research is conducted on two case studies: railway signalling systems and blockchain based applications.