First Results of a Formal Analysis of the Network Time Security Specification

被引：5

作者：

Teichel, Kristof ^{[1
]}

Sibold, Dieter ^{[1
]}

Milius, Stefan ^{[2
]}

机构：

[1] Phys Tech Bundesanstalt, Bundesallee 100, D-38116 Braunschweig, Germany

[2] Univ Erlangen Nurnberg, Theoret Comp Sci, D-91058 Erlangen, Germany

来源：

SECURITY STANDARDISATION RESEARCH, SSR 2015 | 2015年 / 9497卷

关键词：

Time synchronization; Security protocols; Formal verification; Model checking; ProVerif;

D O I：

10.1007/978-3-319-27152-1_12

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

This paper presents a first formal analysis of parts of a draft version of the Network Time Security specification. It presents the protocol model on which we based our analysis, discusses the decision for using the model checker ProVerif and describes how it is applied to analyze the protocol model. The analysis uncovers two possible attacks on the protocol. We present those attacks and show measures that can be taken in order to mitigate them and that have meanwhile been incorporated in the current draft specification.

引用

页码：218 / 245

页数：28

共 50 条

[21] A review on security requirements specification by formal methods
Mishra, Aditya Dev
Mustafa, Khurram
CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2022, 34 (05):
[22] Towards formal specification of abstract security properties
Mana, Antonio
Pujol, Gimena
ARES 2008: PROCEEDINGS OF THE THIRD INTERNATIONAL CONFERENCE ON AVAILABILITY, SECURITY AND RELIABILITY, 2008, : 80 - +
[23] Formal Analysis for Network Security Properties on a Trace Semantics
Jiang, Yun
Liu, Xifa
2008 INTERNATIONAL CONFERENCE ON ADVANCED COMPUTER THEORY AND ENGINEERING, 2008, : 957 - +
[24] A formal model for network-wide security analysis
Matousek, Petr
Rab, Jaroslav
Rysavy, Ondrej
Sveda, Miroslav
FIFTEENTH IEEE INTERNATIONAL CONFERENCE AND WORKSHOPS ON THE ENGINEERING OF COMPUTER-BASED SYSTEMS, PROCEEDINGS, 2008, : 171 - 181
[25] FORMAL SPECIFICATION AND DESIGN TIME TESTING
GERRARD, CP
COLEMAN, D
GALLIMORE, RM
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1990, 16 (01) : 1 - 12
[26] Safety analysis in formal specification
Sere, K
Troubitsyna, E
FM'99-FORMAL METHODS, VOL II, 1999, 1709 : 1564 - 1583
[27] Formal Specification and Analysis of Firewalls
Mejri, M.
Adi, K.
Fujita, H.
NEW TRENDS IN SOFTWARE METHODOLOGIES, TOOLS AND TECHNIQUES, 2009, 199 : 284 - 293
[28] Hazard analysis in formal specification
Sere, K
Troubitsyna, E
COMPUTER SAFETY, RELIABILITY AND SECURITY, 1999, 1698 : 350 - 360
[29] A Formal Specification and Verification Framework for Timed Security Protocols
Li, Li
Sun, Jun
Liu, Yang
Sun, Meng
Dong, Jin-Song
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2018, 44 (08) : 725 - 746
[30] A Formal Methods Approach to Security Requirements Specification and Verification
Rouland, Quentin
Hamid, Brahim
Bodeveix, Jean-Paul
Filali, Mamoun
2019 24TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2019), 2019, : 236 - 241

← 1 2 3 4 5 →