FIDO2Verif - A formal verification tool to analyze the FIDO2 protocol

This is the source code repo for FIDO2Verif, a formal verification tool to analyze the FIDO2 protocol. This instruction describes the organization of the source code and how to use it. The results generated by this tool was published in the paper titled "A Formal Analysis of the FIDO2 Protocols" in European Symposium on Research in Computer Security 2022 (ESORICS). If you want to cite our paper in your work, please use the following BibTeX entry.

@inproceedings{FIDO2Analysis2022,
  title={A Formal Analysis of the FIDO2 Protocols},
  author={Guan, Jingjing and Li, Hui and Ye, Haisong and Zhao, Ziming},
  booktitle={Proceedings of the European Symposium on Research in Computer Security (ESORICS)},
  year={2022}
}

The tag version_1.0 corresponds to the ESORICS paper.

Instructions

Software Requirements

To run FIDO2Verif, you need ProVerif 2.01+ and Python 3.0+ (to batch ProVerif input file.). Before running the tool, you should unzip the ProVerif folder and copy the "proverif.exe" to the same directory of python script, and ensure that the rootpath of this project does not contain special characters like blanks " ".

File Organization

Source code files:

• FIDO2Verif.pv: a python script to analyze the FIDO2 protocol in batches and output the results.
• FIDO2.pvl: a lib file that models all operations of the FIDO2 protocol.
• Reg.pv: registration process to analyze confidentiality and authentication goals.
• Reg_unlink.pv: registration process to analyze unlinkability goals.
• Auth.pv: authentication process to analyze confidentiality and authentication goals.
• Auth_unlink.pv: authentication process to analyze unlinkability goals.
• Auth_A3_A4.pv: authentication process to analyze leak resilience goals.

Generated files:

• LOG/xxx.log: a log file with the results of all the cases.
• Result/: the directory to store the cases satisfying the properties.
• TEMP/TEMP--xxxxxxx.pv: a temporary file generated by the FIDO2Verif.pv for ProVerif to analyze a specific test case.

Verify the confidentiality and authentication goals

We use a python script to automatically generate the .pv files of all possible cases for batch analysis (FIDO2Verif.py). You can run the script without arguments and analyze confidentiality and authentication objectives in all cases.

PROJECTROOTDIR> python FIDO2Verif.py

Or you can run the script with -t/-target to specific which process you want to analyze.

• "reg_client" represents registration process with client-side storage authenticators.
• "reg_server" represents registration process with server-side storage authenticators.
• "auth_client_em" represents authentication process with client-side storage authenticators.
• "auth_client_sim" represents simple transaction authorization process with client-side storage authenticators.
• "auth_client_gen" represents generic transaction authorization process with client-side storage authenticators.
• "auth_server_em" represents authentication process with server-side storage authenticators.
• "auth_server_sim" represents simple transaction authorization process with server-side storage authenticators.
• "auth_server_sim" represents generic transaction authorization process with server-side storage authenticators.

PROJECTROOTDIR> python FIDO2Verif.py -t reg_client 
PROJECTROOTDIR> python FIDO2Verif.py -t reg_server 
PROJECTROOTDIR> python FIDO2Verif.py -t auth_client_em 
PROJECTROOTDIR> python FIDO2Verif.py -t auth_client_sim 
PROJECTROOTDIR> python FIDO2Verif.py -t auth_client_gen 
PROJECTROOTDIR> python FIDO2Verif.py -t auth_server_em 
PROJECTROOTDIR> python FIDO2Verif.py -t auth_server_sim 
PROJECTROOTDIR> python FIDO2Verif.py -t auth_server_gen 

Since the analysis will take a long time under a large amount of cases, we give a simplified version by use "-s/-simple".

PROJECTROOTDIR> python FIDO2Verif.py -s

Use -h/-help to get help informations.

PROJECTROOTDIR> python FIDO2Verif.py -h

After running the script, you can find the result in Result folder. The results are classified by folder, for example, "../Result/reg_client/S-creid" contains the result of the confidentiality of CreID in registration process, client-side storage authenticator scene. Then the files shows the minimal assumptions of this result, for example "97 reg_client true type reg_client query S-skatfields-1 6" means that one data field can be compromised and 6 denotes the cases that all the channel are public Dolev-Yao Channel. Opening this file, you can find which fields can be compromised and which channels can be compromised to let the protocol satisfies the security properties.

Also, there would be the log files which record the results for all the cases.

Verify the unlinkability goals

Go to the RootPath, and run following command.

PROJECTROOTDIR> proverif -lib "FIDO2.pvl" Reg_unlink.pv
PROJECTROOTDIR> proverif -lib "FIDO2.pvl" Auth_unlink.pv

Verify the authentication goals A3 and A4

Go to the RootPath, and run following command.

PROJECTROOTDIR> proverif -lib "FIDO2.pvl" Auth_A3_A4.pv

To analyze unlinkability for different modes of CTAP2 process, set the "ctap_type" in .pv file. To analyze unlinkability for different types of authenticator, set the "au_type" in .pv file. To analyze unlinkability for different modes of authentication, set the "tr_type" in .pv file.