Formal Verification of Peer-Assisted FIDO2 Passkey Recovery Protocol with Tamarin

The transition from passwords to FIDO2 passkeys eliminates phishing risks but introduces significant challenges in account recovery. While peer-Assisted recovery protocols have been proposed to address this for enterprises, the security of these protocols is often analyzed only via informal frameworks such as STRIDE and therefore lacks guarantees about algebraic interactions. To the best of our knowledge, prior work has not reported an unbounded symbolic verification of a peer-Assisted FIDO2 passkey recovery protocol, nor formally analyzed a peer-Assisted key-splitting design. In this work, we present the first comprehensive formal verification of a peer-Assisted FIDO2 recovery protocol using the Tamarin-prover. Our symbolic analysis invalidates the security claims of the original Single-Key design under an Eventually Compromised Server (ECS) model with trusted user registration and an out-of-band peer channel. We identify four vulnerabilities, three of which are critical key-compromise attacks, including a cross-context decryption oracle and a novel transitive key compromise, Domino Effect, where an adversary can cascade compromises through the trust graph, and the fourth attack, a cryptographic denial of service. To address these flaws, we propose and formally verify a hardened protocol variant incorporating a Double-Key Pair architecture, freshness and self-referential integrity checks. Our results show that, under the stated assumptions, the hardened protocol satisfies the target security properties for post-setup server compromise.