Model Checking of Parallel Attack in Andrew Secure RPC Protocol Based on SPIN

Abstract

Abstract: 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.

Key words: Andrew Secure RPC protocol,Model checking,SPIN,Combinatorial identity modeling method,Parallel attacks

XIAO Mei-hua ZHU Ke MA Cheng-lin. Model Checking of Parallel Attack in Andrew Secure RPC Protocol Based on SPIN[J].Computer Science, 2015, 42(7): 103-107.

References

[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-155 Zhou Qing-lei,Zhao Lin,Zhao Dong-ming.Analysis and verification of Andrew RPC protocol based on strand spaces[J].Computer 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-82 Wu 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 ofcryptographic protocols[M]∥Model Checking Software.Springer Berlin Heidelberg,2002:187-204
[7] Krawczyk U,Sapiecha P.Effective reduction of cryptographicprotocols 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,111 Hou 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 modelchecking 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

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

Comments

Recommended 0

No Suggested Reading articles found!