| 安全协议形式化分析的不变式生成技术 |
| |
| 引用本文： | 范红,冯登国,郭金庚.安全协议形式化分析的不变式生成技术[J].中国科学院研究生院学报,2002,19(1):91-96. |
| |
| 作者姓名： | 范红 冯登国 郭金庚 |
| |
| 作者单位： | 1. 中国科学院研究生院信息安全国家重点实验室,北京,100039
2. 解放军信息工程大学安全学院计算机系,郑州,450004 |
| |
| 基金项目： | 973资助项目(G19990 35 80 2 )，国家杰出青年科学基金资助项目(6 0 0 2 5 2 0 5) |
| |
| 摘 要： | 给出了应用于不同系统的不变式的概述,分析了彼此之间的关系,进行了分类,并探讨了其未来发展趋势.密码协议的形式化分析日渐引起人们的广泛关注.这导致了不变式生成与描述技术的发展.不变式是对入侵者可知和不可知消息的定义,可用于协议认证和秘密性的证明,从而成为许多协议形式化分析工具和技术的核心
|
| 关 键 词： | 协议 形式化分析 不变式 |
| 修稿时间： | 2001年9月19日 |
Invariant Generation Techniques in Cryptographic Protocol Analysis |
| |
| FAN Hong,FENG Deng Guo GUO Jin Geng.Invariant Generation Techniques in Cryptographic Protocol Analysis[J].Journal of the Graduate School of the Chinese Academy of Sciences,2002,19(1):91-96. |
| |
| Authors: | FAN Hong FENG Deng Guo GUO Jin Geng |
| |
| Institution: | FAN Hong 1 FENG Deng Guo 1GUO Jin Geng 2 |
| |
| Abstract: | 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 |
| |
| Keywords: | cryptographic protocols formal analysis invariant |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
