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

• Item type: Journal(1)
• 公開日: 2023-12-15
• タイトル: FIDO2の形式化の再考と複数モードの検証への拡張
• タイトル / 言語: en
• タイトル: Rethinking FIDO2 Formalization and Extending Verification of Multi-modes
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [特集:次世代デジタルプラットフォームにおける情報流通を支えるセキュリティとトラスト（特選論文）] FIDO2，WebAuthn2，CTAP2，形式検証，ProVerif
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• ID登録: 10.20729/00231436
• ID登録 / ID登録タイプ: JaLC
• 著者所属: 株式会社フレクト
• 著者所属: 茨城大学
• 著者所属(英): en
• 著者所属(英): FLECT CO., LTD.
• 著者所属(英): en
• 著者所属(英): Ibaraki University
• 著者名: 佐藤, 瑞己; 米山, 一樹
• 著者名(英): Mizuki, Sato; Kazuki, Yoneyama
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: FIDO2はトークンなどを用いたパスワードレス認証の実現を目的として標準化されているプロトコルである．ESORICS 2022において，GuanらはFIDO2に対するProVerifを用いた安全性の形式検証を行った．彼らは，FIDO2をサブプロトコルであるWebAuthn2とCTAP2の仕様に沿って形式化し，秘密情報の漏洩などを考慮した安全性を検証している．しかし，彼らの形式化には証明書の取扱いに関する軽微なミスがあり，仕様に忠実な形式化になっていないという問題があった．また，WebAuthn2とCTAPの組合せについて，形式化されていないモードや仕様が存在する．本研究では，まずGuanらの形式化の証明書の取扱いに関するミスを指摘し，修正する．次に，Guanらが形式化していなかったWebAuthn2のいくつかのモードとCTAPの異なる仕様の組合せについて形式化と検証を行う．また，CTAPの検証について，Barbosaらが提案したCTAP2の改良プロトコルであるsPACAについても形式化を行った．結果として，WebAuthn2におけるユーザ-クライアント間の認証性について，より弱めた攻撃者の下で，既存の検証では発見できなかった異なる攻撃が存在することを示す．具体的には，認証機-クライアント間の通信の過程で攻撃者は認証機によって保存されるユーザハンドルを差し替えることが可能となる．さらに，攻撃を防ぐためのWebAuthn2における修正方法を示す．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 64, 号 12, p. 1599-1613, 発行日 2023-12-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764
• 公開者 / 言語: ja
• 公開者 / 出版者: 情報処理学会