FIDO2-formalization

プロトコルファイル

FIDO2_reg.pvl
- FIDO2 register プロトコル
FIDO2_auth.pvl
- FIDO2 authenticate プロトコル
FIDO2_reg_mac.pvl
- FIDO2 register 修正プロトコル

検証用ファイル

register.pv
- register 検証ファイル
authenticate.pv
- authenticate 検証ファイル
authenticate_A3.pv
- authenticate 安全性 A3 検証用
authenticate_A4.pv
- authenticate 安全性 A4 検証用

実行方法

実行例

$ proverif -lib src/register.pvl src/register.pv

-libでプロトコルファイル(.pvl)を指定。実行対象は検証用ファイル(.pv)を用いる。検証用ファイル内のat_type, au_type, ctap_type, tr_typeを変更することで様々なモードを検証できる。