| 安全协议的形式化需求及验证 |
| |
| 引用本文： | 刘怡文,李伟琴. 安全协议的形式化需求及验证[J]. 计算机工程与应用, 2002, 38(17): 125-128 |
| |
| 作者姓名： | 刘怡文 李伟琴 |
| |
| 作者单位： | 北京航空航天大学,北京,100083 |
| |
| 摘 要： | 该文采用近世代数和时序逻辑的方法提出并描述了密码协议的形式化安全需求,并在AT模型的基础上加入信任和知识的非单调逻辑,建立了安全协议的计算模型。利用该计算模型对Denning_Sacco公钥协议进行了验证,发现了对此协议的重放攻击,并对协议进行了修改。
|
| 关 键 词： | BAN逻辑 模型检查 NRL FDR SMV 定理证明 |
| 文章编号： | 1002-8331-(2002)17-0125-04 |
| 修稿时间： | 2001-06-01 |
Formal Requirements and Verification for Security Protocols |
| |
| Liu Yiwen Li Weiqin. Formal Requirements and Verification for Security Protocols[J]. Computer Engineering and Applications, 2002, 38(17): 125-128 |
| |
| Authors: | Liu Yiwen Li Weiqin |
| |
| Abstract: | Using temporal logic and algebra,This paper illustrates the formal requirements for security protocols.By adding non-monotonic logic of belief and knowledge to the Abadi_Tuttle model of computation,the paper present s a model of computation for security protocols.Using this model,it verifies the well known Denning_Sacco Public-Key pro-tocol,discovers the replay attack upon the protocol,and adapt s it. |
| |
| Keywords: | BAN logic model checker NRL FDR SMV theorem prover |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
