Personal tools
You are here: Home Personal J. Alberto Verdejo López Eventos Conferencia: Pruebas Formales de Criptografia Usando Secuencias de Juegos
Document Actions

Conferencia: Pruebas Formales de Criptografia Usando Secuencias de Juegos

What
When 2007-11-12
from 17:00 to 18:30
Where Facultad de Informatica - UPM
by J. Alberto Verdejo López last modified 2007-11-09 10:14

Pruebas Formales de Criptografia Usando Secuencias de Juegos Gilles Barthe INRIA Facultad de Informatica - UPM Campus de Montegancedo Lunes, 12 de noviembre, 17:00 Hemiciclo 1001

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.

Powered by Plone CMS, the Open Source Content Management System

This site conforms to the following standards: