A Modern Mechanism for Formal Analysis of Biometric Authentication Security Protocol

Full Text (PDF, 702KB), PP.15-29

Views: 0 Downloads: 0

Author(s)

Pradeep R. 1,* N. R. Sunitha 1 G. S. Thejas 2

1. Department of Computer Science and Engineering, Siddaganga Institute of Technology, Tumakuru, 572103, India

2. Department of Computer Science and Electrical Engineering, Tarleton State University, Texas A&M University System, TX, USA

* Corresponding author.

DOI: https://doi.org/10.5815/ijcnis.2023.03.02

Received: 7 Oct. 2022 / Revised: 10 Jan. 2023 / Accepted: 1 Feb. 2023 / Published: 8 Jun. 2023

Index Terms

Biometric, Iris, Formal Verification, Model Checking, Scyther

Abstract

A Biometric Authentication Security (BAS) protocol is a method by which a person's unique physiological or behavioral characteristics are used to verify their identity. These characteristics can include fingerprints, facial features, voice patterns, and more. Biometric authentication has become increasingly popular in recent years due to its convenience and perceived security benefits. However, ensuring that the BAS protocols are secure and cannot be easily compromised. . Developing a highly secure biometric authentication protocol is challenging, and proving its correctness is another challenge. In this work, we present a modern mechanism for formally analyzing biometric authentication security protocol by taking a Aadhaar Level-0 Iris-based Authentication Protocol as a use case. The mechanism uses formal methods to formally verify the security of the Aadhaar Level-0 Iris-based Authentication protocol, and is based on the widely-used BAN logic (Buruccu, Abadi, and Needham). Using Scyther model checker we analyze the existing biometric authentication protocol and have shown its effectiveness in identifying potential security vulnerabilities. The proposed mechanism is based on a set of security requirements that must be met for the protocol to be considered secure. These requirements include the need for the protocol to be resistant to replay attacks, man-in-the-middle attacks, and impersonation attacks. The mechanism also considers the possibility of an attacker obtaining the biometric data of a legitimate user.

Cite This Paper

Pradeep R., N. R. Sunitha, G. S. Thejas, "A Modern Mechanism for Formal Analysis of Biometric Authentication Security Protocol", International Journal of Computer Network and Information Security(IJCNIS), Vol.15, No.3, pp.15-29, 2023. DOI:10.5815/ijcnis.2023.03.02

Reference

[1]I. Pali, L. Krishania, D. Chadha, A. Kandar, G. Varshney, and S. Shukla, “A Comprehensive Survey of Aadhar and Security Issues,” 2020, [Online]. Available: http://arxiv.org/abs/2007.09409
[2]B. C. Conference, “Biometric Authentication Features of UID ( Aadhaar ) Authentication,” no. September, 2013.
[3]P. Patil and S. Jagtap, “Multi-modal biometric system using finger knuckle image and retina image with template security using PolyU and DRIVE database,” Int. J. Inf. Technol., vol. 12, no. 4, pp. 1043–1050, 2020, doi: 10.1007/s41870-020-00501-0.
[4]T. J. Tsitaitse, Y. Cai, S. L. Suntu, and M. N. U. khan, “Secure and Fast Handovers Authentication Methods for Wi-Fi Based Networks: A Review perspective,” Int. J. Comput. Networks Appl., vol. 5, no. 3, pp. 32–42, 2018, doi: 10.22247/ijcna/2018/49434.
[5]K. Nandakumar, A. K. Jain, and A. Nagar, “Biometric template security,” EURASIP J. Adv. Signal Process., vol. 2008, 2008, doi: 10.1155/2008/579416.
[6]A. Dantcheva, P. Elia, and A. Ross, “What else does your biometric data reveal? A survey on soft biometrics,” IEEE Trans. Inf. Forensics Secur., vol. 11, no. 3, pp. 441–467, 2016, doi: 10.1109/TIFS.2015.2480381.
[7]N. Asokan, V. Niemi, and K. Nyberg, “Man-in-the-middle in tunnelled authentication protocols,” Lect. Notes Comput. Sci. (including Subser. Lect. Notes Artif. Intell. Lect. Notes Bioinformatics), vol. 3364 LNCS, pp. 28–41, 2005, doi: 10.1007/11542322_6.
[8]M. Tanveer, A. U. Khan, H. Shah, A. Alkhayyat, S. A. Chaudhry, and M. Ahmad, “ARAP-SG: Anonymous and Reliable Authentication Protocol for Smart Grids,” IEEE Access, vol. 9, pp. 143366–143377, 2021, doi: 10.1109/ACCESS.2021.3121291.
[9]Rekha and R. Gupta, “Elliptic curve cryptography based secure image transmission in clustered wireless sensor networks,” Int. J. Comput. Networks Appl., vol. 8, no. 1, pp. 67–78, 2021, doi: 10.22247/IJCNA/2021/207983.
[10]J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, “Symbolic model checking: 1020 States and beyond,” Inf. Comput., vol. 98, no. 2, pp. 142–170, 1992, doi: 10.1016/0890-5401(92)90017-A.
[11]H. Foster, Assertion-based verification: Industry myths to realities. 1973.
[12]K. Hofer-Schmitz and B. Stojanović, “Towards formal verification of IoT protocols: A Review,” Comput. Networks, vol. 174, no. March, 2020, doi: 10.1016/j.comnet.2020.107233.
[13]S. Zhang, A. Burns, J. Chen, and E. S. Lee, “Hard real-time communication with the timed token protocol: Current state and challenging problems,” Real-Time Syst., vol. 27, no. 3, pp. 271–295, 2004, doi: 10.1023/B:TIME.0000029051.60313.06.
[14]S. Liu and M. Silverman, “Practical guide to biometric security technology,” IT Prof., vol. 3, no. 1, pp. 27–32, 2001, doi: 10.1109/6294.899930.
[15]F. Boussinot, S. Ramesh, R. K. Shyamasundar, and R. De Simone, “Validation and analysis of the futurebus arbitration protocol: A case study,” Sadhana, vol. 21, no. 2, pp. 185–211, 1996, doi: 10.1007/BF02745519.
[16]K. Lodaya, M. Mukund, R. Ramanujam, and P. S. Thiagarajan, “Models and logics for true concurrency,” Sadhana, vol. 17, no. 1, pp. 131–165, 1992, doi: 10.1007/BF02811341.
[17]G. Klein, R. Huuck, and B. Schlich, “Operating system verification,” J. Autom. Reason., vol. 42, no. 2–4, pp. 123–124, 2009, doi: 10.1007/s10817-009-9126-9.
[18]W. R. Bevier, W. A. Hunt, J. S. Moore, and W. D. Young, “An approach to systems verification,” J. Autom. Reason., vol. 5, no. 4, pp. 411–428, 1989, doi: 10.1007/BF00243131.
[19]F. Flammini, A. Lazzaro, and N. Mazzocca, “Modeling of railway logics for reverse enginering, verification and refactoring,” Int. J. Saf. Secur. Eng., vol. 1, no. 1, pp. 77–94, 2011, doi: 10.2495/SAFE-V1-N1-77-94.
[20]M. J. Scott and E. K. Antonsson, “Arrow’s Theorem and engineering design decision making,” Res. Eng. Des. - Theory, Appl. Concurr. Eng., vol. 11, no. 4, pp. 218–228, 1999, doi: 10.1007/s001630050016.
[21]V. Kakkad, M. Patel, and M. Shah, “Biometric authentication and image encryption for image security in cloud framework,” Multiscale Multidiscip. Model. Exp. Des., vol. 2, no. 4, pp. 233–248, 2019, doi: 10.1007/s41939-019-00049-y.
[22]M. Ganavi, S. Prabhudeva, and S. N. Nayak, “A Secure Image Encryption and Embedding Approach using MRSA and RC6 with DCT Transformation,” Int. J. Comput. Networks Appl., vol. 9, no. 3, pp. 262–278, 2022, doi: 10.22247/ijcna/2022/212553.
[23]E. Liu, A. K. Jain, and J. Tian, “A coarse to fine minutiae-based latent palmprint matching,” IEEE Trans. Pattern Anal. Mach. Intell., vol. 35, no. 10, pp. 2307–2322, 2013, doi: 10.1109/TPAMI.2013.39.
[24]A. Herbadji, N. Guermat, L. Ziet, Z. Akhtar, M. Cheniti, and D. Herbadji, “Contactless multi-biometric system using fingerprint and palmprint selfies,” Trait. du Signal, vol. 37, no. 6, pp. 889–897, 2020, doi: 10.18280/TS.370602.