摘要： 介绍2种利用加密算法同态特性的安全协议攻击，定义安全协议项代数表示和基于角色行为序列的协议模型，提出一种基于角色行为实例交互的安全协议约束序列生成方法，应用等式理论将Dolev D等人提出的Dolev-Yao模型(IEEE Transactions on Information Theory, 1983, 第12期)进行扩展，设计攻击者一阶逻辑演绎系统，采用约束求解方法对NSL协议进行建模和形式化验证，发现基于“完美密码系统假设”无法验证的同态攻击。

关键词: 安全协议, 攻击, 同态, 等式理论

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 can not be found under perpect cryptography assumptions.

Key words: security protocol, attack, homomorphism, equational theory

中图分类号: 

• TP393.08