A Composability Analysis Framework for Web3 Wallet Recovery Mechanisms

A Composability Analysis Framework for Web3 Wallet Recovery Mechanisms

Speakers: Panagiotis Chatzigiannis; Coby Wang; Sunpreet Arora; Mohsen Minaei

Conference: IEEE S&P

YouTube: https://www.youtube.com/watch?v=iK977CBOFOw

Overview

The proliferation of Web3 technologies, particularly decentralized finance (DeFi) and non-fungible tokens (NFTs), has brought with it a critical challenge: secure and reliable management of private keys for blockchain accounts. Unlike traditional banking systems where institutions can reset passwords or recover lost accounts, the decentralized nature of blockchain means losing a private key often results in permanent loss of access to digital assets. This talk, presented by Panagiotis Chatzigiannis from Visa Research, introduces a novel composability analysis framework designed to formally assess the security of combined Web3 wallet recovery mechanisms.

The core problem addressed is the inherent trade-off between the availability and security of private keys. While various individual recovery methods exist—from mnemonic phrases and physical storage to multi-signature schemes and designated guardians—combining these approaches in a single wallet design can inadvertently introduce new, complex attack vectors. The research aims to provide a rigorous method for developers and users to determine if a composed wallet design remains secure, especially against rational adversaries who may collude.

This work is highly significant for the broader adoption of Web3. The fear of losing assets due to lost keys or compromised recovery mechanisms is a major barrier for mainstream users. By offering a framework for formal verification, the researchers provide a crucial tool for building more robust and trustworthy Web3 wallets, thereby enhancing user confidence and paving the way for a more secure decentralized future.

Background

▶ Watch: Introduction: Blockchain accounts and key loss problem (0:00)

The fundamental principle of blockchain accounts is the direct control of assets through a private key. This key acts as a digital signature, authorizing transactions and proving ownership. The security of this system hinges on two critical factors: the key must be available to the legitimate owner and secure from unauthorized access. The decentralized ethos of blockchain, while offering independence from central authorities, also means there's no "forgot my password" function; a lost key is a lost account, permanently.

Early attempts at key management often involved users remembering complex strings of numbers or mnemonic phrases (e.g., 12 random words). While these methods aimed for user control, they were largely impractical for most people due to the cognitive burden or the security risks associated with physical storage (e.g., writing down phrases on paper, storing on unsecured drives). The vulnerability of these methods led to high-profile stories of users losing significant assets, highlighting the urgent need for more robust solutions.

To address the availability-security trade-off, several advanced recovery mechanisms emerged. One approach involves secret sharing schemes, where a private key is broken into multiple shares, requiring a subset of these shares for reconstruction. While more secure than a single point of failure, losing even one critical share could still render the key unrecoverable. More sophisticated solutions leverage smart contract accounts, which offer greater flexibility than basic Bitcoin-style accounts. These allow for custom logic, such as setting spending limits for delegated agents or designating guardians. A guardian, a user-selected entity, can help replace a lost key with a new one through a contract function. To mitigate malicious guardian behavior, a dispute function is typically implemented, allowing the user to challenge an unauthorized key rotation within a specified time delay.

Another notable recovery method discussed is Kelp, a guardian-less recovery protocol. Kelp allows anyone to initiate a recovery process, but it relies on a complex system of collaterals and multiple time locks to deter malicious actors. An attacker attempting to take over an account must deposit collateral, which the legitimate user can claim if they successfully dispute the malicious recovery within a time window.

The challenge arises when developers attempt to combine these individual recovery methods to offer users multiple recovery paths, aiming for the "best of all worlds." While intuitively appealing, the interactions between these disparate mechanisms are often non-obvious and can introduce unforeseen vulnerabilities. Prior to this research, there was no formal, systematic way to determine if a composed solution still achieved its intended security goals, especially when considering the potential for collusion among various agents involved in the recovery process. This gap in formal analysis is a major impediment to the widespread adoption of Web3 wallets, as users and developers lack confidence in the security of complex recovery designs.

Key Findings

▶ Watch: The 'chicken problem' in wallet recovery design (4:15)

The central contribution of this research is the development of a composability analysis framework specifically tailored for Web3 wallet recovery mechanisms. This framework provides a formal and systematic approach to evaluate the security of wallet designs that integrate multiple recovery paths. The key findings and contributions are:

1. Formal Security Analysis for Composed Designs: The framework addresses the critical gap in understanding how different recovery mechanisms interact when combined. It provides a method to formally analyze whether a composite wallet design maintains its security properties, rather than relying on informal reasoning or ad-hoc testing.
2. Rational Adversary Model: The research introduces a model where an adversary is assumed to be rational, controlling various agents associated with the wallet, and always acting to maximize their expected financial gain. This realistic adversarial model allows for the identification of attack strategies, including collusion, that might otherwise be overlooked.
3. Application of Model Checking: The framework leverages model checking as a formal verification method. This allows for an exhaustive exploration of all possible state transitions and agent interactions within a given wallet design, considering probabilities and parameters, to identify potential insecure states. This provides a much more accurate and faster analysis than manual methods, especially for complex systems.
4. Identification of Collusion Vulnerabilities: The analysis demonstrates that combining recovery paths can create new and unexpected vulnerabilities, particularly when agents collude. The framework systematically uncovers these collusion attack vectors, showing how seemingly secure individual mechanisms can become insecure when their controlling agents cooperate maliciously.
5. Counter-intuitive Impact of Parameters: The study reveals that certain design parameters, such as time delays in dispute mechanisms, do not always work to the user's advantage. In some scenarios, longer time delays can provide adversaries with more time to execute attacks, locking out the legitimate user for extended periods. This finding is crucial for guiding developers in parameter tuning.
6. Parameter Sensitivity Analysis: The framework enables parameter sensitivity analysis, allowing developers to understand the influence of each design parameter (e.g., wallet value, reputation values, time locks) on the overall security of the wallet. This helps in making informed decisions for designing more robust and resilient Web3 wallets.

In essence, the research provides a much-needed formal toolkit to move beyond guesswork in Web3 wallet design, offering concrete methods to identify and mitigate complex security risks arising from the composability of recovery mechanisms.

Technical Deep Dive

▶ Watch: Introduction to smart contract accounts and flexibility (5:00)

The core of the proposed framework lies in its ability to formally model and analyze the interactions between various agents and recovery mechanisms within a Web3 wallet. This is achieved through a rational adversary model coupled with model checking techniques.

Agent-Based Model:

The framework models a Web3 wallet as interacting with several agents (V1, V2, etc.). These agents can be categorized as:

• Spending Agents: Possess some degree of spending power over the wallet's funds, potentially with limits.
• Recovery Agents: Participate in a wallet recovery scheme, helping the user regain access to a lost key.

Each agent is associated with a reputation value (Y). This value can be influenced by their actions. Agents can choose between two primary strategies:

1. Conservative Action (AC): The agent follows the protocol as intended. In this case, their reputation value is preserved, and they end the "game" with the same reputation they started with.
2. Attack Action: The agent deviates from the protocol with the intention of stealing funds. The success of an attack action is probabilistic. If successful, the agent gains value (e.g., a portion of the wallet's funds); if unsuccessful or disputed, they may lose reputation or deposited collateral.

Rational Adversary and Security Definition:

The framework assumes a rational adversary who controls all agents involved with the wallet. This adversary's primary goal is to maximize the expected winning value by choosing the optimal strategy for each agent (individually or in collusion).

A wallet design is considered secure if the rational adversary's best strategy, for all agents, is to simply follow the protocol (conservative action). Conversely, if there is any deviation from the protocol that offers a higher expected value for the adversary, the design is deemed insecure. This security assessment is highly dependent on various parameters, including:

• The total wallet value.
• The reputation values of individual agents.
• The time delays specified in smart contracts for dispute periods.
• The probability of the user responding in time to a malicious action.

Model Checking for Exhaustive Analysis:

To answer the question of security for complex designs and parameter sets, the framework employs model checking. This formal verification method works by:

1. Translating the System: The entire wallet design, including all agents, their strategies, possible actions, and associated probabilities and parameters, is translated into a state transition system. This system represents all possible states the wallet and its agents can be in, and all possible transitions between these states.
2. Exhaustive Search: The model checker then exhaustively explores all possible transition paths within this system. It considers the probabilities associated with different actions (e.g., successful attack, user dispute) and calculates the likelihood of reaching each end state.
3. Identifying Problematic States: By systematically searching through all states, the model checker can identify specific conditions or sequences of actions that lead to an insecure outcome for the user. This is significantly more accurate and faster than manual analysis, especially for designs with many interacting components.

Illustrative Wallet Designs and Attack Scenarios:

The talk presents two primary example wallet designs to demonstrate the framework's capabilities:

Design 1:

This design features:

• SK1: The user's primary secret key, stored on their phone.
• Spending Agent (Agent 1): Holds SK2, allowing limited spending (e.g., up to $100 for SK2 alone, up to $2,000 with both SK1 and SK2).
• Recovery Path 1 (Secret Sharing): SK1 is split into two shares; one stored in the user's cloud, the other held by Agent 2.
• Recovery Path 2 (Guardian): Agent 3 acts as a guardian, capable of rotating the master public key (PK1 to PK1 prime) if the user loses SK1. Agent 4 is a dedicated dispute agent, able to challenge Agent 3's malicious key rotations. The user can also dispute if SK1 is still available.

The framework analyzes various attack scenarios:

• Individual Attacks:
• Agent 1 drains low amounts. User can rotate key.
• Agent 2 (holding a share) blackmails user for a percentage (e.g., 10% of wallet value) before releasing the share. User can use Recovery Path 2.
• Agent 3 performs a malicious key rotation to take over the account. User or Agent 4 can dispute.
• Agent 4 refuses to dispute a malicious rotation. User can still dispute or use Recovery Path 1.
• Collusion Attacks:
• Agent 1 + Agent 2: Agent 2 informs Agent 1 that the user lost SK1, prompting Agent 1 to drain the wallet. User can still recover via Agent 3.
• Agent 2 + Agent 3: Both agents deny recovery. The user is left without options, potentially losing all funds. This is a critical vulnerability highlighted by the framework.
• Agent 1 + Agent 3 + Agent 4: Agent 3 does unauthorized key rotation, Agent 4 doesn't dispute, Agent 1 drains the wallet. User must act fast before time lock expires, but substantial damage might already occur.

Design 2 (Adding Kelp):

This design extends Design 1 by adding a third recovery path using Kelp.

• Recovery Path 3 (Kelp): Utilizes the Kelp protocol, with Agent 5 as a dedicated dispute agent for Kelp recoveries.

New collusion scenarios arise:

• Agent 2 + Agent 5: Agent 2 denies recovery, and Agent 5 initiates a Kelp recovery to take over the account. If the user doesn't have SK1, it becomes a race against time for recovery via Path 2.
• Agent 2 + Agent 3 + Agent 5: This powerful coalition can deny both Path 1 and Path 2 recoveries, and then immediately initiate a Kelp takeover. Unless the user still secretly holds SK1 (which contradicts the recovery request), the account will be taken over.

The framework processes these scenarios, producing visual representations (e.g., graphs with blue for secure, red for insecure regions) based on parameter variations (e.g., wallet value, reputation, time delays). This allows developers to understand the specific conditions under which their wallet design remains secure.

Demo / Proof of Concept

▶ Watch: How guardian-based wallet recovery works (6:00)

While the talk did not present a live software demonstration or a specific Proof of Concept tool in the traditional sense, the speakers effectively illustrated the framework's application through detailed analysis of hypothetical, yet realistic, composed Web3 wallet designs. The "demo" was conceptual, demonstrating the framework's analytical process and its ability to uncover non-obvious vulnerabilities.

The core of this illustrative "proof of concept" was the step-by-step breakdown of two distinct wallet designs, detailing their components, agents, and various recovery paths. For each design, the speakers meticulously walked through:

1. Individual Agent Malicious Actions: Showing how a single agent might attempt to exploit the system (e.g., Agent 1 draining funds, Agent 2 blackmailing, Agent 3 performing malicious key rotation).
2. Collusion Scenarios: Highlighting the critical insights gained from the framework, where combinations of malicious agents could lead to severe compromises (e.g., Agents 2 and 3 colluding to deny all recovery, Agents 2, 3, and 5 colluding for a complete account takeover).
3. Parameter Influence: Discussing how varying parameters like wallet value, agent reputation, and contract time delays directly impact the security outcome.

The visual representation, such as graphs depicting regions of "secure" (blue) versus "insecure" (red) based on parameter values, served as a clear demonstration of the framework's output. This showed how developers could use the framework to input their specific wallet parameters and receive an assessment of its security posture, thereby making informed design choices. This analytical approach, powered by model checking, serves as a robust proof of concept for the framework's utility in identifying and mitigating complex security risks in Web3 wallet composability.

Defensive Implications

▶ Watch: Mitigating malicious guardians with dispute mechanisms (6:40)

The composability analysis framework provides critical insights and actionable strategies for both Web3 wallet developers and users to enhance security.

For Web3 Wallet Developers:

• Prioritize Formal Analysis: Before deploying any complex wallet design that combines multiple recovery mechanisms, developers should rigorously apply formal analysis tools like this framework. Relying solely on intuition or individual component security is insufficient.
• Beware of Collusion Risks: The framework vividly demonstrates that the greatest threats often arise from collusion among seemingly independent agents. Developers must design recovery schemes with this in mind, ensuring that no combination of agents can unilaterally compromise a user's funds or deny all recovery paths.
• Careful Parameter Tuning: Parameters such as time delays for dispute functions, collateral amounts for guardian-less recoveries (like Kelp), and the reputation values assigned to agents are not benign. The research shows that longer time delays, counter-intuitively, can sometimes work against the user by giving adversaries more time to drain accounts. Developers must perform parameter sensitivity analysis to find optimal values that balance security and usability.
• Design for Redundancy with Independence: While offering multiple recovery paths is good, ensure these paths are genuinely independent in their failure modes. If different paths rely on overlapping sets of agents or share critical single points of failure, the intended redundancy is negated.
• Transparency and User Education: While not directly part of the technical framework, the implications suggest that developers should be transparent with users about the security model of their wallets, especially concerning potential collusion risks and the need for timely user action in dispute scenarios.
• Continuous Evaluation: The framework can be extended to model dynamically changing parameters or even potential software flaws not caught by auditors. Developers should consider integrating such dynamic analysis into their development lifecycle.

For Web3 Wallet Users:

• Understand Your Wallet's Security Model: Users should ideally seek to understand how their chosen wallet handles key recovery, especially if it involves multiple agents or complex smart contract logic. While the framework is for developers, its findings underscore the complexity.
• Be Vigilant and Responsive: If a wallet design includes dispute mechanisms, users must be prepared to act quickly if they suspect malicious activity. The concept of "time locks" means that inaction can lead to permanent loss.
• Diversify Trust: If a wallet relies on multiple guardians or recovery agents, users should carefully select these entities, ideally ensuring they are independent and trustworthy. The risk of collusion is real.
• Question Complex Designs: If a wallet's recovery mechanism seems overly convoluted, it might be hiding unforeseen vulnerabilities. While complexity can offer features, it also introduces attack surface.

Ultimately, the framework equips developers with the tools to build more resilient Web3 wallets, thereby providing users with greater assurance and contributing to the safer, broader adoption of decentralized technologies.

Key Takeaways

• Composing Web3 wallet recovery mechanisms introduces complex and often non-obvious security risks that cannot be adequately assessed through intuition alone.
• A formal analysis framework, leveraging model checking, is crucial for exhaustively evaluating the security of composite wallet designs, especially against rational and colluding adversaries.
• The rational adversary model, which assumes agents act to maximize expected financial gain, effectively uncovers collusion vulnerabilities that might otherwise be overlooked in multi-agent recovery schemes.
• Design parameters, such as time delays in dispute mechanisms and agent reputation values, significantly influence a wallet's security posture, with counter-intuitive findings like longer time delays sometimes working against the user.
• The framework aids developers in performing parameter sensitivity analysis, enabling them to make informed decisions for designing more robust and resilient Web3 wallets.
• By providing a method for rigorous security assessment, this research is a vital step towards building trustworthy Web3 infrastructure, which is essential for mainstream adoption of decentralized technologies.

About the Speaker(s)

The talk was presented by Panagiotis Chatzigiannis, representing Visa Research. He is one of the co-authors of the paper, alongside Coby Wang, Sunpreet Arora, and Mohsen Minaei. Their affiliation with Visa Research indicates a focus on cutting-edge financial technology and security, particularly within the nascent Web3 and blockchain ecosystems. Their work on this composability analysis framework highlights a commitment to addressing fundamental security challenges that impede the broader adoption and reliability of decentralized digital asset management systems. The collective expertise of the authors likely spans areas such as formal methods, blockchain security, cryptography, and economic modeling of adversarial behavior.