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.