| 改进的加密协议形式化验证模型和算法 |
| |
| 引用本文： | 桑田,黄连生,张磊.改进的加密协议形式化验证模型和算法[J].清华大学学报(自然科学版),2002,42(1):48-51. |
| |
| 作者姓名： | 桑田 黄连生 张磊 |
| |
| 作者单位： | 清华大学,计算机科学与技术系,北京,100084 |
| |
| 基金项目： | 国家自然科学基金资助项目 ( 6 9872 0 19) |
| |
| 摘 要： | 状态搜索技术是分析加密协议安全属性的最流行的形式化验证方法之一 ,Mur是一种常用的能分析一般性协议的模型工具 ,它的原理简明 ,但缺点是容易产生状态爆炸。为了克服这一问题 ,针对加密协议的特点 ,提出了改进模型和算法。根据协议的描述定义状态空间 ,建立以攻击者为核心的验证模型 ,使用搜索算法检测是否存在攻击者能完成攻击的不安全状态。在对通信过程、消息传递方式等方面改进后 ,搜索空间的可达状态数减少了很多 ,验证系统的效率显著提高
|
| 关 键 词： | 状态搜索 形式化验证 加密协议 攻击者 Mur |
| 文章编号： | 1000-0054(2002)01-0048-04 |
| 修稿时间： | 2001年3月20日 |
Improved formal model and algorithm for verifying cryptographic protocols |
| |
| SANG Tian,HUANG Liansheng,ZHANG Lei.Improved formal model and algorithm for verifying cryptographic protocols[J].Journal of Tsinghua University(Science and Technology),2002,42(1):48-51. |
| |
| Authors: | SANG Tian HUANG Liansheng ZHANG Lei |
| |
| Abstract: | |
| |
| Keywords: | state exploration formal verification cryptographic protocols intruder Mur |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
