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 条

[31] A formal specification in JML of Java']Java security package
Agarwal, Poonam
Rubio-Medrano, Carlos E.
Cheon, Yoonsik
Teller, Patricia. J.
ADVANCES AND INNOVATIONS IN SYSTEMS, COMPUTING SCIENCES AND SOFTWARE ENGINEERING, 2007, : 363 - 368
[32] A formal specification of EPCIS discovery in the RFID network
Li, Xin-Peng
Zhao, Wen
Zhang, Shi-Kun
Wang, Li-Fu
Tien Tzu Hsueh Pao/Acta Electronica Sinica, 2008, 36 (SUPPL.): : 9 - 18
[33] Integrated security analysis framework for an enterprise network - a formal approach
Bera, P.
Ghosh, S. K.
Dasgupta, P.
IET INFORMATION SECURITY, 2010, 4 (04) : 283 - 300
[34] Security policy specification for home network
Kim, Geon Woo
Lee, Deok Gyu
Han, Jong Wook
Kim, Sang Wook
INTERNATIONAL JOURNAL OF AD HOC AND UBIQUITOUS COMPUTING, 2009, 4 (06) : 372 - 378
[35] Real-Time Animation for Formal Specification
Mery, Dominique
Singh, Neeraj Kumar
COMPLEX SYSTEMS DESIGN AND MANAGEMENT, 2010, : 49 - 60
[36] FORMAL SPECIFICATION OF SECURITY REQUIREMENTS USING THE THEORY OF NORMATIVE POSITIONS
JONES, AJI
SERGOT, M
LECTURE NOTES IN COMPUTER SCIENCE, 1992, 648 : 103 - 121
[37] Formal specification and verification of resource bound security using PVS
Yu, WJ
Mok, AK
SOFTWARE SECURITY - THEORIES AND SYSTEMS, 2004, 3233 : 113 - 133
[38] Towards a formal specification method for enterprise information system security
Sengupta, Anirban
Barik, Mridul Sankar
INFORMATION SYSTEMS SECURITY, PROCEEDINGS, 2006, 4332 : 373 - +
[39] Formal specification and management of security policies with collective group obligations
Cuppens, Frederic
Cuppens-Boulahia, Nora
Elrakaiby, Yehia
JOURNAL OF COMPUTER SECURITY, 2013, 21 (01) : 149 - 190
[40] Security Protocol For Distributed Networks using Formal Method Specification
Nandewal, Arun
Mahendra, Deepesh
Chandrasekaran, K.
2016 3RD INTERNATIONAL CONFERENCE ON ADVANCED COMPUTING AND COMMUNICATION SYSTEMS (ICACCS), 2016,

← 1 2 3 4 5 →