| 基于同态的安全协议攻击及其形式化验证 |
| |
| 引用本文： | 韩继红,周志勇,郭渊博,王亚弟.基于同态的安全协议攻击及其形式化验证[J].计算机工程,2009,35(7):144-146. |
| |
| 作者姓名： | 韩继红 周志勇 郭渊博 王亚弟 |
| |
| 作者单位： | 解放军信息工程大学电子技术学院,郑州,450004 |
| |
| 基金项目： | 国家自然科学基金，国家高技术研究发展计划(863计划) |
| |
| 摘 要： | 介绍2种利用加密算法同态特性的安全协议攻击，定义安全协议项代数表示和基于角色行为序列的协议模型，提出一种基于角色行为实例交互的安全协议约束序列生成方法，应用等式理论将Dolev D等人提出的Dolev-Yao模型（IEEE Transactions on Information Theory，1983，第12期）进行扩展，设计攻击者一阶逻辑演绎系统，采用约束求解方法对NSL协议进行建模和形式化验证，发现基于“完美密码系统假设”无法验证的同态攻击。
|
| 关 键 词： | 安全协议 攻击 同态 等式理论 |
| 修稿时间： | |
Attack on Security Protocol Based on Homomorphism and Its Formal Verification |
| |
| HAN Ji-hong,ZHOU Zhi-yong,GUO Yuan-bo,WANG Ya-di.Attack on Security Protocol Based on Homomorphism and Its Formal Verification[J].Computer Engineering,2009,35(7):144-146. |
| |
| Authors: | HAN Ji-hong ZHOU Zhi-yong GUO Yuan-bo WANG Ya-di |
| |
| Affiliation: | Institute of Electronic Technique;PLA Information Engineering University;Zhengzhou 450004 |
| |
| Abstract: | This paper introduces two attacks on security protocols which have cipher homomorphism, defines term representation and security protocol model based on role's action sequences, proposes a method of transforming role instances interleaving to sequence of constraints, extends the Dolev-Yao intruder model with equational theory, putforwards a intruder deduction system in first-order logic, models and verifies NSL protocol using constraint solving method, discovers the attack based on cipher homomorphism which... |
| |
| Keywords: | security protocol attack homomorphism equational theory |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程》浏览原始摘要信息 |
|
点击此处可从《计算机工程》下载全文 |
