Machine checked proofs for MLWE based encryption using EasyCrypt

Abstract

Med den truende faren til kvantedatamaskiner trenger vi offentlig nøkkel-kryptografi som ikke avhenger av diskret logaritme-problemet og andre problemer som kan løses effektivt på kvantedatamaskiner. En fremgangsmåte er å basere kryptografien på gitterproblemer. Vi definerer et kryptosystem og beviser det sikkert med gitterbaserte antakelser. For ekstra sikkerhet gjør vi dette i et verktøy kalt EasyCrypt, som lar datamaskinen sjekke bevisene dine. For å muliggjøre dette utvikler vi også et nytt matrisebibliotek til EasyCrypt som støtter matriser med dynamisk størrelse.

With the looming threat of quantum computing we need public key cryptography that does not rely on the discrete log problem and other problems that can be solved effciently on a quantum computer. One approach is to base the cryptography on lattice problems. We define a cryptosystem and prove it secure under lattice based assumptions. For additional assurance we do so using a tool called EasyCrypt, which lets the computer check the validity of your proof. To make this possible we also develop a new matrix library for EasyCrypt that can support dynamically sized matrices.