| 基于环境敏感互模拟的Kerberos协议形式化分析 |
| |
| 引用本文： | 武智广,吕银华,翁惠玉.基于环境敏感互模拟的Kerberos协议形式化分析[J].计算机仿真,2007,24(2):99-102. |
| |
| 作者姓名： | 武智广 吕银华 翁惠玉 |
| |
| 作者单位： | 上海交通大学软件学院,上海,200240;上海交通大学计算机科学与工程系,上海,200040 |
| |
| 摘 要： | 进程演算通常用来研究交互式反应系统,其中的互模拟方法是用来形式化验证系统属性的重要途径.首先扩展了进程演算中的Spi演算,并将其应用于形式化描述网络安全协议--Kerberos协议的安全属性.为了验证该协议所声称的安全属性,引入了Spi演算中环境敏感互模拟的方法,即两个系统与环境发生交互过程中是否互模拟.通过采用该互模拟关系对Kerberos协议两个安全属性--可认证性和保密性--的证明,发现其可认证性是可靠的,而保密性存在一个可能的漏洞.最后,指出了基于互模拟的安全协议形式化验证方法今后值得进一步研究的方向.
|
| 关 键 词： | 进程演算 安全协议 形式化方法 |
| 文章编号： | 1006-9348（2007）02-0099-04 |
| 修稿时间： | 2006-01-152006-03-08 |
Analysis of Kerberos Protocols Based on Environmental Sensitive Bisimulation Method |
| |
| WU Zhi-guang,LU Yin-hua,WENG Hui-yu.Analysis of Kerberos Protocols Based on Environmental Sensitive Bisimulation Method[J].Computer Simulation,2007,24(2):99-102. |
| |
| Authors: | WU Zhi-guang LU Yin-hua WENG Hui-yu |
| |
| Affiliation: | 1. School of Software, Shanghai Jiaotong University, Shanghai 200240, China; 2. Department of Computer Science and Engineering, Shanghai Jiaotong University, Shanghai 200240, China |
| |
| Abstract: | |
| |
| Keywords: | Process calculus Security protocols Formal method |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
