Por que provas informais não são suficientes

Os projetistas de protocolos produzem regularmente argumentos informais de segurança — raciocínios em prosa sobre por que um invasor não pode ter sucesso. A história mostra que esses argumentos frequentemente estão errados, mesmo quando os protocolos são projetados por especialistas.

O Needham-Schroeder (1978) foi projetado para autenticação mútua. Em 1995, Gavin Lowe encontrou um ataque de intermediário usando verificação automatizada — 17 anos após a publicação. A prova informal não detectou uma sutil repetição de mensagens.

O WEP foi aprovado pelo IEEE em 1997 com alegações informais de segurança. Em 2001, pesquisadores encontraram reutilização do fluxo de chaves RC4, colisões de IV e ausência de integridade — comprometendo-o em minutos. O raciocínio informal não detectou nada disso.

A segurança de protocolos depende das interações entre muitas sessões simultâneas, invasores ativos e suposições criptográficas. O raciocínio humano tem dificuldade com explosões de estados e execuções simultâneas intercaladas.

Os métodos formais modelam matematicamente o protocolo e comprovam — ou refutam — propriedades de segurança (sigilo, autenticação e sigilo futuro) para todas as estratégias possíveis do invasor, não apenas para aquelas consideradas pelo projetista.

Simbólico (Dolev-Yao): a criptografia é uma caixa-preta perfeita; o foco está na lógica do protocolo. Computacional: jogos de segurança probabilísticos reais; mais próximo das garantias do mundo real. Ambos detectam erros reais.

O POODLE (2014) explorou um oráculo de preenchimento no CBC do SSL 3.0. A vulnerabilidade era uma falha de projeto no nível do protocolo, não um erro de implementação. A análise formal da especificação do SSL 3.0 teria sinalizado o oráculo antes da implantação.

O TLS 1.3 (RFC 8446) foi projetado em conjunto com análises formais usando ProVerif e miTLS. A especificação foi iterada com base nas descobertas formais — um marco na adoção de métodos formais por organizações de padronização.

As ferramentas formais verificam o modelo do protocolo, não a implementação. Um protocolo verificado formalmente ainda pode ter uma implementação insegura. F* / HACL* amplia a verificação para o próprio código criptográfico.

A verificação formal é cara: a modelagem do protocolo leva semanas e exige conhecimento especializado. Mas, para alvos de alto valor (TLS, SSH, Signal), o custo é justificável — uma única falha de protocolo pode afetar bilhões de usuários.

O que tornou significativa a descoberta de Lowe, em 1995, sobre o ataque ao Needham-Schroeder?

As provas informais falham porque o raciocínio humano não detecta as interações entre sessões simultâneas e as estratégias dos invasores. Needham-Schroeder, WEP e POODLE tinham argumentos informais de segurança. O TLS 1.3 incorporou análise formal durante o projeto. As ferramentas formais detectam erros no nível do protocolo antes da implantação.