Construir una prueba de que un sistema criptográfico es seguro es una tarea inherentemente creativa y compleja; sin embargo, no hay una razón esencial para que su verificación también lo sea. Ante el incremento en la complejidad (y cantidad) de las pruebas generadas, y con el objetivo de facilitar su verificación, algunos criptógrafos han propuesto estructurar las pruebas en forma de secuencias de juegos. En una prueba típica, se parte de un juego inicial donde participan un adversario y un retador, y la probabilidad de ganar del adversario se relaciona con la probablidad de violar la propiedad de seguridad del sistema que se quiere establecer. Este juego inicial se transforma paso a paso, preservando (o aumentando) la probabilidad de que el adversario gane, hasta alcanzar un juego en el cual se puede acotar esta probabilidad. La mayor ventaja de este método radica en que al representar los juegos como programas en un lenguaje probabilístico, ciertas transformaciones corresponden a optimizaciones de programas bien estudiadas en el área de compiladores, mientras que la formulación de otras y la prueba de su corrección puede mecanizarse mas fácilmente. En esta disertación se describirá brevemente un marco, dentro del asistente de pruebas Coq, que permite construir y verificar pruebas criptográficas basadas en juegos.