高级搜索

留言板

尊敬的读者、作者、审稿人, 关于本刊的投稿、审稿、编辑和出版的任何问题, 您可以本页添加留言。我们将尽快给您答复。谢谢您的支持!

姓名
邮箱
手机号码
标题
留言内容
验证码

安全协议的形式化规范

胡成军 郑援 吕述望 沈昌祥

胡成军, 郑援, 吕述望, 沈昌祥. 安全协议的形式化规范[J]. 电子与信息学报, 2004, 26(4): 556-561.
引用本文: 胡成军, 郑援, 吕述望, 沈昌祥. 安全协议的形式化规范[J]. 电子与信息学报, 2004, 26(4): 556-561.
Hu Cheng-jun, Zheng Yuan, Lǚ Shu-wang, Shen Chang-xiang. Formal Specification of Security Protocols[J]. Journal of Electronics & Information Technology, 2004, 26(4): 556-561.
Citation: Hu Cheng-jun, Zheng Yuan, Lǚ Shu-wang, Shen Chang-xiang. Formal Specification of Security Protocols[J]. Journal of Electronics & Information Technology, 2004, 26(4): 556-561.

安全协议的形式化规范

Formal Specification of Security Protocols

  • 摘要: 该文给出用PVS(Prototype Verification System)对安全协议进行形式化规范的一种方法。该方法以高阶逻辑为规范语言,利用trace模型来描述协议的行为,并假设系统中存在强攻击者和理想加密系统。重要的结构如消息、事件、协议规则等都通过语义编码方式定义。
  • Needham R M, Schroeder N D. Using encryption for authentication in large network of computers[J].Communications of the ACM.1978, 21(12):993-999[2]Steiner J G, Neuman B C, Schiller J I. Kerberos: an authentication service for open network systems. In Usenix Conference Proceedings, Dallas, Texas, 1988: 191-202.[3]CCITT. CCITT Recommendation X.509, The directory authentication framework, version 7,1987.[4]Owre S, Rushby J, Shankar N, Henke F. Formal verification for fault-tolerant architectures:Prolegomena to the design of PVS. IEEE Trans. on Software Engineering, 1995, SE-21(2): 107-125.[5]Paulson L. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 1998, 6(1): 85-128.[6]Millen J.[J].H. Rue. Protocol-independent secrecy. In 2000 IEEE Symposium on Security and Privacy, Oakland California, USA, IEEE Computer Society Press.2000,:-[7]Lowe G. A hierarchy of authentication specifications. In Proc. of The 10th Computer Security Foundations Workshop, Rockport, Massachusetts, USA, IEEE Computer Society Press, 1997:31-43.[8]Burrows M, Abadi M, Needham R. A logic of authentication[J].ACM Trans. on Computer Systems.1990, 8(1):18-36[9]Guttman J D, Thayer F J. Authentication tests. In 2000 IEEE Symposium on Security and Privacy, Oakland, California, USA, IEEE Computer Society Press, 2000: 96-109.[10]Roscoe A W. Modeling and verifying key-exchange protocols using CSP FDR. In Proc. of the 1995 IEEE Computer Security Foundations Workshop IIX, Dromquinna Manor, Kenmare,County Kerry, Ireland, IEEE Computer Society Press, 1995: 98-107.[11]Thayer J, Herzog J, Guttman J. Strand spaces: Why is a security protocol correct? In Proc. of the 1998 Symposium on Security and Privacy, Oakland California, USA, IEEE Computer Society Press, 1998: 160-171.[12]Paulson L. Isabelle: A Generic Theorem Prover. Berlin, New York: Springer, 1994.[13]胡成军,郑援,沈昌祥.密码协议的秘密性证明.计算机学报,2003,26(3):367-372.
  • 加载中
计量
  • 文章访问数:  2120
  • HTML全文浏览量:  130
  • PDF下载量:  487
  • 被引次数: 0
出版历程
  • 收稿日期:  2002-11-28
  • 修回日期:  2003-02-28
  • 刊出日期:  2004-04-19

目录

    /

    返回文章
    返回