一句话：首次对支付宝实际部署的 IIFAA DID 协议做从设计到实现的端到端形式化验证，发现并修复安全缺陷。
去中心化身份（DID）提升认证与隐私，但工业级协议从设计到实现的全链路正确性难以保证。本文对遵循 IIFAA DID 标准、已部署于支付宝并签发数百万 DID 的真实协议开展端到端形式化验证。设计层用 Tamarin 在超级 App 威胁模型下建模并自动验证安全属性，发现并修复多个设计缺陷。实现层从已验证符号模型提取 I/O 规约并转化为函数式规约，用 VeriFast 验证实现，发现并修复实现与设计的不一致，使实现忠实遵循已验证设计。该工作展示了端到端形式化验证在工业安全协议中的可行性。
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 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 Tamarin. We identified several design flaws that could lead to a security breach. These issues were reported to the design team and have been addressed in the updated 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 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.
DOI 原文 ·
@inproceedings{paperbot9451,
title = {Securing Millions of Decentralized Identities in Alipay Super App with End-to-End Formal Verification},
author = {Ziyu Mao and Xiaolin Ma and Lin Huang and Huan Yang and Wu Zhang and Weichao Sun and Yongtao Wang and Jingling Xue and Jingyi Wang},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00305}
}