基于SPIN的Andrew Secure RPC协议并行攻击模型检测
|
摘要
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.
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.
引文
[1]Burrows M,Abadi M,Needham R M.A logic of authentication[J].Series A,Mathematical and Physical Sciences,1989,426(1871):233-271
[2]Lowe G.Some new attacks upon security protocols[C]∥CSFW,1996.1996:162-169
[3]周清雷,赵琳,赵东明.基于串空间模型的Andrew RPC协议的分析与验证[J].计算机工程与应用,2007,43(13):153-155Zhou Qing-lei,Zhao Lin,Zhao Dong-ming.Analysis and verification of Andrew RPC protocol based on strand spaces[J].Com-puter Engineering and Applications,2007,43(13):153-155
[4]Holzmann G J.The model checker SPIN[J].IEEE Transactions on software engineering,1997,23(5):279-295
[5]吴昌,肖美华,罗敏,等.安全协议验证模型的高效自动生成[J].计算机工程与应用,2010,46(2):79-82Wu Chang,Xiao Mei-hua,Luo Min,et al.Effective automatic generation of verification model on security protocol[J].Computer Engineering and Applications,2010,46(2):79-82
[6]Maggi P,Sisto R.Using SPIN to verify security properties of cryptographic protocols[M]∥Model Checking Software.Springer Berlin Heidelberg,2002:187-204
[7]Krawczyk U,Sapiecha P.Effective reduction of cryptographic protocols specification for model-checking with Spin[J].Annales UMCS,Informatica,2011,11(3):27-40
[8]Ruys T C,Holzmann G J.Advanced spin tutorial[M]∥Model Checking Software.Springer Berlin Heidelberg,2004:304-305
[9]Dolev D,Yao A C.On the security of public key protocols[J].IEEE Transactions on Information Theory,1983,29(2):198-208
[10]侯刚,周宽久,勇嘉伟,等.模型检测中状态爆炸问题研究综述[J].计算机科学,2013,40(z6):77-86,111Hou Gang,Zhou Kuan-jiu,Yong Jia-wei,et al.Survey of State Explosion Problem in Model Checking[J].Computer Science,2013,40(z6):77-86,111
[11]李兴锋,张新常,杨美红,等.基于SPIN的模块化模型检测方法研究[J].电子与信息学报,2011,33(4):902-907Li Xing-feng,Zhang Xin-chang,Yang Mei-hong,et al.Study on Modularized Model Checking Method Based on SPIN[J].Journal of Electronics&Information Technology,2011,33(4):902-907
[12]Yamada Y,Wasaki K.Automatic generation of SPIN model checking code from UML activity diagram and its application to Web application design[C]∥2011 7th International Conference on Digital Content,Multimedia Technology and its Applications(IDCTA).IEEE,2011:139-144
[2]Lowe G.Some new attacks upon security protocols[C]∥CSFW,1996.1996:162-169
[3]周清雷,赵琳,赵东明.基于串空间模型的Andrew RPC协议的分析与验证[J].计算机工程与应用,2007,43(13):153-155Zhou Qing-lei,Zhao Lin,Zhao Dong-ming.Analysis and verification of Andrew RPC protocol based on strand spaces[J].Com-puter Engineering and Applications,2007,43(13):153-155
[4]Holzmann G J.The model checker SPIN[J].IEEE Transactions on software engineering,1997,23(5):279-295
[5]吴昌,肖美华,罗敏,等.安全协议验证模型的高效自动生成[J].计算机工程与应用,2010,46(2):79-82Wu Chang,Xiao Mei-hua,Luo Min,et al.Effective automatic generation of verification model on security protocol[J].Computer Engineering and Applications,2010,46(2):79-82
[6]Maggi P,Sisto R.Using SPIN to verify security properties of cryptographic protocols[M]∥Model Checking Software.Springer Berlin Heidelberg,2002:187-204
[7]Krawczyk U,Sapiecha P.Effective reduction of cryptographic protocols specification for model-checking with Spin[J].Annales UMCS,Informatica,2011,11(3):27-40
[8]Ruys T C,Holzmann G J.Advanced spin tutorial[M]∥Model Checking Software.Springer Berlin Heidelberg,2004:304-305
[9]Dolev D,Yao A C.On the security of public key protocols[J].IEEE Transactions on Information Theory,1983,29(2):198-208
[10]侯刚,周宽久,勇嘉伟,等.模型检测中状态爆炸问题研究综述[J].计算机科学,2013,40(z6):77-86,111Hou Gang,Zhou Kuan-jiu,Yong Jia-wei,et al.Survey of State Explosion Problem in Model Checking[J].Computer Science,2013,40(z6):77-86,111
[11]李兴锋,张新常,杨美红,等.基于SPIN的模块化模型检测方法研究[J].电子与信息学报,2011,33(4):902-907Li Xing-feng,Zhang Xin-chang,Yang Mei-hong,et al.Study on Modularized Model Checking Method Based on SPIN[J].Journal of Electronics&Information Technology,2011,33(4):902-907
[12]Yamada Y,Wasaki K.Automatic generation of SPIN model checking code from UML activity diagram and its application to Web application design[C]∥2011 7th International Conference on Digital Content,Multimedia Technology and its Applications(IDCTA).IEEE,2011:139-144