摘要
Andrew Secure RPC协议具有身份认证和秘钥交换功能,其因简洁明了而被广泛应用于对称密钥加密体系中。模型检测技术具有高度自动化的优点,在协议安全性验证领域得到广泛应用,但模型检测方法只能检测到一轮协议会话中存在的攻击,难以检测到多轮并行会话中存在的并行攻击。针对Andrew Secure RPC协议运行环境中存在的并行性与可能出现的安全隐患,提出了组合身份建模方法。该方法运用著名的SPIN模型检测工具,对Andrew Secure RPC协议进行模型检测,从而得到攻击序列图,成功发现并行反射攻击和类缺陷攻击。上述组合身份建模方法为复杂环境下协议的模型检测提供了新的方向。
Andrew Secure RPC protocol is a kind of protocol with functions of identity authentication and key exchange,which is widely used in symmetric cryptography because of its conciseness.Model checking technology is widely used in verification of protocols due to its high automation,however,there is also a disadvantage in model checking technology that it can only find out attacks in single round of protocol session,which is hard used in multi rounds of protocol session.We proposed a modeling method,called combinatorial identity modeling method,which uses SPIN to verify Andrew Secure RPC protocol in consideration of the parallel environment and potential danger in Andrew Secure RPC protocol.According to the research conclusion,we found out two kinds of attacks which are reflection attack and type flaw attack in Andrew Secure RPC protocol.With this conclusion,we offered a new direction in model checking research in verifying protocol under complicated environment.
出处
《计算机科学》
CSCD
北大核心
2015年第7期103-107,共5页
Computer Science
基金
国家自然科学基金(61163005)
计算机软件新技术国家重点实验室开放课题(KFKT2012B18)
江西省高校科技落地计划项目(KJLD13038)
江西省自然科学基金(2010GZS0150
20132BAB201033)资助
