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.
展开▼
