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

［情報処理学会論文誌 Vol.64　No.12, pp.1599-1613］

［論文概要］

FIDO2はトークンなどを用いたパスワードレス認証の実現を目的として標準化されているプロトコルであり、既存研究において検証ツールProVerifを用いた安全性の形式検証が行われている。しかし、既存の形式化は仕様に忠実ではないという問題があり、また形式化されていないプロトコルのモードや仕様が存在する。本研究では、仕様に忠実な形式化を与え、既存研究で形式化されていなかったFIDO2の仕様の組合せについて検証を行った。結果として、既存の検証では発見できなかった攻撃が存在することを示し、それに対するプロトコルの修正方法を示した。

［受賞理由］

本論文は広く利用されている認証プロトコルであるFIDO2に対して形式検証ツールを用いて安全性検証を行い，自明ではない攻撃方法を明らかにした上でその対策も示しており，社会的意義が顕著な論文である．また，形式化コードの公開やFIDOコミュニティへの報告も行っており，セキュリティ分野への貢献も評価できる．以上から，論文賞に相応しい優れた論文であると言える．