Model-Driven Engineering for Formal Veriﬁcation and Security Testing of Authentication Protocols Mariapia Raimondo

2025-05-06 0 0 208.8KB 4 页 10玖币

侵权投诉

Model-Driven Engineering for Formal Veriﬁcation

and Security Testing of Authentication Protocols

Mariapia Raimondo

Dip. di Matematica e Fisica

Universit`

a della Campania “L. Vanvitelli”

Caserta, Italy

mariapia.raimondo@unicampania.it

Stefano Marrone

Dip. di Matematica e Fisica

Universit`

a della Campania “L. Vanvitelli”

Caserta, Italy

stefano.marrone@unicampania.it

Angelo Palladino

Aerospace Business Unit

Kineton srl

Napoli, Italy

angelo.palladino@kineton.it

Abstract—Even if the veriﬁcation 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 Uniﬁed Modeling Lan-

guage (UML) proﬁling 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.

Index Terms—Formal veriﬁcation of security protocols, Model

Driven Engineering, Veriﬁcation and Validation, Railway sig-

nalling, blockchain technology

I. INTRODUCTION

Critical systems are now connected to the Internet due to an

increase in the complexity of their functionalities. This growth

of complexity goes not only in the direction of increasing the

level of automation but also in opening such systems to remote

control. Security becomes a prime factor in such a context: its

lack could lead not only to economic loss or privacy leaks, but

also to damage to people and goods. This is the case of the

railway signalling systems, which is considered in this paper.

Another emerging domain where security plays an impor-

tant role is the one constituted by the emerging Distributed

Ledger Technologies (DLTs) and, despite its relatively recent

adoption, a lack of security in DLT would have a strong

social impact. In fact, the blockchain technology, which is

a particular case of DLT, has received widespread support

and acclamation. It provides an infrastructure to manage

transactions within a community without the need of a trusted

third party that supervises. Sufﬁce to say, cryptocurrencies

are based on blockchain technology and they are one of the

main strategies of long-term investment adopted nowadays.

Moreover, the European Community has started writing down

regulations1to use them and proposals to prevent the usage

of this technology for illicit purposes2.

Formal veriﬁcation can be very useful both to check the cor-

rectness of the behaviour of Industrial Control Systems (ICSs)

and the achievement of the security levels required by the new

technologies such as the blockchain ones. Unlike simulation

and testing, this complementary technique is able to ﬁnd very

speciﬁc conditions that could bring to a security ﬂaw that

has not been considered in security test plans. Furthermore,

formal methods are recommended for certiﬁcation purposes,

especially in critical systems. Nonetheless, it is worth under-

lining that: simulation and testing are still the most effective

methods to demonstrate the presence of a security issue in a

speciﬁc scenario; formal modelling and analysis often require

specialised skilled people, whose effort is devoted to low-level

details error-prone activities. The work presented in this paper

deals with the problem of easing the work of the modeller

and unifying the approach to check security and behavioural

properties. The main objective is to provide a comprehensive

approach, supporting formal analysis and testing, based on

Model-Driven Engineering (MDE) techniques.

The approach presented in the paper is based on a traditional

model-driven process schema with the following elements.

First, a UML Proﬁle able to capture the authentication related

features of the modelled system is deﬁned. Then, a model

transformation is provided to derive a formal notation from

an annotated UML model of the system. Finally, the produced

model is analysed with a set of techniques to verify security

properties by formal analysis and/or to generate test scripts to

support the veriﬁcation. Where possible, the approach involves

the use of existing and assessed solvers and toolchains. More

in particular, the UML Proﬁle is used to enrich behavioural

models with cryptoprimitives and security properties. The

model transformation is used to derive an Alice & Bob (AnB)

model which is then checked over security properties. At

the best of our knowledge, there is no unifying description

framework for the different tools that could be used in the

formal veriﬁcation approach. This work will be also driven by

1https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=CELEX%

3A32022R0858&qid=1656931726550

2https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=CELEX%

3A52021PC0422&qid=1656931726550

arXiv:2210.03020v1 [cs.CR] 6 Oct 2022

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

Model-DrivenEngineeringforFormalVericationandSecurityTestingofAuthenticationProtocolsMariapiaRaimondoDip.diMatematicaeFisicaUniversitadellaCampaniaL.VanvitelliCaserta,Italymariapia.raimondo@unicampania.itStefanoMarroneDip.diMatematicaeFisicaUniversitadellaCampaniaL.VanvitelliCaserta,Italystef...

展开>> 收起<<

Model-Driven Engineering for Formal Veriﬁcation and Security Testing of Authentication Protocols Mariapia Raimondo.pdf

共4页,预览1页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Model-Driven Engineering for Formal Veriﬁcation and Security Testing of Authentication Protocols Mariapia Raimondo

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: