基于同态的安全协议攻击及其形式化验证

摘要：

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

关键词：安全协议、攻击、同态、等式理论

所属期刊栏目：35

分类号：TP3;TN9

资助基金：国家自然科学基金资助项目60503012;国家"863"计划基金资助项目2007AA01Z405

在线出版日期：2009-05-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：144-146,165