Formal Verification of NTRUEncrypt Scheme
Gholam Reza Moghissi, Ali Payandeh · International Journal of Computer Network and Information Security · 2016
In this paper we explore a mechanized verification of the NTRUEncrypt scheme, with the formal proof system Isabelle/HOL.More precisely, the functional correctness of this algorithm, in its reduced form, is formally verified with computer support.We show that this scheme is correct what is a necessary condition for the usefulness of any cryptographic encryption scheme.Besides, we present a convenient and application specific formalization of the NTRUEncrypt scheme in the Isabelle/HOL system that can be used in further study around the functional and security analysis of NTRUEncrypt family.