Uma história de dois modelos: Verificação formal de KEMTLS via Tamarin

Resumo

KEMTLS é uma proposta para alterar o handshake do TLS para autenticar o handshake usando chaves de mecanismo de encapsulação de chave de longo prazo em vez de assinaturas, motivada por compensações nas características dos algoritmos pós-quânticos. Provas anteriores de segurança de KEMTLS e sua variante KEMTLS-PDK foram provas manuscritas no modelo reductionista sob suposições computacionais. Neste artigo de pesquisa, apresentamos análises simbólicas verificadas por computador de KEMTLS e KEMTLS-PDK usando dois modelos Tamarin distintos. Na primeira análise, adaptamos o modelo Tamarin detalhado do TLS 1.3 por Cremers et al. (ACM CCS 2017), que segue de perto o formato de fio da especificação do protocolo, para KEMTLS(-PDK). Mostramos que KEMTLS(-PDK) tem as mesmas propriedades de segurança que o TLS 1.3 neste modelo. Fomos capazes de automatizar completamente esta prova Tamarin, em comparação com o modelo Tamarin anterior do TLS 1.3, que exigiu um grande esforço manual de comprovação; também descobrimos algumas inconsistências no modelo anterior. Na segunda análise, apresentamos um novo modelo Tamarin de KEMTLS(-PDK), que segue de perto o modelo de segurança de troca de chaves em múltiplas etapas a partir de provas anteriores de KEMTLS(-PDK) feitas à mão. A segunda abordagem está mais distante do formato de fio da especificação do protocolo, mas captura mais sutilezas nas definições de segurança, como negabilidade e diferentes níveis de segredo para frente; também identifica alguns erros nas afirmações de segurança das provas feitas à mão. Nossos resultados de segurança positivos aumentam a confiança no design de KEMTLS(-PDK). Além disso, ver esses modelos lado a lado nos permite comentar sobre a compensação na análise simbólica entre detalhe na especificação do protocolo e granularidade das propriedades de segurança.