Análisis formal de protocolos criptográficos

En la actualidad cada vez enviamos una mayor cantidad de información a través de Internet, y cada vez esta ésta es de carácter más confidencial y sensible. Por esa razón, cada vez se utilizan protocolos criptográficos de comunicación más sofisticados en los que se cifra la información transmitida de modo que pueda garantizarse su confidencialidad y, así, evitar que un participante con intenciones deshonestas pueda averiguar información que no debería saber. Sin embargo, a pesar de todas estas medidas de seguridad, los ataques de seguridad en los que se roban datos sensibles como números de tarjetas de crédito (como los sufridos por Sony) o contraseñas de cuentas son frecuentes.

El problema radica en la dificultad de depurar los protocolos criptográficos que se desarrollan, y más teniendo en cuenta que su complejidad va en aumento. Para evitar agujeros de seguridad en la definición de un protocolo criptográfico se pueden seguir algunas buenas prácticas basadas en errores de seguridad ya conocidos o efectuar pruebas una vez se haya implementado ya el protocolo. Sin embargo, con estos métodos resulta difícil garantizar al 100% la seguridad de un protocolo criptográfico o si hay un fallo en el diseño del protocolo pero éste se descubre una vez ya implementado el protocolo, se habrá perdido tiempo y dinero.