Protocol Derivation System for the Needham-Schroeder family

被引:2
|
作者
Zhang, Junwei [1 ]
Ma, Jianfeng [1 ]
Yang, Chao [1 ]
机构
[1] Xidian Univ, Sch Comp Sci & Technol, Xian 710071, Shaanxi, Peoples R China
基金
中国国家自然科学基金;
关键词
network security; PDS; Needham-Schroeder family; PCL; AUTHENTICATION; LOGIC;
D O I
10.1002/sec.565
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
A framework consisting of the Protocol Derivation System (PDS) and the Protocol Composition Logic (PCL) has been recently proposed by Datta et al. for the design and analysis of a secure composition of cryptographic protocols. However, the PDS in this proposed framework can only be used for the protocols of the Station-to-Station family, which are signature-based authenticated Diffie-Hellman key exchange protocols. In this paper, the PDS is extended to support key exchange protocols using a trusted third party and an encryption-based authentication such as those in the Needham-Schroeder family. This is achieved by means of adding new components, refinements, and transformations to the PDS. In addition, the PCL is applied to prove the correctness of the derived protocols. Then, the derivation graph of the Needham-Schroeder family is developed by using the extended PDS. Finally, the derivations and proofs of the protocols in the Needham-Schroeder family are shown in this paper. Copyright (c) 2012 John Wiley & Sons, Ltd.
引用
收藏
页码:2687 / 2703
页数:17
相关论文
共 50 条
  • [21] 使用组合协议逻辑PCL验证Amended Needham-Schroeder协议
    刘锋
    李舟军
    周倜
    李梦君
    计算机工程与科学, 2008, (11) : 13 - 15
  • [22] A parameterized analysis of public-key protocols:Needham-Schroeder and Kerberos-5
    Muhammad, Shahabuddin
    Furqan, Zeeshan
    Guha, Ratan K.
    ICON: 2006 IEEE INTERNATIONAL CONFERENCE ON NETWORKS, VOLS 1 AND 2, PROCEEDINGS: NETWORKING -CHALLENGES AND FRONTIERS, 2006, : 294 - +
  • [23] Needham-Schroeder协议的认证测试方法形式化分析
    李廷元
    秦志光
    刘晓东
    张选芳
    计算机工程与应用, 2010, 46 (19) : 100 - 102
  • [24] An Image Based Authentication System-Using Needham Schroeder Protocol
    Kumar, Raman
    Puri, Asmita
    Gautam, Vivek
    Singla, Saumya
    INTERNATIONAL JOURNAL OF COMPUTER SCIENCE AND NETWORK SECURITY, 2010, 10 (11): : 135 - 140
  • [25] 基于事件逻辑的改进Needham-Schroeder协议安全性证明
    刘欣倩
    肖美华
    程道雷
    梅映天
    李伟
    计算机工程与科学, 2015, 37 (10) : 1850 - 1855
  • [26] A computational analysis of the Needham-Schroeder-(Lowe) protocol
    Warinschi, B
    16TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2003, : 248 - 262
  • [27] A computational analysis of the Needham-Schroeder-(Lowe) protocol
    Warinschi, Bogdan
    JOURNAL OF COMPUTER SECURITY, 2005, 13 (03) : 565 - 591
  • [28] Safe simplifying transformations for security protocols or not just the needham schroeder public key protocol
    Hui, ML
    Lowe, G
    PROCEEDINGS OF THE 12TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, 1999, : 32 - 43
  • [29] Safe simplifying transformations for security protocols or not just the Needham Schroeder public key protocol
    Univ of Leicester, Leicester, United Kingdom
    Proc Comput Secur Found Workshop, (32-43):
  • [30] A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol
    Backes, M
    Pfitzmann, B
    FST TCS 2003: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, 2003, 2914 : 1 - 12