论文部分内容阅读
安全协议是网络安全中重要的组成部分，其安全性质（如保密性、数据完整性）直接影响着网络数据交换能否顺利进行。对安全协议常使用形式化分析方法进行研究。在形式化分析时需要对安全协议建立模型，并确定模型的基本假设（包括诚实主体能力、攻击者能力等）。以往对安全协议研究时通常假设密码算法是完美的，即主体的长期私钥不会被泄露(Dolev-Yao模型)。然而在真实的网络环境中，攻击者可能获取主体的长期私钥，而且随着计算能力的提高，密码算法也能够被破解。当协议主体中有某一方的长期私钥被攻击者获取时，攻击者不仅能伪装成该主体欺骗其他主体，也可以伪装成其他主体欺骗被获取长期密钥的该主体，这样的攻击被称为Actor Key Compromise(AKC)攻击，被攻击的主体称为actor。除密钥交换、密钥建立协议外，对AKC攻击的研究在协议研究领域中较少受到关注。本文则强调了AKC攻击问题的重要性，并发现了很多在Dolev-Yao模型下验证为安全，但在AKC攻击模型下无法满足安全性质的协议。通过大量实验，本文总结出4类AKC攻击模式。这4类模式有一部分与Dolev-Yao模型下攻击模式相似，但区别在于4类AKC攻击模式都是在利用主体长期私钥的前提下，对消息进行篡改转发达到攻击目的。如果能对这4类AKC攻击提出解决方案，则可以避免大部分AKC攻击。因此针对这4类AKC攻击模式，本文给出了4类AKCS(Actor KeyCompromise Security，在AKC攻击下保持协议安全性质)协议转换模型和3个协议设计原则。这些模型具备理论上的正确性，本文以定理形式呈现并给出了证明。在上述模型基础上，本文给出了将一般协议转换为AKCS协议的启发式算法。在实例分析中，将算法应用在电子商务、邮件、Windows局域网协议等协议中。本文使用Scyther工具对转换后的协议进行验证。实验表明，上述协议受AKC攻击，在算法转换后，协议不再受AKC攻击影响。