A Formal Security Analysis of IIFAA DID in Super Apps

A DID Document is a key component of decentralized identity, containing claims (attributes), cryptographic keys, authentication protocols, and service endpoints. These elements enable identity verification and secure communication.

A DID system facilitates credential issuance, authentication, and verification among three roles: holder, issuer, and verifier. Note that verifier corresponds to the Service Provider (SP) in the original IIFAA Decentralized Authentication Technical Specification [IIFAADID]. The issuer issues a verifiable credential (VC) to the holder, who later generates a verifiable presentation (VP) for the verifier. A key feature, selective disclosure, allows the holder to share only necessary claims while protecting other personal information.

A VC is a cryptographically secured digital certificate linking a holder to verified attributes. It contains three components: (1) Meta (metadata like validity dates), (2) Claims (verifiable information), and (3) proofVC (a cryptographic proof ensuring integrity and issuer authenticity).

A VP is a cryptographically signed document compiled by the holder, containing one or more VCs. It proves credential possession while enabling selective disclosure. Like a VC, it includes proofVP to ensure integrity and authenticity, allowing verifiers to trust the claims without contacting the issuer.

A super app like Alipay hosts multiple mini-programs, offering diverse services through a unified interface. It consists of a frontend client on the phone and a backend server operated by the super app developer, while each mini-program has its own frontend client and remote backend server. In a DID protocol within a super app, the holder, issuer, and verifier roles map to the super app client (securely managing private keys and credentials in trusted environments like TEE), the mini-program client, and the mini-program server, respectively.

Consider a mini-program on Alipay. The four entities interact as follows:

1. Alipay Client manages mini-program lifecycle, integrity, authentication, and permissions, providing APIs for interaction with Alipay's lower-layer services.
2. Alipay Server handles user management, API interactions, and service implementation for the Alipay client.
3. Mini-Program Client, developed using web technologies, interacts with the Alipay client via JSAPI [AlipayJSAPI] and communicates with its server over TLS.
4. Mini-Program Server, maintained by its developer, processes business logic and data while adhering to Alipay's security standards. It communicates with the Alipay server via OpenAPI [OpenAPI], enforcing mutual message signing for authentication and data integrity.

Mini-program integrity is ensured through signature verification. Upon release, the platform signs the mini-program code and configuration file (generated by the Alipay Server). The Alipay client verifies this signature before execution.

JSAPI access control rules are defined in the mini-program's configuration file. DID-related JSAPIs or plugins require explicit permission, granted only to enterprise mini-programs after a business contract. As a result, multiple mini-programs can access DID services on a holder's device, but the JSAPI link lacks additional encryption and integration protection.

Like other DID standards [MEVID, BSNDID, eIDAS], IIFAA [IIFAADID] is informal and written in a native language. Figure 1 outlines its implementation in Alipay for a specific mini-program on the platform. We distilled the protocol into two sub-protocols—VC Issuance and VP Verification—by manually reviewing the IIFAA standard [IIFAADID] and Alipay implementation documents. The procedures "VC Construction” and "VP Construction” will be referenced in Section 4.2.

As described in Section 2.2, the Alipay client acts as the holder, managing private keys and credentials in a trusted environment (TEE) via services provided by the Alipay server. The mini-program's client (frontend) and server (backend server) function as the issuer for VC issuance and the verifier for VP verification. Message exchanges primarily rely on JSAPI calls and TLS.

Our formal model covers the following aspects of IIFAA: (1) initialization, (2) VC Issuance, (3) VP Verification, (4) SD-JWT Data Format, (5) TLS and JSAPI Calls, and (6) Adversary Capabilities.

Initialization. The protocol starts by initializing a mini-program within a user's Alipay app using the multiset rewriting rule (MSR):

rule MiniprogramRegister:
  [ Fr(~appid), Fr(~openid), Fr(~k),
    !SuperApp(name, phoneNumber, userid) ]
  --[ MiniprogramReg($A, userid, ~appid)]->
  [ !MiniProgram($A, ~openid, ~appid), 
    !MLTK($A, ~k), !MPK($A, pk(~k)) ] 
  

A variable is fresh if prefixed by ~ and public if prefixed by $. To enhance privacy, the Alipay client anonymizes userid across mini-programs, replacing it with openid [Alipay-Docs] to prevent tracking. Each registered mini-program has a unique appid. Upon registration, a persistent key pair (!MLTK, !MPK) is generated, with !MPK stored in the DID document for signature verification. The identifier $A denotes the mini-program's role, either $issuer or $verifier.

VC Issuance. As shown in Figure 1, the Alipay user requests a $\mathtt{\text{VC}}$ via the mini-program frontend and receives it upon issuance. The process involves: (i) verifying the holder's claims and (ii) constructing the $\mathtt{\text{VC}}.$

User information (e.g., name and age) is stored on the Alipay server and accessed via OAuth 2.0 [OAuth2.0], specifically the authorization code flow. Upon user consent, Alipay generates an authorization code (AuthCode) for the mini-program, which exchanges it for a short-lived access token to retrieve user data. We abstract this process, modeling only the TLS exchange between the mini-program's server and Alipay servers.

According to the basic user information, the issuer generates the claims about this user (e.g., student of Zhejiang Univ.), then constructs a VC based on the W3C standard [VC-Data-Integrity-1.0]. We model SD-JWT [sdjwt], which enables selective disclosure in a JSON-encoded structure within a JWS payload, aligning with [IIFAADID].

As shown in Figure 1, the "VC Construction" process works as follows: $\mathtt{\text{C}}=\{c_1,\dots ,c_n\}$ denotes all claims available, $\mathtt{\text{digest}}$ represents the concatenation of their hashes, and $\mathtt{\text{sigJWT}}$ is the concatenation of $\mathtt{\text{digest}}$ and its issuer-signed value using the private key ${\mathsf{sk}}_{\mathtt{\text{I}}}$. For secure transmission to the Alipay client, the VC is encrypted with an envelope key in practice. In contrast, the IIFAA technical specification specifies encryption using the holder's DID public key.

VP Verification. As shown in Figure 1, a VP verification request originates from the mini-program frontend. The Alipay client, as the holder, constructs the VP using a single VC stored in TEE on the device (see Section 3).

During "VP Construction", the holder selects claims $\mathtt{\text{D}}=\{c_{i_1},\dots ,c_{i_k}\}$ from $\mathtt{\text{C}}=\{c_1,\dots ,c_n\}$, excluding private claims $\mathtt{\text{C}}\setminus \mathtt{\text{P}}$, to form ${\mathtt{\text{VC}}}^{\prime }$. The holder signs ${\mathtt{\text{VC}}}^{\prime }$ with their private key ${\mathsf{sk}}_{\mathtt{\text{H}}}$, generating $\mathtt{\text{sigH}}$ as proof of origin. The verifier checks $\mathtt{\text{sigH}}$ with the holder's public key ${\mathsf{pk}}_{\mathtt{\text{H}}}$, verifies $\mathtt{\text{sigJWT}}$ using the issuer's public key ${\mathsf{pk}}_{\mathtt{\text{I}}}$ for authenticity, and confirms $\mathtt{\text{D}}$ matches its hash in $\mathtt{\text{digest}}$.

We model a term structure in Tamarin using the tuple operator $⟨\cdot ⟩$ and multiset union $+$. The associative and commutative properties of $+$ enable selective disclosure modeling via the subterm relation $⊏$ [subterm].

SD-JWT Data Format. SD-JWT [sdjwt] is a composite JSON-encoded JWS structure enabling selective disclosure. By separating claims during VC issuance (as shown in the "VC Construction" process in Figure 1), its signature proof remains valid even when some claims are selectively removed.

TLS and JSAPI Calls. TLS secures communication between mini-program servers and the Alipay server (10 rules), while JSAPI calls enable interactions between mini-program clients and the Alipay client (4 rules).

Adversary Capabilities. We define 10 rules to model adversary capabilities for handling mobile app hooks and private key leakage (see Section 3).

Tamarin requires manual intervention for protocols with large state spaces. We use interactive mode to refine proof strategies, record solving steps, and apply regex-based heuristics for automation. Auxiliary lemmas further aid verification.

This work complements manual auditing by verifying IIFAA [IIFAADID] in Alipay, identifying security assumptions, and proposing mitigations for potential attacks.

Following [Morio2023, Girol2020], we formalize each security goal as $\tau \Rightarrow C\vee P_1\vee \cdots \vee P_n$, where $\tau$ is the trigger event [Girol2020], $C$ is the intended security property, and $P_i$ represents the $i$-th attack vector violating $C$.

This rule states: if $\tau$ holds, then either $C$ is satisfied, or an attack vector $P_i$ exists. To identify all the attack vectors, we start with $\tau \Rightarrow C$. When Tamarin finds the first attack trace $P_1$, it is added to the formula. This process repeats iteratively until $\tau \Rightarrow C\vee P_1\vee \cdots \vee P_n$ holds, ensuring no further attack vectors exist.

As shown in Table 1, our analysis validates three security goals (Executability, Integrity, and Selective Disclosure) and finds that the satisfaction of the other three goals (Secrecy, Injective Agreement, and Legal Presentation) requires additional conditions. We reported these to developers, who confirmed that mitigation solutions were deployed.

1. Multiple VPs may recover VC

The falsification of Goal 1 (Secrecy) reveals that an adversary controlling multiple mini-program verifiers can reconstruct a $\mathtt{\text{VC}}$ from its $\mathtt{\text{VP}}$s by observing inputs, outputs, and using compromised private keys for decryption.

The attack proceeds as follows:

1. Malicious verifiers $V$ send VP requests to the same holder.
2. Each verifier $v_i\in V$ receives ${\mathtt{\text{VP}}}_i$, decrypts it using ${\mathsf{sk}}_{v_i}$, and collects the disclosed claims.
3. Since different VPs may reveal different parts of a VC, the adversary aggregates claims ${\mathit{c}}_i$ from multiple ${\mathtt{\text{VP}}}_i$ to reconstruct the original VC as:
   $\mathtt{\text{VC}}\leftarrow \mathtt{\text{sigJWT}}\Vert {\mathit{c}}_1\Vert \cdots \Vert {\mathit{c}}_n$

In practice, enterprise mini-program verifiers undergo strict registration and audits, making it difficult—but not impossible—for an attacker to control multiple malicious mini-programs to execute this attack.

This attack underscores the need for stricter security in enterprise verifiers, including rigorous registration, auditing, and compliance checks. VP verification should also require user confirmation, particularly for sensitive data, ensuring undisclosed claims remain protected. Additionally, zero-knowledge proof technology can be employed to protect users' sensitive information, preventing verifiers from obtaining accurate personal privacy data.

2. Lack of Challenge Code Enables VP Replay

The falsification of Goal 3 (Injective Agreement) confirms a replay attack in VP verification, as noted in [Braun2024]. Like W3C standards [VC-Data-Integrity-1.0], IIFAA DID [IIFAADID] treats challenge codes as optional. While we recommend using a challenge-response mechanism to prevent replay attacks, developers argue that some applications omit it for efficiency, especially when replay attacks have inconsequential consequences.

Based on our analysis, we recommend a thorough risk assessment to balance efficiency and security, ensuring that omitting challenge codes is justified and aligns with the application's security needs.

3. Decoupling VP from Presenter Identity

Verifying Goal 4 (Legal Presentation) reveals that VPs are not directly bound to the presenter. A VP remains valid even if forwarded to another holder, creating a privacy risk where verification does not confirm the original presenter's identity.

On mobile platforms (e.g., the Alipay client), we recommend implementing VP verification as an "atomic operation" (e.g., one-click actions like "click-to-jump") to minimize the window for interception and misuse. Optionally, biometric authentication (e.g., facial or fingerprint recognition [fingerprint]) can be integrated based on risk levels, further binding a VP to its legitimate user.

A bottom-up modeling approach enhances the efficiency and scalability of DID protocol analysis, facilitating its integration into practical auditing workflows—our most valuable takeaway.

Formal analysis of protocols is highly time-consuming. Extracting the complete protocol (see Section 2.3), modeling in Tamarin (see Section 3.1), and developing proof strategies took approximately three person-months. The final model comprises 33 rules, totalling $\sim 1000$ lines of code (LoC).

In practice, the lifecycle of protocols like DID—from design to deployment—evolves rapidly, demanding a verification approach distinct from most academic security studies [SPDM, EME, 5GAKA, TLS1.3]. Existing research emphasizes low-level details (e.g., handshake mechanisms), resulting in complex models with limited scalability. The high effort required to build formal models from scratch further hinders the adoption of automated formal methods in industry.

Enhancing the efficiency of formal analysis is crucial for real-world adoption. As DID depends on infrastructure like TLS, a bottom-up approach proved effective in formalizing complex models like IIFAA DID [IIFAADID]. By initially modeling foundational components such as TLS and JSAPI, integrating these into an updated or entirely new DID protocol model becomes more streamlined. This reuse of models boosts scalability and reduces modeling and proof efforts, vital as [IIFAADID] and similar standards [MEVID, BSNDID, eIDAS] evolve.