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.
• 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
• Examples (NTRU, MaTRU)
• Case studies
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.
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).