This repository stores Maude's system modules that construct the symbolic models of three postquantum cryptography schemes. Specifically, the selected schemes are Key Encapsulation Mechanisms (KEMs). The symbolic modules allow us to perform invariant analysis, find a Man In The Middle (MITM) attack, and model checking of Liveness, Fairness and Security properties. The analyzed KEMs are:
Please check the corresponding publication for further insights on the symbolic specification and verification of Kyber.
For a complete detailed explanation of the framework along with three use cases with the above mechanisms, please see the journal paper of PeerJ Computer Science.
The repository is divided into three main folders, one for each of the specified KEMs. Each folder stores two kinds of files: one txt
file and four maude
files. The txt
file contains basic information and a series of notations on the specified KEM. The maude
files are:
KEM.maude
: Contains the full specification using the framework.KEM-PREDS
&KEM-CHECK
: Contain the necessary modules to perform model checking with Maude.KEM-test.maude
: Stores a series of commands to (i) perform invariant analysis through thesearch
command and (ii) verify three properties with the LTL Model Checker.
where KEM
is either kyber
, bike
or cm
respectively for each selected protocol.
In order to perform invariant analysis and model checking one has to:
- Have Maude 3.3 installed. It can be downloaded from the official download page.
- Download this repository and extract the contents.
- Open a terminal in the parent folder of the downloaded repository.
- Start Maude by following the instructions. Maude can be initiated by running the
./maude.darwin64
- Load a testing file with the command
load KEM-test.maude
, whereKEM
has to be eitherkyber
,bike
orcm
. The code inside testing files will perform the following commands.- Invariant analysis with the
search
commands. - Model checking with the
reduce
commands.
- Invariant analysis with the