Hierarchy Requirements and Verification for Cryptographic Protocols
-
摘要: 将密码协议的安全需求分为浅层需求和深层需求2个层面,阐述了密码协议的分层安全需求.采用近世代数和时序逻辑的方法定义了形式化描述语言,并形式化地描述了密码协议的分层安全需求.将类BAN逻辑与模型检查相结合,在Abadi-Tuttle模型的基础上建立密码协议的计算模型.以Otway-Rees协议为例,利用该计算模型和定理证明技术对密码协议进行了多层需求验证.Abstract: The security requirements for cryptographic protocols were divided into shallow requirements and deep requirements. The hierarchy security requirements were illustrated. Using temporal logic and algebra, a formal requirement language was presented and used to describe the formal hierarchy requirements for cryptographic protocols. A model of computation was developed by modifying and extending the Abadi and Tuttle model, combining BAN logic and the NRL Protocol Analyzer. Using this model and theorem proving techniques, the formal requirements of the Otway-Rees protocol was verified.
-
Key words:
- logic algebra /
- formal languages /
- theorem proving /
- model checking
-
[1] Roscoe A W. Intensional specifications of security protocols . In:Guttman J, ed. Proceedings of 9th IEEE Computer Security Foundations Workshop . Los Alamitos:IEEE Computer Society, 1996. 28~38. [2]Boyd C. Towards extensional goals in authentication protocols .http://dimacs.rutgers.edu/workshops/security/program2/program.html,1997. [3]Paulson L C. The inductive approach to verifying cryptographic protocols[J]. Journal of Computer Security, 1998, 6(1/2):85~128. [4]Abadi M, Tuttle M R. A semantics for logic of authentication . In:Proceedings of the 10th ACM Symposium on Principles of Distributed Computing . New York:ACM Press, 1991. 201~216. [5]Meadows C. A model of computation for the NRL protocol analyzer . In:Gong L, ed. Proceedings of Computer Security Foundations Workshop VII .Los Alamitos:IEEE Computer Society Press, 1994. 84~89. [6]Syverson P F. Adding time to a logic of authentication . In:Sandhu R, ed. Proceedings of the First ACM Conference on Computer and Communications Security . New York:ACM Press, 1993. 97~101. -
点击查看大图
计量
- 文章访问数: 2729
- HTML全文浏览量: 161
- PDF下载量: 904
- 被引次数: 0
下载:
