International Journal of Computer Network and Information Security (IJCNIS)
IJCNIS Vol. 8, No. 4, 8 Apr. 2016
Cover page and Table of Contents: PDF (size: 631KB)
Author(s)
Index Terms
Public key encryption, Lattice, NTRUEncrypt, Formal proof system, Higher order logic, Formal verification, Isabelle/HOL, Theorem proving, Proof assistant
Abstract
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.
Cite This Paper
Gholam Reza Moghissi, Ali Payandeh, "Formal Verification of NTRUEncrypt Scheme", International Journal of Computer Network and Information Security(IJCNIS), Vol.8, No.4, pp.44-55, 2016. DOI:10.5815/ijcnis.2016.04.06
Reference
[1]Hoffstein, J., Pipher, J., Silverman, J.H., "NTRU: A ring-based public key cryptosystem", Lecture Notes in Computer Science, 1998.
[2]Bernstein, D.J., "Post-Quantum Cryptography", Department of Computer Science, University of Illinois at Chicago, 2008.
[3]Silverman, J.H., Whyte, W., "Estimating decryption failure probabilities for NTRUEncrypt", Technical report, NTRU Cryptosystems, Report #018, version 1, available at http://www.ntru.com, 2003.
[4]Kaiser, M., Buchmann, J., "Formal Analysis of a Public-Key Algorithm", International Journal of Computer Science 2.2, 2007.
[5]Kusch, S., Buchmann, J., "Formalizing the DSA Signature Scheme in Isabelle/ HOL", Diplomarbeit, Technische Universit¨at Darmstadt, 2007.
[6]Kusch, S., Kaiser, M., "A Computer Proven Application of the Discrete Logarithm Problem", International Journal of Computer Science 2.2, 2007.
[7]Nipkow, T., Paulson, L.C., Wenzel, M., "Isabelle/HOL—a proof assistant for higher-order logic", Lecture Notes in Computer Science, vol. 2283. Springer, 2002. doi:10.1007/3-540-45949-9.
[8]Nipkow, T., Klein, G., "Concrete Semantics-A Proof Assistant Approach", Springer, 2014.
[9]Nipkow, T., "Programming and Proving in Isabelle/HOL", http://isabelle.informatik.tu-muenchen.de/, 2012.
[10]Wenzel, M., "The Isabelle/Isar Reference Manual", TU MÄunchen, MÄunchen, 1999, http://isabelle.in.tum.de/doc/isar-ref.pdf.
[11]Holzl, J., "Proving Real-Valued Inequalities by Computation in Isabelle/HOL", Diploma thesis, Institut f¨ur Informatik, Technische Universit¨at M¨unchen, 2009.
[12]"IEEE P1363.1. Public-key cryptographic techniques based on hard problems over lattices", http://grouper.ieee.org/groups/1363/lattPK/index.html, Accessed May 31, 2014.
[13]Hoffstein, J., Howgrave-Graham, N., Pipher, J., Silverman, J.H., Whyte, W., "Hybrid lattice reduction and meet in the middle resistant parameter selection for ntruencrypt", NTRU Cryptosystems, Inc., Acton, MA, Tech. Rep., 2007.
[14]Ballarin, C., "Tutorial to locales and locale interpretation", In L. Lambán, A. Romero, and J. Rubio, editors, Contribuciones Científicas en honor de Mirian Andrés Gómez. Servicio de Publicaciones de la Universidad de La Rioja, Logroño, Spain, 2010.
[15]Mallagaray, J.D., "Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL", Universidad de La Rioja, 2011/2012, http://www.unirioja.es/cu/jodivaso/degree_thesis/.
[16]Security Innovation, https://www.securityinnovation.com/. Accessed August 9, 2013.
[17]Nipkow, T., "What's in Main", Isabelle TUM, 2013, http://isabelle.in.tum.de/doc/main.pdf.
[18]Krauss, A., "Defining Recursive Functions in Isabelle/HOL", Isabelle TUM, 2008, http://isabelle.in.tum.de/documentation.html.
[19]Sternagel, C., Thiemann, R., "Executable matrix operations on matrices of arbitrary dimensions", Archive of Formal Proofs, 2010.
[20]Lindenberg, C., Wirt, K., Buchmann, J., "Formal proof for the correctness of RSA-PSS", IACR Cryptology ePrint Archive 2006, 11.
[21]Silverman, J.H., "An Introduction to the Theory of Lattices and Applications to Cryptography", Computational Number Theory and Applications to Cryptography, University of Wyoming, 2006.
[22]Isabelle-TUM, https://isabelle.in.tum.de/(2013). Accessed December ?05, ?2013.
[23]Appel, A.W., "Verification of a Cryptographic Primitive: SHA-256", ACM Transactions on Programming Languages and Systems (TOPLAS), Princeton University, 2015.