Post-Quantum Cryptosystems and Their Formal Analysis

Assoc. Prof. Dr. Sedat Akleylek, Department of Computer Engineering, Ondokuz Mayıs University, Samsun, Turkey
Dr. Besik Dundua, VIAM, Tbilisi State University, Tblisi, Georgia
Dr. Mikheil Rukhaia, VIAM, Tbilisi State University, Tblisi, Georgia
The aim of this tutorial is to give an insight of post-quantum cryptography focusing lattices and their formal analysis.
There has been increasing demand to post-quantum cryptographic schemes with their security based on the computational hardness of the coding, multivariate, lattice problems and other algebraic structures. Post-quantum cryptographic schemes refer to the algorithms that are resistant to quantum attacks. These are the alternatives of public key cryptographic schemes such as RSA, DLP-based schemes and elliptic curve-based protocols. These schemes have been proposed for public key encryption, signature schemes and hash functions. Post-quantum cryptographic schemes are classified into the following approaches: code-based, hash-based, multivariate and lattice-based cryptography. Lattice-based cryptographic schemes are one of the most widely studied post-quantum cryptographic protocols. The security of these schemes depends on the hardness of lattice problems under some parameters. NTRU is the first proposed lattice-based cryptosystem. It is one of the most thoroughly researched and widely implemented alternative to standard public key cryptosystems. It supports faster encryption and decryption and also it requires small areas. NTRU is standardized and commercialized post-quantum cryptosystem. Thus, its security from the theoretical point of view has been deeply analyzed. In recent years, application of formal methods to the analysis of cryptographic protocols is experiencing a renewed period of growth with the emergence of new concepts and systems that allow a better understanding and usability. Formal analysis of cryptographic protocols is used to model a cryptographic protocol and its security properties to verify that a protocol is secure. In the last decades, such a formal analysis revealed security flaws in some protocols.
In this tutorial, we will introduce post-quantum cryptography with applications in real world. Then, we will focus on lattice- based cryptosystems and their formal analysis with automated softwares. In the security side, we will analyze the methods that are resistant to well-known attacks. We will discuss about how to write a code to analyze lattice-based cryptosystems formally. Also, we will provide some examples by considering NTRU-based cryptosystems.
This tutorial is scheduled for 3 hours (half day). The number of participants is limited to 30.
Outline
• Introduction to post-quantum cryptography
• Lattice-based cryptosystems
• NTRU-based cryptosystems
• Applications of cryptosystems in the areas of communications and network
• Basics of security analysis
• Introduction to formal analysis
• MAUDE
• Examples (NTRU, MaTRU)
• Case studies
Target Audience
This tutorial assumes a basic knowledge of public key cryptographic schemes. It does not cover theoretical mathematics. This tutorial is for the cryptographic protocol designers and software developers from academia and industry.
Acknowledgments
This work is partially supported by the joint research project funded by Shota Rustaveli National Science Foundation of Georgia (SRNSFG, no:04/03) and Scientific and Technological Research Council of Turkey (TÜBİTAK, no:118E312).