论文标题
用于正式验证和安全测试身份验证协议的模型驱动工程
Model-Driven Engineering for Formal Verification and Security Testing of Authentication Protocols
论文作者
论文摘要
即使可以通过正式分析来实现身份验证协议的验证，由于缺乏自动化和集成过程，这种活动的建模是容易出错的任务。本文提出了一种基于统一建模语言（UML）分析技术和模型转换的综合方法，以实现从高级模型开始的身份验证协议的自动分析。特别是，一种基于UML的方法能够生成一个注释的通信协议模型，可以从中生成形式符号（例如ANBX，tamarin）。可以通过测试案例生成方法与现有求解器和/或传统的测试技术分析此类模型。由于安全的需求不断增长以及将工业流程和设备连接到虚拟化计算基础设施的必要性，因此研究的工业影响很高。该研究是对两个案例研究进行的：铁路信号系统和基于区块链的应用。
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.
