摘要
给出了应用于不同系统的不变式的概述,分析了彼此之间的关系,进行了分类,并探讨了其未来发展趋势.密码协议的形式化分析日渐引起人们的广泛关注.这导致了不变式生成与描述技术的发展.不变式是对入侵者可知和不可知消息的定义,可用于协议认证和秘密性的证明。
Formal methods for cryptographic protocol analysis has drawn attention in recent years This leads to a development of the generation and specification techniques of invariant Invariantis defined what messages an intruder can and cannot learn and can be used to prove authentication as well as secrecy results, appear to be central This paper introducls an overview of invariant in different systems, analyzes their relationships to each other, develops a simple taxonomy, and discuses some of the implications for future research
出处
《中国科学院研究生院学报》
CAS
CSCD
2002年第1期91-96,共6页
Journal of the Graduate School of the Chinese Academy of Sciences
基金
973资助项目(G19990 35 80 2 )
国家杰出青年科学基金资助项目(6 0 0 2 5 2 0 5)
关键词
协议
形式化分析
不变式
cryptographic protocols, formal analysis,invariant