1、DY模型是基于安全协议的分层次的思想,先考虑安全协议本身的行为逻辑是否存在缺陷,之后再考虑实现方法是否存在问题。
而在一般的协议分析中我 们在安全协议验证中我们假定攻击者不具备攻破密码算法的能力,在此前提之下DY模型规定攻击者具有的能力(攻击者不被主体协议察觉的情况下窃听到网络的消息,,攻击者不被主体协议察觉的情况下拦截并存储网络中的消息,,攻击者可以伪造消息,攻击者可以发送消息,攻击者可以最为合法的协议参与者参与协议的运行 )。笼统的讲 DY模型下,攻击者具有完全控制整个网络的能力,
DY 模型对攻击者的能力给出了限定,但是没有给出具体的规则,比方说行为的执行顺序,伪造消息的方法,如何成为合法的协议参与主体等,所以在建模中很难精确的实现DY模型,也就是说DY模型在每一种安全分析工具中被体现存在差异性。
Dolev-Yao模型的参考文献:
Backes M, Pfitzmann B. Symmetric encryption in a simulatable Dolev-Yao style cryptographic library[C]// 2004.
Roberto M. Amadio, Witold Charatonik. On Name Generation and Set-Based Analysis in the Dolev-Yao Model[C]// Proceedings of the 13th International Conference on Concurrency Theory. 2002.
Backes M, Backes M, Duermuth M, et al. A cryptographically sound Dolev-Yao style security proof of the Otway-Rees protocol[J]. 2004, 3193(2004):89--108.
2、强安全模型 eCK的概念
eCK强安全模型的概念比较复杂,这里只说名在强安全模型下敌手的攻击能力具有的行为能力。具有长期私钥泄露,向前安全,DY模型,随机数泄露,会话秘钥泄露,状态协泄露等
eCK 强安全模型参考文献:
倪亮, 陈恭亮, 李建华. eCK模型的安全性分析[J]. 山东大学学报(理学版)(7):49-53+70.
赵建杰, 谷大武. eCK模型下可证明安全的双方认证密钥协商协议[J]. 计算机学报(1):49-56.