Uma Análise Simbólica da Privacidade para o TLS 1.3 com Encrypted Client Hello

Resumo

TLS 1.3, a nova versão do protocolo de Segurança da Camada de Transporte (TLS), fornece fortes garantias de autenticação e confidencialidade que foram amplamente analisadas em uma variedade de modelos formais. No entanto, apesar de seu uso controverso da criptografia de metadados de handshake, as garantias de privacidade do TLS 1.3 permanecem fracas e mal compreendidas. Por exemplo, o protocolo revela a identidade do servidor-alvo aos atacantes de rede, permitindo a vigilância passiva e a censura ativa das conexões TLS. Para fechar essa lacuna, o grupo de trabalho TLS da IETF está padronizando uma nova extensão de privacidade chamada Encrypted Client Hello (ECH, anteriormente chamada ESNI), mas a ausência de um modelo de privacidade formal torna difícil verificar se essa extensão funciona. De fato, várias versões iniciais do ECH foram encontradas vulneráveis a ataques de rede ativos. Neste artigo de pesquisa, apresentamos a primeira análise formal mecanizada de propriedades de privacidade para o handshake do TLS 1.3. Estudamos todos os modos padrão do TLS 1.3, com e sem ECH, usando o analisador de protocolo simbólico ProVerif. Discutimos ataques ao ECH, alguns encontrados durante o curso deste estudo, e mostramos como eles são considerados na versão mais recente. Nossa análise ajudou a orientar o processo de padronização para o ECH e fornecemos recomendações concretas de privacidade para implementadores do TLS. Além disso, contribuímos com o modelo mais abrangente do TLS 1.3 até o momento, que pode ser usado por designers experimentando com novas extensões do protocolo. O nosso é um dos maiores provas de privacidade tentados usando uma ferramenta de verificação automática e pode ser de interesse geral para analistas de protocolos.