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 条
  • [41] FORMAL SPECIFICATION OF REAL-TIME SYSTEMS
    GORSKI, J
    COMPUTER PHYSICS COMMUNICATIONS, 1988, 50 (1-2) : 71 - 88
  • [42] Real time formal specification using VDM(++)
    vanKatwijk, J
    Durr, E
    Goldsack, S
    SECOND WORKSHOP ON OBJECT-ORIENTED REAL-TIME DEPENDABLE SYSTEMS, PROCEEDINGS OF WORDS '96, 1996, : 17 - 24
  • [43] A Formal Security Framework for Mobile Agent Systems: Specification and Verification
    Loulou, Monia
    Kacem, Ahmed Hadj
    Mosbah, Mohamed
    Jmaiel, Mohamed
    CRISIS: 2008 THIRD INTERNATIONAL CONFERENCE ON RISKS AND SECURITY OF INTERNET AND SYSTEMS, PROCEEDINGS, 2008, : 69 - 76
  • [44] Formal specification and analysis of distributed systems
    Pranevicius, H
    JOURNAL OF INTELLIGENT MANUFACTURING, 1998, 9 (06) : 559 - 569
  • [45] Formal specification and analysis of production systems
    Bos, V
    Kleijn, JJT
    INTERNATIONAL JOURNAL OF PRODUCTION RESEARCH, 2002, 40 (15) : 3879 - 3894
  • [46] Formal specification and analysis of distributed systems
    HENRIKAS PRANEVICIUS
    Journal of Intelligent Manufacturing, 1998, 9 : 559 - 569
  • [47] Formal specification and analysis of distributed systems
    Kaunas University of Technology, Studentu 50, Kaunas LT-3028, Lithuania
    J Intell Manuf, 6 (559-569):
  • [48] Formal Specification and Analysis of Spacecraft Collision Avoidance Run Time Assurance Requirements
    Hobbs, Kerianne L.
    Davis, Jennifer
    Wagner, Lucas
    Feron, Eric
    2021 IEEE AEROSPACE CONFERENCE (AEROCONF 2021), 2021,
  • [49] AN APPROACH TO FORMAL SPECIFICATION AND ANALYSIS FOR TIME PERFORMANCE OF THE CONCURRENT REAL-TIME SYSTEM (RTEXS)
    YAO, Y
    COMPUTERS IN INDUSTRY, 1989, 12 (04) : 347 - 354
  • [50] Network Security : Formal and Optimized Configuration
    Fall, Marfall N.
    Mejri, Mohamed
    NEW TRENDS IN SOFTWARE METHODOLOGIES, TOOLS AND TECHNIQUES, 2010, 217 : 229 - 246
12345