Prueba formal de algoritmos de firma digital y sus implementaciones usando asistentes de pruebas

La criptografía juega un papel fundamental en el desarrollo de software seguro. Sin embargo, la tarea de diseñar primitivas criptográficas correctas y forzar su correcto uso en la práctica ha sido una tarea extremadamente difícil. La historia de la criptografía está llena de ejemplos de primitivas y protocolos inseguros de amplio uso general. Varios formalismos se han presentado en la literatura para probar con lápiz y papel la correctitud de primitivas criptográficas. Sin embargo, estas “pruebas” no son verificables en la práctica y los criptógrafos han buscado técnicas que puedan simplificar la complejidad de dichas pruebas. Una forma muy popular a este respecto está basada en el uso de Teoría de Juegos. En este caso, las pruebas se estructuran como una secuencia de juegos y en los cuales pruebas intermedias establecen la validez de la transición entre juegos sucesivos.

Técnicas basadas en generación de código ejecutable son un ejemplo particular de estas técnicas basadas en teorìa de juegos. Estas técnicas tienen una vision de los juegos centrada en código ejecutable y se fundamentan en la teoría de los lenguajes de programación para justificar los pasos de las pruebas. Sin embargo, si bien estas técnicas contribuyen a formalizar de una manera precisa las premisas de seguridad a probar y además permiten de realizar pruebas de una manera sistemática, las pruebas son demasiado largas y complicadas. Por tal motivo, métodos de verificación formal son necesarias para llegar a un alto grado de confianza en las pruebas. La biblioteca de rutinas CertiCrypt permite verificar formalmente este tipo de pruebas en Coq. Ha sido usada para probar la seguridad semántica de diversos algoritmos de encriptación y de primitivas de firma digital (como ElGamal, Hashed-ElGamal, OAEP, FDH). El objetivo del proyecto es presentar pruebas completamente verificadas de al menos una de las presentadas en la literatura (muy probablemente Skein presentado por Schneier et al). Esta verificación va a permitir establecer que este algoritmos y su implementacion satisface propiedades relevantes de funciones de hash: resistencia a las pre-imágenes, resistencia a las colisiones, resistencia a pre-imágenes secundarias y propiedades pseudoaleatorias.