X-Men: A Mutation-Based Approach for the Formal Analysis of Security Ceremonies
Table of Contents
There is an increasing number of cyber-systems (e.g., systems for payment, transportation, voting, critical infrastructures) whose security depends intrinsically on human users. A security ceremony expands a security protocol with everything that is considered out-of-band to it, including, in particular, the mistakes that human users might make when participating actively in the security ceremony.
Our approach defines mutation rules that model possible behaviors of a human user, and automatically generates mutations in the behavior of the other agents of the ceremony to match the human-induced mutations. This allows for the analysis of the original ceremony specification and its possible mutations, which may include the way in which the ceremony has actually been implemented. To automate our approach, we have developed the tool X-Men, which is a prototype that extends Tamarin, one of the most common tools for the automatic unbounded verification of security protocols. As a proof of concept, we have applied our approach to three real-life case studies, uncovering a number of concrete vulnerabilities.
This section list any major frameworks/libraries used to bootstrap the project.
This is how you can set up the project locally. To get a local copy up and running follow these simple example steps.
-
Java 13 or greater
https://www.oracle.com/java/technologies/javase/jdk13-archive-downloads.html
-
Python 3.9.10
https://www.python.org/downloads/release/python-3910/
Python is using the following modules:
- os
- fileinput
- ntpath
- subprocess
- sys
- glob
- shutil
- csv
- tqdm
- argparse
-
Tamarin
https://tamarin-prover.github.io/manual/book/002_installation.html
Please follow the instruction below on how to run the X-Men tool:
-
Be sure that Java, Python and Tamarin are correctly installed on your machine.
-
Download the project folder on your machine.
-
Open a terminal and go to the folder which cointains the wolverine.py file
-
Execute wolverine.py using:
python3 wolverine.py
-
Select one of the models you can find in the Models folder. You can choose between:
- Oyster.spthy
- SSO.spthy
- CoachService.spthy
The python script splits the model in three files: (filename_pre.spthy, filename.spthy and filename_post.spthy)
-
X-Men opens.
-
Click on "Click here to upload a model" icon and select the filename.spthy file just created by wolverine (do not consider filename_pre.spthy nor filename_post.spthy).
-
Once the model is uploaded, go in the option tab in X-Men which now is enabled.
-
Select the mutation you want to apply.
-
Go back to the previous tab and click on the icon to generate the mutated models.
-
Click on the closure button on top of X-Men to close the tool.
-
Wolverine resumes the work merging the previous splitted file with the mutated models.
-
Wolverine executes Tamarin for each of the mutated model generating a file report.csv which contains the mutated models which security properties are now falsified.
Tamarin uses C-style comments, so everything between /* and */ or the line following // is a comment. We take advantage of comments in the X-Men framework to divide the internal structure of the models in three sections as shown here:
/MODEL/
theory theory_name
begin
/* Channel rules */
/RULES/
builtins: ...
functions: ...
/* Protocol/Ceremony Rules */
/ENDOFRULES/
/* Restrictions and Lemmas */
end
/ENDOFMODEL/
The comments /MODEL/ and /ENDOFMODEL/ set the boundaries of the entire file. Within these boundaries, there are:
- \item an inner bound (from /MODEL/ to /RULES/) where the channel rules are defined;
- \item an inner bound (from /RULES/ to /ENDOFRULES/) where functions and the ceremony rules are defined;
- \item an inner bound (from /ENDOFRULES/ to /ENDOFMODEL/) where the restrictions and the lemmas are defined.