Formal verification of Hybrid Post-Quantum TLS protocol

This project provides a formal verification of the Hybrid Post-Quantum TLS protocol using the Maude-NPA tool. Maude-NPA is a tool written in Maude for analyzing cryptographic protocols.

Prerequisites

• Maude-NPA

Installation

1. Download and install Maude-NPA from the official website.
2. Download and move hybridpqtls.maude to the maude-npa directory.

Usage

1. Open a terminal and navigate to the maude-npa directory.
2. Start Maude by running the following command:

   maude

3. Load the maude-npa.maude file:

   load maude-npa.maude

4. Load the hybridpqtls.maude file:

   load hybridpqtls.maude

   If hybridpqtls.maude is located in a different directory, provide the full path to the file:

   load /path/to/hybridpqtls.maude

5. Use the Maude-NPA commands to test the protocol.