Decentralized Identity (DID) enhances authentication and privacy by empowering individuals to control their own digital identities, which has gained traction globally. To our knowledge, this paper presents the first end-to-end verification effort (from design to implementation) of a real-world Decentralized Identity (DID) protocol following the IIFAA DID standard, which has been deployed within the widely used super app Alipay and issued millions of DIDs in practice. We integrate formal verification into the development lifecycle of such industrial security protocol to systematically enhance its reliability from two levels: (1) At the design level, we utilized state-of-the-art protocol design verifier \textsc{Tamarin} to formally model the IIFAA DID standard under a realistic threat model tailored for super apps. We then formulated and performed automated verification of desired security properties using \textsc{Tamarin}. We identified several design flaws which may lead to security breach which are reported to the design team and fixed by new design. (2) At the implementation level, we first extract the desired specification derived from the verified symbolic model of protocol design in the form of a set of intermediate I/O specifications. Subsequently, we translate the I/O specifications into a set of functional specifications at the implementation level, which can then be verified by the automated tool \textsc{VeriFast}. We identified several inconsistencies between the implementation and the verified design which are fixed by the development team and led to verified implementation faithfully obeying the verified design, together offering an end-to-end verified secure DID protocol in Alipay super app.
Our work showcases how an industrial security protocol development team can design and implement a practical verified secure Decentralized Identity (DID) protocol with the help of end-to-end formal verification.