International Journal of Computer Network and Information Security (IJCNIS)
IJCNIS Vol. 8, No. 3, 8 Mar. 2016
Cover page and Table of Contents: PDF (size: 798KB)
Analysis of Cryptographic Protocols AKI, ARPKI and OPT using ProVerif and AVISPA
Full Text (PDF, 798KB), PP.34-40
Views: 0 Downloads: 0
Author(s)
Amol H. Shinde
1,*
A. J. Umbarkar
1
Index Terms
Formal Verification, Cryptographic Protocols, ProVerif, AVISPA, Comparison of Tools
Abstract
In recent years, the area of formal verification of cryptographic protocols became important because of the active intruders. These intruders can find out the flaws in the protocols and can use them to create attacks. To avoid such possible attacks, the protocols must be verified to check if the protocols contain any flaws. The formal verification tools have helped in verifying and correcting the protocols. Various tools are available these days for verifying the protocols. In this paper, the two verification tools namely ProVerif and AVISPA are used for analysis of protocols - AKI (Accountable Key Infrastructure), ARPKI (Attack Resilient Public Key Infrastructure) and OPT (Origin and Path Trace). A comparative evaluation of the selected tools is presented and revealed security properties of the protocols selected.
Cite This Paper
Amol H. Shinde, A. J. Umbarkar,"Analysis of Cryptographic Protocols AKI, ARPKI and OPT using ProVerif and AVISPA", International Journal of Computer Network and Information Security(IJCNIS), Vol.8, No.3, pp.34-40, 2016.DOI: 10.5815/ijcnis.2016.03.05
Reference
[1]C. Meadows, “Formal methods for cryptographic protocol analysis: emerging issues and trends,” IEEE Journal on Selected Areas in Communications, vol. 21, no. 1, pp. 44–54, 2003. doi: 10.1109/JSAC.2002.806125.
[2]B. Blanchet, “Automatic verification of correspondences for security protocols,” Journal of Computer Security, vol. 17, no. 4, pp. 363–434, 2009.
[3]L. Viganò “Automated security protocol analysis with the AVISPA tool,” Electr. Notes Theor. Comput. Sci., vol. 155, pp. 61–86, 2006. doi: 10.1016/j.entcs.2005.11.052.
[4]C. J. F. Cremers, “The scyther tool: Verification, falsification, and analysis of security protocols,” in Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, 2008, pp. 414–418. doi: 10.1007/978-3-540-70545-1_38.
[5]S. Meier, B. Schmidt, C. Cremers, and D. A. Basin, “The TAMARIN prover for the symbolic analysis of security protocols,” in Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, 2013, pp. 696–701. doi: 10.1007/978-3-642-39799-8_48.
[6]D. X. Song, S. Berezin, and A. Perrig, “Athena: A novel approach to efficient automatic security protocol analysis,” Journal of Computer Security, vol. 9, no. 1/2, pp. 47–74, 2001.
[7]C. Meadows, “The NRL protocol analyzer: An overview,” J. Log. Program., vol. 26, no. 2, pp. 113–131, 1996.
[8]Tiffany Hyun-Jin Kim, Lin-Shung Huang, Adrian Perrig, Collin Jackson, and Virgil D. Gligor. Accountable key infrastructure (AKI): a proposal for a public-key validation infrastructure. In 22nd International World Wide Web Conference, WWW '13, Rio de Janeiro, Brazil, May 13-17, 2013, pages 679-690, 2013.
[9]David A. Basin, Cas J. F. Cremers, Ti_any Hyun-Jin Kim, Adrian Perrig, Ralf Sasse, and Pawel Szalachowski. ARPKI: attack resilient public-key infrastructure. In Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, November 3-7, 2014, pages 382-393, 2014.
[10]Tiffany Hyun-Jin Kim, Cristina Basescu, Limin Jia, Soo Bum Lee, Yih-Chun Hu, and Adrian Perrig. Lightweight source authentication and path validation. In ACM SIGCOMM 2014 Conference, SIGCOMM'14, Chicago, IL, USA, August 17-22, 2014, pages 271-282, 2014.
[11]J. K. Millen, S. C. Clark, and S. B. Freedman, “The interrogator: Protocol security analysis,” IEEE Trans. Software Eng., vol. 13, no. 2, pp. 274–288, 1987.
[12]L. C. Paulson, “Isabelle: The next 700 theorem provers,” in Logic and computer science, vol. 31, 1990, pp. 361–386.
[13]B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filliatre, E. Gimenez, H. Herbelin, G. Huet, C. Munoz, C. Murthy, “The coq proof assistant reference manual: Version 6.1,” 1997.
[14]E. M. Clarke, S. Jha, and W. R. Marrero, “Verifying security protocols with brutus,” ACM Trans. Softw. Eng. Methodol., vol. 9, no. 4, pp. 443– 487, 2000.
[15]J. C. Mitchell, M. Mitchell, and U. Stern, “Automated analysis of cryptographic protocols using mur-phi,” in 1997 IEEE Symposium on Security and Privacy, May 4-7, 1997, Oakland, CA, USA, 1997, pp. 141–151.