International Journal of Information Technology and Computer Science (IJITCS)
IJITCS Vol. 11, No. 12, 8 Dec. 2019
Cover page and Table of Contents: PDF (size: 668KB)
A Comparative Analysis of Tools for Testing the Security Protocols
Full Text (PDF, 668KB), PP.30-37
Views: 0 Downloads: 0
Author(s)
Index Terms
AVISPA, Authentication protocols, BAN Logic, Handover, Privacy, Wimax
Abstract
In this paper, Analysis and comparison of two popular security verification tools namely Automated Validation of Internet Security Protocols and Applications (AVISPA) and Burrows-Abadi-Needham (BAN) logic are presented in terms of the usability, complexity, and other properties of the selected tools. The comparison shows the benefits and the drawbacks for the two tools. As a case study, two previously proposed security protocols, which were tested before by BAN logic only are evaluated and proved using the automated verification tool AVISPA to ensure that these protocols satisfy the other main security measures.
Cite This Paper
Reham Abdellatif Abouhogail, "A Comparative Analysis of Tools for Testing the Security Protocols", International Journal of Information Technology and Computer Science(IJITCS), Vol.11, No.12, pp.30-37, 2019. DOI:10.5815/ijitcs.2019.12.03
Reference
[1]Sebastian Mödersheim and Luca Vigano and David von Oheimb. Automated Validation of Security Protocols (AVASP). Lecture slides 2005.
[2]AVISPA v1.1 User Manual 2006.
[3]Michael Burrows, Martin Abadi, and Roger Needham. A logic of authentication. Technical Report 39, Digital Systems Research Center 1989.
[4]Thammarat C, Kurutach W. A lightweight and secure NFC‐base mobile payment protocol ensuring fair exchange based on a hybrid encryption algorithm with formal verification. Int J CommunSyst. 2019;32: e3991.https://doi.org/10.1002/dac.3991.
[5]Vanga Odelu, Ashok Kumar Das, and Adrijit Goswami. SEAP: Secure and Efficient Authentication Protocol for NFC Applications Using Pseudonyms. IEEE Transactions on Consumer Electronics 2016; 62. No. 1.:30-38.
[6]Reham Abdellatif Abouhogail, Mohammed S. Gadelrb. A New Secure and Privacy Preserved Protocol for IEEE802.11s Networks. Computers & Security Aug. 2018; 77: 745-755.
[7]Reham Abdellatif Abouhogail. A New Secure Lightweight Authentication Protocol for NFC mobile Payment. International Journal of Communication Networks and Information Security (IJCNIS) August 2019; Vol. 11, No. 2: 283-289.
[8]Hua Guo, Ya Gao, Tongge Xu, Xiyong Zhange, Jianfeng Y. A secure and efficient three-factor multi-gateway authentication protocol for wireless sensor networks. Ad Hoc Networks 2019; 95: 1-16.
[9]Sriramulu Bojjagani, V.N. Sastry. A secure end-to-end proximity NFC-based mobile payment protocol. Computer Standards & Interfaces 2019 Oct.; 66: 1-21.
[10]Michail Sidorov, Ming Tze Ong, Ravivarma Vikneswaran, Junya Nakamura, Ren Ohmura and Jing Huey Khor. Ultralightweight Mutual Authentication RFID Protocol for Blockchain Enabled Supply Chains. IEEE ACESS. DOI 10.1109/ACCESS.2018.2890389, IEEE Access.
[11]Reham Abdellatif Abouhogail. Improving the Handoff Latency of the Wireless Mesh Networks Standard. International Journal of Security and Its Applications 2016; 10: 73 -86.
[12]Reham Abdellatif Abouhogail. Fast Handover with Privacy Preserving Authentication Protocol for Mobile WiMAX Networks. International Journal of Security and Its Applications 2014; 8:361-376.
[13]Pascal Lafourcade, and Maxime Puys. Performance Evaluations of Cryptographic Protocols Veri_cation Tools Dealing with Algebraic Properties. International Symposium on Foundations and Practice of Security 2016.
[14]David A. Basin, Sebastian Modersheim, and Luca Vigano. Ofmc. A symbolic model checker for security protocols 2005; Int. J. Inf. Sec., 4(3):181- 208
[15]Mathieu Turuani. The CL-Atse Protocol Analyser. In Frank Pfenning, editor, 17th International Conference on Term Rewriting and Applications - RTA 2006 Lecture Notes in Computer Science, 4098 of LNCS: 277-286. Springer, August 2006.
[16]C.J.F. Cremers. The Scyther Tool: Verification, falsification, and analysis of security protocols. In Computer Aided Verification, 20th International Conference, CAV, 5123/2008 of LNCS, Springer, 2008: 414-418.
[17]Meier S., Schmidt B., Cremers C. Basin D. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In: Sharygina N., Veith H. (eds) Computer Aided Verification. CAV; 2013. Lecture Notes in Computer Science, vol 8044. Springer, Berlin, Heidelberg
[18]Cremers, C.J.F. The Scyther tool: Verification, falsification, and analysis of security protocols. Paper presented at CAV 2008. LNCS. Gupta, A., Malik, S. (eds.), vol. 5123, 414–418. Springer, Heidelberg 2008.
[19]B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In Proceedings of CSFW'01: 82-96. IEEE Comp. Soc. Press 2001.
[20]Bruno Blanchet, Ben Smyth, Vincent Cheval, and Marc Sylvestre. Cryptographic Protocol Verifier User Manual and Tutorial. May 16, 2018.
[21]Luca Vigan. Automated Security Protocol Analysis with the AVISPA Tool. Electronics notes in theoretical computer Science 2006; 155: 61–86.
[22]Ronan Saillard, Thomas Genet. CAS+. March 21, 2011. Available at:
[23]http://people.irisa.fr/Thomas.Genet/span/CAS_manual.pdf. [accessed 18.08.2019].
[24]Pisarev I.A., Babenko L.K. Registration protocol security analysis of the electronic voting system based on blinded intermediaries using the Avispa tool. In Proceedings of Trudy ISP RAN; 2018; 30; 4 155-168; Russia: ISP RAS
[25]Sheng Ding, Jin Cao, Chen Li, Kaifan, and Hui Li. A Novel Attribute-Based Access Control Scheme Using Blockchain for IoT. IEEE Access 2019; 7: 38431- 38441.
[26]Li Gong, Roger Needham, and Raphael Yahalom. Reasoning about belief in cryptographic protocols. In Proceedings of 1990 IEEE Symposium on Research in Security and Privacy; 1990 May 234–248. IEEE Computer Society.
[27]Paul F. Syverson and Paul C. van Oorschot. A unified cryptographic protocol logic. CHACS Report. 1996. NRL Publication. pp. 5540–227, Naval Research Lab.
[28]Ben Smyth. "FORMAL VERIFICATION OF CRYPTOGRAPHIC PROTOCOLS WITH AUTOMATED REASONING". Ph.D. thesis. University of Birmingham. March 2011.
[29]Colin Boyd and Wenbo Mao. On a Limitation of BAN Logic. Springer-Verlag, 1993: Pp.240-247.