期刊文献+

基于PVS的密码协议形式化规范(英文)

Formal Specification of Cryptographic Protocols Using PVS
下载PDF
导出
摘要 给出用PVS对密码协议进行形式化规范的一种方法.该方法以高阶逻辑为规范语言,利用trace模型来描述协议的行为,并假设系统中存在强攻击者和理想加密系统.重要的结构如消息、事件、协议规则等都通过语义编码方式定义. A specification method using PVS is presented. Higher order logic is chosen as the specification language. Strong spy and ideal encryption are assumed, and trace model is used to define protocols' behaviors. Moreover, useful structures such as message, event, protocol rule, etc. are semantically encoded.
出处 《中国科学院研究生院学报》 CAS CSCD 2002年第3期233-239,共7页 Journal of the Graduate School of the Chinese Academy of Sciences
基金 the 973 project(G1999035801)
关键词 密码协议 形式化规范 PVS 规范语言 规范方法 加密系统 语义编码方式 cryptographic protocol, formal specification, PVS
  • 相关文献

参考文献9

  • 1[1]R M Needham, N D Schroeder. Using Encryption for Authentication in Large Network of Computers. Communications of the ACM,1978,21(12):993~999
  • 2[2]J G Steiner, B C Neuman, J I Schiller. Kerberos: an Authentication Service for Open Network Systems. In: Usenix conference proceedings, Dallas, Texas, February 1988,191~202
  • 3[3]CCITT. CCITT Recommendation X.509. The Directory Authentication Framework, version 7, 1987
  • 4[4]S Owre, J Rushby, N Shankar, F Henke. Formal Verification for Fault-tolerant Architectures. Prolegomena to the design of PVS. IEEE Transactions on Software Engineering,1995,21(2):107~125
  • 5[5]L Paulson. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security, 1998,6(1):85~128
  • 6[6]J Millen, H Rue . Protocol-Indendent Secrecy. In:2000 IEEE Symposium on Security and Privacy. IEEE Computer Society, 2000.110~209
  • 7[7]G Lowe. A Hierarchy of Authentication Specifications. In: Proceedings of The 10th Computer Security Foundations Workshop. IEEE Computer Society Press, 1997
  • 8[8]M Burrows, M Abadi, R Needham. A Logic of Authentication. ACM Transaction on Computer Systems, 1990,8
  • 9[9]J D Guttman, F J Thayer. Authentication Tests. In: 2000 IEEE Symposium on Security and Privacy. IEEE Computer Society, 2000.96~109

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部