UAFVerif - A formal verification tool to analyze the FIDO UAF protocol

This is the source code repo for UAFVerif, UAFVerif+, and AutoMinAs. UAFVerif and UAFVerif+ are formal verification tools to analyze the FIDO UAF protocol. And AutoMinAs is a tool to automatically identify the minimal assumptions for any given 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 entitled "A formal analysis of the FIDO UAF protocol" in The Network and Distributed System Security Symposium 2021 (NDSS). If you want to cite our paper in your work, please use the following BibTeX entry.

@inproceedings{UAFAnalysis2021,
  title={A formal analysis of the FIDO UAF protocol},
  author={Feng, Haonan and Li, Hui and Pan, Xuesong and Zhao, Ziming},
  booktitle={Proceedings of the Network and Distributed System Security Symposium (NDSS)},
  year={2021}
}

The project is still being updated, with the tag version_1.0 corresponding to the NDSS paper, and the tag version_2.0 corresponding to the TDSC submission.

Instructions

Software Requirements

To run UAFVerif and UAFVerif+, you need ProVerif 2.01+ and Python 3.0+ (to batch ProVerif input file.).

File Organization

Source code files:

for NDSS Version (tagged version_1.0)

UAFVerif.pv: a python script to analyze the UAF protocol in batches and output the results.
UAF.pvl: a lib file that contains all operations of the UAF 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.

for TDSC Submission (tagged version_2.0)

UAFVerif+.pv: a python script to analyze the UAF protocol with a more detail model in batches and output the results.
UAF+.pvl: a lib file that contains all operations of the UAF protocol, including the seperation of WS and US, and with AppID or not.
Content.py: a python file with the Classes to control the contents of .pv file for different scenarios
Definition.py: a python file with the Classes to define
AutoMinAs.py: a python script to automatically obtain the minimal assumptions for a given protocol taking the protocol process, security assumptions, and security properties as inputs.

User input files:

for the tool AutoMinAs of TDSC Submission

Src/Assumptions: the full name and abbreviations for the assumptions of this protocol.
- Full names are events corresponding to data fields leakage
- Abbreviations are acronyms for each event
- The inputs should follow the format: full_name, abbr
Src/Process: the ProVerif codes of protocol processes.
- If there are multiple scenarios of the protocol to be analyzed, a single .pv file is required for each scenario.
- The name of the .pv file should be the name of this scenario.
Src/Queries: the secrecy queries and authentication queries of each protocol scenario.
- The queries of security properties for each scenario should be placed in a subdirectory with the same name of .pv file.
- The the authentication queries are put in the first file in the subdirectory, and the secrecy queries are put in the second file.
- The inputs should follow the format: name_of_query|head_of_query|body_of_query

Generated files:

for NDSS Version (tagged version_1.0)

LOG/xxx.log: a log file.
result/: the directory to store all analysis results.
TEMP/TEMP--xxxxxxx.pv: a temporary file generated by the UAFVerif.pv for ProVerif to analyze a specific case.

for TDSC Submission (tagged version_2.0)

ERROR/Auth_xxxx_error.pv or Reg_xxxx_error.pv: record cases where the results were not correctly obtained.
LOG/Auth_xxx.log, Reg_xxx.log, FINAL_RESULT.log: a log file for a specific Authentication or Registration case, or the final result.
QUERY/Auth_xxxx.pv or Reg_xxxx.pv: a temporary .pv file generated for ProVerif to analyze a specific Authentication or Registration case.

Verify the confidentiality and authentication goals

for NDSS Version (tagged version_1.0) With a large number of input cases, we use a python script to batch analyze (UAFVerif.py). You can run the script without arguments and analyze confidentiality and authentication objectives in all cases.

PROJECTROOTDIR> python UAFVerif.py

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

"reg" represents the registration process.
"auth_1b_em" represents the authentication process for 1B authentication in login phase.
"auth_1b_st" represents the authentication process for 1B authentication in step-up authentication phase.
"auth_1r_em" represents the authentication process for 1R authentication in login phase.
"auth_1r_st" represents the authentication process for 1R authentication in step-up authentication phase.
"auth_2b" represents the authentication process for 2B authentication in step-up authentication phase.
"auth_2r" represents the authentication process for 2R authentication in step-up authentication phase.

PROJECTROOTDIR> python UAFVerif.py -t reg 
PROJECTROOTDIR> python UAFVerif.py -t auth_1b_em 
PROJECTROOTDIR> python UAFVerif.py -t auth_1b_st 
PROJECTROOTDIR> python UAFVerif.py -t auth_1r_em 
PROJECTROOTDIR> python UAFVerif.py -t auth_1r_st 
PROJECTROOTDIR> python UAFVerif.py -t auth_2b 
PROJECTROOTDIR> python UAFVerif.py -t auth_2r

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 script/script.py -s

Use -h/-help to get help informations.

PROJECTROOTDIR> python UAFVerif.py -h

After running the script, you can find the result in result folder. The results are classified by folder, for example, "../result/reg/autr_1b/S-ak" contains the result of the confidentiality of the ak in registration process, 1B authenticator scene. Then the files shows the minimal assumptions of this result, for example "34 reg true type autr_1b query S-ak fields-1 mali-6 ,0,1,2,3,4,7" means we found a minimal assumptions, where one data field can be compromised and 6 malicious entities can exist. Opening this file, you can find which fields can be compromised and which malicious entities are exist to let the protocol satisfies the security goal.

Also, there would be the log files which record all the analysis procedure.

for TDSC Submission (tagged version_2.0) With a large number of input cases, we use a python script to batch analyze (UAFVerif+.py). You can run the script without arguments and analyze confidentiality and authentication goals in all cases.

PROJECTROOTDIR> python UAFVerif+.py

for AutoMinAs With a all combinations of assumptions to be analyzed in each input cases, we use a python script to batch analyze (AutoMinAs). You can run the script without arguments and analyze confidentiality and authentication goals in all cases with different combinations of assumptions.

PROJECTROOTDIR> python AutoMinAs.py

Verify the unlinkability goals

Go to the rootpath, and run following command.

PROJECTROOTDIR> proverif -lib "FIDO.pvl" reg_unlink.pv" or "proverif -lib "UAF.pvl" reg_unlink.pv
PROJECTROOTDIR> proverif -lib "FIDO.pvl" reg_unlink.pv" or "proverif -lib "UAF.pvl" auth_unlink.pv