FIDO2の形式化の再考と複数モードの検証への拡張

FIDO2はトークンなどを用いたパスワードレス認証の実現を目的として標準化されているプロトコルである．ESORICS 2022において，GuanらはFIDO2に対するProVerifを用いた安全性の形式検証を行った．彼らは，FIDO2をサブプロトコルであるWebAuthn2とCTAP2の仕様に沿って形式化し，秘密情報の漏洩などを考慮した安全性を検証している．しかし，彼らの形式化には証明書の取扱いに関する軽微なミスがあり，仕様に忠実な形式化になっていないという問題があった．また，WebAuthn2とCTAPの組合せについて，形式化されていないモードや仕様が存在する．本研究では，まずGuanらの形式化の証明書の取扱いに関するミスを指摘し，修正する．次に，Guanらが形式化していなかったWebAuthn2のいくつかのモードとCTAPの異なる仕様の組合せについて形式化と検証を行う．また，CTAPの検証について，Barbosaらが提案したCTAP2の改良プロトコルであるsPACAについても形式化を行った．結果として，WebAuthn2におけるユーザ-クライアント間の認証性について，より弱めた攻撃者の下で，既存の検証では発見できなかった異なる攻撃が存在することを示す．具体的には，認証機-クライアント間の通信の過程で攻撃者は認証機によって保存されるユーザハンドルを差し替えることが可能となる．さらに，攻撃を防ぐためのWebAuthn2における修正方法を示す．

Fast Identity Online2 (FIDO2) is the protocol to authenticate a device without passwords but with some token. Guan et al. formalized FIDO2 with ProVerif and verify security properties. They formalized FIDO2 according to the specifications of sub-protocols WebAuthn2 and CTAP2 respectively and verify security properties in terms of leakage of secret information. First, we point out and fix a minor error in the treatment of certificates in the formalization by Guan et al. Then, we show the formal analysis against multiple modes of WebAuthn and multiple versions of CTAP, which Guan et al. did not formalize. In the verification of CTAP, an improved protocol (sPACA) of CTAP2 proposed by Barbosa et al. is also formalized and analyzed. We find different attacks on user-to-client authenticity in WebAuthn2 under a weaker attacker than Guan et al's. In our attack, an attacker can replace a user handle that is stored by an authenticator by modifying a message in the channel between the authenticator and the client. Also, we give a countermeasure of the attack by showing a modification of WebAuthn2.