un relato de dos modelos: verificación formal de KEMTLS vía Tamarin

Resumen

KEMTLS es una propuesta para cambiar el protocolo de enlace de TLS para autenticar el protocolo de enlace utilizando claves de mecanismo de encapsulación de claves a largo plazo en lugar de firmas, motivada por compensaciones en las características de los algoritmos post-cuánticos. Las pruebas de seguridad anteriores de KEMTLS y su variante KEMTLS-PDK han sido pruebas manuscritas en el modelo reduccionista bajo suposiciones computacionales. En este artículo de investigación, presentamos análisis simbólicos verificados por ordenador de KEMTLS y KEMTLS-PDK utilizando dos modelos Tamarin distintos. En el primer análisis, adaptamos el detallado modelo Tamarin de TLS 1.3 de Cremers et al. (ACM CCS 2017), que sigue de cerca el formato de cable de la especificación del protocolo, a KEMTLS(-PDK). Mostramos que KEMTLS(-PDK) tiene las mismas propiedades de seguridad que TLS 1.3 en este modelo. Fuimos capaces de automatizar completamente esta prueba Tamarin, en comparación con el modelo Tamarin anterior de TLS 1.3, que requirió un gran esfuerzo de prueba manual; también descubrimos algunas inconsistencias en el modelo anterior. En el segundo análisis, presentamos un modelo Tamarin novedoso de KEMTLS(-PDK), que sigue de cerca el modelo de seguridad de intercambio de claves multietapa de las pruebas de KEMTLS(-PDK) anteriores con papel y lápiz. El segundo enfoque está más alejado del formato de cable de la especificación del protocolo, pero captura más matices en las definiciones de seguridad, como la negabilidad y diferentes niveles de confidencialidad hacia adelante; también identifica algunos errores en las afirmaciones de seguridad de las pruebas con papel y lápiz. Nuestros resultados de seguridad positivos aumentan la confianza en el diseño de KEMTLS(-PDK). Además, ver estos modelos uno al lado del otro nos permite comentar sobre la compensación en el análisis simbólico entre el detalle en la especificación del protocolo y la granularidad de las propiedades de seguridad.