Aes

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

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.

Continuar leyendo