Especificación Formal de Protocolos Criptográficos en Cálculo de Situaciones
José Hernández-Orallo, Javier Pinto
Novatica nº34, jul-ago 1998
Resumen
Presentamos un modelo genérico en Cálculo de Situaciones (C.S.) para formalizar protocolos criptográficos. Se distingue de otras lógicas para la modelización criptográfica que usan los conceptos de creencia o secreto porque nuestra propuesta está basada en el concepto de conocimiento y no es necesaria ninguna construcción adicional fuera del C.S. Como muestra, presentamos la especificación formal del protocolo de autentificación del ISO/IEC 9798-2 y se ilustra cómo demostrar diferentes propiedades de corrección sobre él.
A la vista de una posible automatización de las demostraciones, el resultado más prometedor hasta ahora es que la especificación de los protocolos se mantiene de una manera extremadamente clara y explícita, facilitando la tarea de diseño y verificación, y permitiendo una implementación directa.
Tornar a la plana major.
© 1996-1997 José Hernández Orallo.