Demonstrating the Necessity of Model Generation in Security Protocol Verification
Mariapia Raimondo, S. Marrone, Simona Bernardi, Angelo Palladino · 2023
Even if the verification of authentication protocols can be achieved through formal analysis, the modelling of such an activity is an error-prone task due to the lack of automated and integrated processes. This paper relies on Unified Modeling Language (UML) profiling and model-transformation techniques to enable automatic analysis of authentication protocols starting from high-level models. The original contribution of this paper is a concrete toolchain, based on a modular approach, to support the modelling and analysis of authentication protocols. In particular, we propose three nested Extended Backus-Naur Form (EBNF) grammars for the high-level specification of the protocol and a transformation from the high-level specification into a specific target language, that is Alice & Bob extended (AnBx). The generated AnBx model can be then formally checked with the Open-Source Fixed-Point Model Checker (OFMC) tool. The validity and necessity of the proposed toolchain is demonstrated with a case study taken from the literature.