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 条
  • [1] Protocol Derivation System for the Needham-Schroeder Family
    Zhang, Junwei
    Yang, Chao
    Ma, Jianfeng
    2011 6TH INTERNATIONAL ICST CONFERENCE ON COMMUNICATIONS AND NETWORKING IN CHINA (CHINACOM), 2011, : 836 - 840
  • [2] Formal analysis of Needham-Schroeder protocol
    Wang, Gui-Lin
    Qing, Si-Han
    Zhou, Zhan-Fei
    Ruan Jian Xue Bao/Journal of Software, 2002, 13 (SUPPL.): : 86 - 92
  • [3] Needham-Schroeder goes to court
    Denning, DE
    COMPUTER SYSTEMS: THEORY, TECHNOLOGY AND APPLICATIONS: A TRIBUTE TO ROGER NEEDHAM, 2004, : 77 - 78
  • [4] Model Checking of Needham-Schroeder Protocol Using UPPAAL
    Rong, Mei
    Li, Zhonghui
    Zhang, Guangquan
    2010 6TH INTERNATIONAL CONFERENCE ON WIRELESS COMMUNICATIONS NETWORKING AND MOBILE COMPUTING (WICOM), 2010,
  • [5] AN ATTACK ON THE NEEDHAM-SCHROEDER PUBLIC-KEY AUTHENTICATION PROTOCOL
    LOWE, G
    INFORMATION PROCESSING LETTERS, 1995, 56 (03) : 131 - 133
  • [6] Using backward strategy to the Needham-Schroeder public key protocol verification
    Kurkowski, M
    Mackow, M
    ARTIFICIAL INTELLIGENCE AND SECURITY IN COMPUTING SYSTEMS, 2003, 752 : 249 - 259
  • [7] Proving Authentication Property of Modified Needham-Schroeder Protocol with Logic of Events
    Xiao, M. H.
    Deng, C. Y.
    Ma, C. L.
    Zhu, K.
    Cheng, D. L.
    PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON COMPUTER INFORMATION SYSTEMS AND INDUSTRIAL APPLICATIONS (CISIA 2015), 2015, 18 : 379 - 383
  • [8] Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol by Rewriting
    Nesi, Monica
    Rucci, Giuseppina
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 135 (01) : 95 - 114
  • [9] Model checking analysis of needham-schroeder public-key protocol
    Zhang, Yu-Qing
    Wang, Lei
    Xiao, Guo-Zhen
    Wu, Jian-Ping
    Ruan Jian Xue Bao/Journal of Software, 2000, 11 (10): : 1348 - 1352
  • [10] Improvement and security analysis on symmetric key authentication protocol Needham-Schroeder
    Liu, Simin
    Ye, Junyao
    Wang, Yinglian
    APPLIED SCIENCE, MATERIALS SCIENCE AND INFORMATION TECHNOLOGIES IN INDUSTRY, 2014, 513-517 : 1289 - 1293