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 条
  • [1] Research on formal security policy model specification and its formal analysis
    Institute of Software, Chinese Academy of Sciences, Beijing 100080, China
    不详
    不详
    Tongxin Xuebao, 2006, 6 (94-101):
  • [2] A formal policy specification language for an 802.11 WLAN with enhanced security network
    Çalikli, HG
    Çaglayan, U
    COMPUTER AND INFORMATION SCIENCES - ISCIS 2005, PROCEEDINGS, 2005, 3733 : 183 - 192
  • [3] Applying practical formal methods to the specification and analysis of security properties
    Heitmeyer, C
    INFORMATION ASSURANCE IN COMPUTER NETWORKS: METHODS, MODELS AND ARCHITECTURES FOR NETWORK SECURITY, PROCEEDINGS, 2001, 2052 : 84 - 89
  • [4] Security requirements specification by formal methods: a research metadata analysis
    Aditya Dev Mishra
    Khurram Mustafa
    Multimedia Tools and Applications, 2024, 83 : 41847 - 41866
  • [5] Security requirements specification by formal methods: a research metadata analysis
    Mishra, Aditya Dev
    Mustafa, Khurram
    MULTIMEDIA TOOLS AND APPLICATIONS, 2023, 83 (14) : 41847 - 41866
  • [6] Formal integrated network security analysis tool: formal query-based network security configuration analysis
    Maity, Soumya
    Bera, P.
    Ghosh, Soumya K.
    Al-Shaer, Ehab
    IET NETWORKS, 2015, 4 (02) : 137 - 147
  • [7] Formal Specification and Validation of Security Policies
    Bourdier, Tony
    Cirstea, Horatiu
    Jaume, Mathieu
    Kirchner, Helene
    FOUNDATIONS AND PRACTICE OF SECURITY, 2011, 6888 : 148 - +
  • [8] Formal Specification and Verification of Security Guidelines
    Zhioua, Zeineb
    Roudier, Yves
    Ameur, Rabea Boulifa
    2017 IEEE 22ND PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING (PRDC 2017), 2017, : 267 - 273
  • [9] Network Time Security Specification Protecting Network-based Time Synchronization
    Sibold, Dieter
    Teichel, Kristof
    2016 EUROPEAN FREQUENCY AND TIME FORUM (EFTF), 2016,
  • [10] Formal analysis of a real-time kernel specification
    Fowler, S
    Wellings, A
    FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, 1996, 1135 : 440 - 458
12345