Security Analysis of Biometric Verification Protocol Using Scyther Model Checker: A Case Study
Article Sidebar
Main Article Content
Abstract
Aadhaar is a biometric-based national identification system used in India that relies on fingerprints, iris scans, and face images as primary means of verification. Ensuring the reliability and security of biometric protocols is critical, as they must be robust and resistant to attacks. To achieve and prove the reliability of a biometric security protocol, the traditional testing technique is not a desirable solution because of its limitations. The formal verification technique is a better solution to prove the reliability of a biometric security protocol as it provides mathematical proofs to validate security protocols. The biometric capture devices used in the Aadhaar system must comply with either Level-0 (L0) or Level-1 (L1) security standards as defined by the Unique Identification Authority of India (UIDAI). The L0 protocol is widely adopted due to its cost-effectiveness, though it is less secure compared to the L1 protocol. This paper focuses on the formal analysis and verification of the L0 iris-based biometric verification security protocol. Using the Scyther model checker, security vulnerabilities in the L0 protocol are identified. A security solution is then proposed by addressing these vulnerabilities and formally proving the correctness of the improved security model against the Dolev-Yao adversary model.
Article Details
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
Copyright Transfer Statement
The copyright of this article is transferred to Current Applied Science and Technology journal with effect if and when the article is accepted for publication. The copyright transfer covers the exclusive right to reproduce and distribute the article, including reprints, translations, photographic reproductions, electronic form (offline, online) or any other reproductions of similar nature.
The author warrants that this contribution is original and that he/she has full power to make this grant. The author signs for and accepts responsibility for releasing this material on behalf of any and all co-authors.
Here is the link for download: Copyright transfer form.pdf
References
Adeyanju, I. A., Emake, E. D., Olaniyan, O. M., Omidiora, E. O., Adefarati, T., Uzedhe, G. O., & Okomba, N. S. (2021). Digital industrial control systems: Vulnerabilities and security technologies. Current Applied Science and Technology, 21(1), 188-207. https://doi.org/10.14456/cast.2021.18
Baillot, P., & Ghyselen, A. (2022). Types for complexity of parallel computation in Pi-calculus. ACM Transactions on Programming Languages and Systems, 44(3), 1-50. https://doi.org/10.1145/3495529
Bao, H., Su, Y., Hua, Z., Chen, M., Xu, Q., & Bao, B. (2024). Grid homogeneous coexisting hyperchaos and hardware encryption for 2-D HNN-like map. IEEE Transactions on Circuits and Systems I: Regular Papers, 71(9), 4145-4155. https://doi.org/10.1109/TCSI.2024.3423805
Blanchet, B., Cheval, V., & Cortier, V. (2022). ProVerif with Lemmas, induction, fast subsumption, and much more. IEEE Symposium on Security and Privacy (69-86). IEEE. https://doi.org/10.1109/SP46214.2022.9833653
Cai, Z., Li, Y., & Zhao, Y. (2024). Murphi2Chisel: A protocol compiler from Murphi to Chisel. Proceedings of the 15th Asia-Pacific Symposium on Internetware (pp. 209-218). https://doi.org/10.1145/3671016.3671376
Celi, S., Hoyland, J., Stebila, D., & Wiggers, T. (2022). A tale of two models: Formal verification of KEMTLS via Tamarin. In V. Atluri, R. Di Pietro, C. D. Jensen, & W. Meng (Eds.). Computer Security – ESORICS 2022. Lecture Notes in Computer Science. Vol 13556 (pp. 63-83). Springer. https://doi.org/10.1007/978-3-031-17143-7_4
Garanina, N., Staroletov, S., & Gorlatch, S. (2023). Auto-tuning high-performance programs using model checking in Promela. https://doi.org/10.48550/arXiv.2305.09130
Jain, A. K., Deb, D., & Engelsma, J. J. (2022). Biometrics: Trust, but verify. IEEE Transactions on Biometrics, Behavior, and Identity Science, 4(3), 303-323. https://doi.org/10.1109/TBIOM.2021.3115465
Jiang, G.-J., Li, Z.-Y., Qiao, G., Chen, H.-X., Li, H. Bin, & Sun, H.-H. (2021). Reliability analysis of dynamic fault tree based on binary decision diagrams for explosive vehicle. Mathematical Problems in Engineering, 2021, Article 5559475. https://doi.org/10.1155/2021/5559475
Krichen, M. (2023). A survey on formal verification and validation techniques for internet of things. Applied Sciences, 13(14), Article 8122. https://doi.org/10.3390/app13148122
Le, T. M. C., Pham, X. T., & Le, V. T. (2024). Advancing security protocol verification: A comparative study of Scyther, Tamarin. Journal of Technical Education Science, 19(1), 43-53. https://doi.org/10.54644/jte.2024.1523
Lewis, M., Soudjani, S., & Zuliani, P. (2023). Formal verification of quantum programs: Theory, tools, and challenges. ACM Transactions on Quantum Computing, 5(1), 1-35. https://doi.org/10.1145/3624483
Pradeep, R., & Sunitha, N. R. (2022). Formal verification of CHAP PPP authentication protocol for smart city/safe city applications. Journal of Physics: Conference Series, 2161, Article 012046. https://doi.org/10.1088/1742-6596/2161/1/012046
Rakotonirina, I., Barthe, G., & Schneidewind, C. (2024). Decision and complexity of Dolev-Yao hyperproperties. Proceedings of the ACM on Programming Languages, 8, 1913-1944. https://doi.org/10.1145/3632906
Ram, A., Dutta, M. P., & Chakraborty, S. K. (2024). An authentication mechanism to prevent various security threats in software defined networking by using AVISPA. Journal of Scientific and Industrial Research, 83(9), 977-988. https://doi.org/10.56042/jsir.v83i9.6313
Sharma, S., Saini, A., & Chaudhury, S. (2023). A survey on biometric cryptosystems and their applications. Computers and Security, 134, Article 103458. https://doi.org/10.1016/j.cose.2023.103458
Sheik, A. T., Maple, C., & Epiphaniou, G. (2022). Considerations for secure MOSIP deployment. IET Conference Proceedings, 2022(8), 135-143. https://doi.org/10.1049/icp.2022.2054
Singh, R., & Jackson, S. (2021). Seeing like an Infrastructure: Low-resolution citizens and the Aadhaar identification project. Proceedings of the ACM on Human-Computer Interaction, 5(CSCW2), Article 315. https://doi.org/10.1145/3476056
Sireesha, V., & Reddy, S. R. K. (2016). Two levels fusion based multimodal biometric authentication using iris and fingerprint modalities. International Journal of Intelligent Engineering and Systems, 9(3), 21-35. https://doi.org/10.22266/ijies2016.0930.03
Thakur, G., Prajapat, S., Kumar, P., & Chen, C.-M. (2024). A privacy-preserving three-factor authentication system for IoT-enabled wireless sensor networks. Journal of Systems Architecture, 154, Article 103245. https://doi.org/10.1016/j.sysarc.2024.103245
Yang, K., Swope, A. M., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R., & Anandkumar, A. (2023). LeanDojo: Theorem proving with retrieval-augmented language models. 37th Conference on neural information processing systems (NeurIPS 2023) (pp. 1-40). NeurIPS.
