Paper 2026/1065

Formal Analysis and Verification of DigiLocker with Tamarin

Abstract

Digilocker is a key component of India's Digital Public Infrastructure, enabling secure digital storage, retrieval, and sharing of government-issued documents. Given its large-scale deployment and reliance on protocols such as OAuth 2.0 with PKCE, HMAC-based API authentication, digital signatures, and encrypted storage, rigorous security assurance is essential which can not be be ensured through conventional testing alone. In this work, we present a formal modeling and verification of DigiLocker’s authentication and document-handling workflows using the Tamarin Prover. We model the OAuth 2.0 authorization code flow with PKCE, issuer-based document retrieval mechanisms (PullURI and PullDoc), document push workflows, and self-upload with encrypted storage under the Dolev–Yao adversary model. We formally specify and verify key security properties, including token secrecy, authorization code uniqueness, PKCE binding, document authenticity, integrity, confidentiality, and key management. Our results show that DigiLocker’s protocol design satisfies these properties under ideal assumptions. However, controlled credential-leak scenarios demonstrate that compromise of sensitive values such as API keys or digilockerids can lead to exploitable attack traces. This study highlights the value of formal verification in strengthening security guarantees for large-scale e-governance systems.