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