An improved formal model of cryptographic protocol

被引：0
|
作者：
Institute of Electronic Technology, PLA Information Engineering University, Zhengzhou 450004, China [1 ]
机构：
[1] Institute of Electronic Technology, PLA Information Engineering University
来源：
Ruan Jian Xue Bao | 2007年 / 7卷 / 1746-1755期
关键词：
Authentication; Cryptographic protocol; Formal verification; Secrecy;
D O I：
10.1360/jos181746
中图分类号：
学科分类号：
摘要：
MSR (multiset rewriting) model is a technique of protocol modeling based on multiset rewriting. According to the results of the current study, this model is not perfect. Since the intruder model of MSR model is not suitable for the verification of the protocol, it was improved. Using this model, the secrecy and authentication of the cryptographic protocols are described. The practice proves the improvement of the former model.
引用
收藏
页码：1746 / 1755
页数：9
相关论文
共 7 条
  • [1] Ji Q.G., Feng D.G., Towards analyzing some kinds of critically formal models for network security protocols, Chinese Journal of Computers, 28, 7, pp. 1071-1083, (2005)
  • [2] Cervesato I., Durgin N.A., Lincoln P.D., Mitchell J.C., Scedrov A., A meta-notation for protocol analysis, Proc. of the 12th IEEE Computer Security Foundations Workshop-CSFW'99, pp. 55-69, (1999)
  • [3] Cervesato I., A specification language for crypto-protocols based on multiset rewriting, dependent types and subsorting, Proc. of the Workshop on Specification, Analysis and Validation for Emerging Technologies-SAVE'01, pp. 1-22, (2001)
  • [4] Cervesato I., Data access specification and the most powerful symbolic attacker in MSR, Software Security, Theories and Systems, pp. 384-416, (2003)
  • [5] Lowe G., A hierarchy of authentication specifications, Proc. of the 10th IEEE Computer Security Foundations Workshop, pp. 31-43, (1997)
  • [6] Cervesato I., Typed MSR: Syntax and examples, Proc. of the 1st Int'l Workshop on Mathematical Methods, Models and Architectures for Computer Network Security-MMM 2001, pp. 159-176, (2001)
  • [7] Butler F., Cervesato I., Jaggard A., Scedrov A., A formal analysis of some properties of Kerberos 5 using MSR, (2004)
1