Hacia la especificación y verificación formal de algoritmos criptográficos : Mini-AES certificado

Abstract

El algoritmo de encriptación de información AES (Advanced Encryption Standard) es un estándar internacional ampliamente utilizado tanto por gobiernos como comercialmente; por lo tanto resulta de importancia crítica garantizar el correcto comportamiento de sus distintas implementaciones. Existe una versión simplificada del algoritmo, llamada Mini-AES, que fue creada con fines académicos pero sin perder la esencia de su funcionamiento y sus propiedades criptográficas. En este trabajo se define un lenguaje de programación imperativa, se implementa Mini-AES sobre el mismo y se demuestra formalmente que su comportamiento es el deseado, esto es, que los procedimientos de encriptar y desencriptar son inversos. El lenguaje de programación en el cual se define el algoritmo Mini-AES se formaliza en el asistente de pruebas Coq, que es utilizado también para desarrollar pruebas sobre el comportamiento de dicho algoritmo, utilizando lógica de Hoare. Se presenta entonces una especificación formal del algoritmo Mini-AES junto con su correspondiente implementación funcionalmente correcta.