Análisis simbólico de la privacidad para TLS 1.3 con Encrypted Client Hello

Resumen

TLS 1.3, la versión más reciente del protocolo de seguridad de capa de transporte (TLS), proporciona garantías de autenticación y confidencialidad sólidas que han sido analizados de forma exhaustiva en una variedad de modelos formales. Sin embargo, a pesar de su uso controvertido del cifrado de metadatos de protocolo de enlace, las garantías de privacidad de TLS 1.3 siguen siendo débiles y poco entendidas. Por ejemplo, el protocolo revela la identidad del servidor destino a los atacantes de la red, lo que permite la vigilancia pasiva y la censura activa de las conexiones TLS. Para cerrar esta brecha, el grupo de trabajo TLS de la IETF está estandarizando una nueva extensión de privacidad llamada Encrypted Client Hello (ECH, anteriormente llamada ESNI), pero la ausencia de un modelo de privacidad formal hace que sea difícil verificar que esta extensión funcione. De hecho, varios borradores iniciales de ECH se encontraron vulnerables a ataques de red activos. En este artículo de investigación, presentamos el primer análisis formal mecanizado de propiedades de privacidad para el protocolo de enlace de TLS 1.3. Estudiamos todos los modos estándar de TLS 1.3, con y sin ECH, utilizando el analizador de protocolos simbólicos ProVerif. Discutimos ataques a ECH, algunos de los cuales se encontraron durante el curso de este estudio, y mostramos cómo se tienen en cuenta en la última versión. Nuestro análisis ha ayudado a guiar el proceso de estandarización para ECH y proporcionamos recomendaciones concretas de privacidad para los implementadores de TLS. También contribuimos con el modelo más completo de TLS 1.3 hasta la fecha, que puede ser utilizado por diseñadores que experimentan con nuevas extensiones del protocolo. Nuestro análisis es uno de los intentos de pruebas de privacidad más grandes utilizando una herramienta de verificación automatizada y puede ser de interés general para los analistas de protocolos.