The project aims to formally analyse post-quantum cryptographic protocols by focusing on lattice-based and code-based. To the best of our knowledge, there needs to be more known formal analyses for these protocols. Moreover, it's known that formal analysis of post-quantum cryptosystems has yet to be studied deeply. In the project's scope, we will use Maude, and its based tool Maude-NPA, to analyse postquantum cryptographic protocols. The methods used in the project are based on studying search and decision problems and different interpretations of algebraic techniques. We will adopt these methodologies to encode and (semi)-automatically analyse post-quantum cryptosystems in Maude frameworks and in an extended Maude-NPA version.
The project's scope is to formally reason and develop ideas around Protocol Dialects. For this purpose, we use the high-performance language Maude. Protocol Dialects are generic protocol transformations that add security to protocols in a lightweight manner. The transformations used by dialects are called Lingos, and these are defined in a parametric and general manner to allow composability, a desirable notion for Lingos to obtain stronger security notions. These qualities make Protocol Dialects perfect for resource-constrained devices, for example, IoT devices and the MQTT protocol. The first publication is available in ESORICS 2023 [PDF].