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.
