O Protocolo Needham-Schroeder e Ataques

O protocolo de Needham-Schroeder (1978) foi uma das primeiras tentativas formais de projetar um protocolo criptográfico de autenticação usando um terceiro confiável (TTP). O objetivo era permitir que duas partes, Alice e Bob, se autenticassem mutuamente e estabelecessem uma chave de sessão compartilhada usando um servidor de autenticação confiável (AS), que compartilha chaves de longo prazo com cada entidade. O protocolo é anterior à infraestrutura de chaves públicas, mas introduziu conceitos — valores únicos para garantir a atualidade e distribuição de chaves por meio de um servidor confiável — que continuam centrais em protocolos modernos como o Kerberos. Entender o NS e suas falhas moldou todo o campo da análise de protocolos.

O protocolo de chave simétrica NS ocorre em cinco etapas. (1) Alice envia {A, B, Na} ao AS, solicitando uma chave de sessão para se comunicar com Bob. (2) O AS responde a Alice com {Na, B, Kab, {Kab, A}_Kb}_Ka — uma chave de sessão Kab e um tíquete para Bob, tudo criptografado com a chave de longo prazo Ka de Alice. (3) Alice encaminha a Bob o tíquete {Kab, A}_Kb. (4) Bob descriptografa o tíquete, extrai Kab e envia {Nb}_Kab a Alice, como desafio. (5) Alice responde {Nb-1}_Kab, provando que possui Kab. O valor Nb impede a repetição da etapa 4. Esse protocolo sofre de um conhecido ataque de repetição, explorado por Denning e Sacco (1981).

Denning e Sacco (1981) descobriram uma falha: a resposta do AS na etapa 2 não é atual, pois não contém uma marca temporal ou um valor único fornecido pelo servidor. Um atacante, Mallory, que havia interceptado anteriormente uma chave de sessão Kab ao comprometer uma sessão passada, pode reenviar o tíquete antigo {Kab, A}_Kb a Bob em qualquer momento futuro. Ao receber o que parece ser um tíquete legítimo de Alice, Bob usa a chave comprometida Kab na sessão. A correção proposta por Denning e Sacco é adicionar uma marca temporal à resposta do AS e ao tíquete. Essa solução foi adotada no Kerberos — marcas temporais são incorporadas aos tíquetes para limitar seu período de validade.

O protocolo de chave pública NS, também de 1978, foi projetado para a autenticação mútua entre duas partes usando criptografia de chave pública. (1) Alice envia {Na, A}_PKb a Bob, com o valor Na criptografado usando a chave pública de Bob. (2) Bob responde {Na, Nb}_PKa, com os dois valores únicos criptografados usando a chave pública de Alice. (3) Alice responde {Nb}_PKb, devolvendo o valor único de Bob criptografado usando a chave pública dele. Após essa troca, ambas as partes possuem os dois valores únicos, Na e Nb, e podem derivar uma chave de sessão. O protocolo pareceu seguro por 17 anos — até o ataque de Lowe em 1995.

Gavin Lowe (1995) descobriu uma falha crítica usando o verificador de modelos FDR (Falhas no raciocínio composicional). Mallory pode se passar por Bob para Alice enquanto retransmite mensagens para um Bob legítimo. Etapa 1: Alice envia {Na, A}_PKm a Mallory, acreditando estar falando com Bob. Mallory encaminha {Na, A}_PKb a Bob. Etapa 2: Bob responde {Na, Nb}_PKa, que Mallory descriptografa e criptografa novamente para Alice: {Na, Nb}_PKa. Alice descriptografa a mensagem e extrai Nb. Etapa 3: Alice envia {Nb}_PKm, acreditando que a mensagem chegará a Bob. Mallory a descriptografa e encaminha {Nb}_PKb a Bob. Bob acredita ter concluído uma autenticação mútua com Alice — mas Alice está, na verdade, autenticando-se com Mallory. A correção é que, na etapa 2, Bob inclua a própria identidade: {Na, Nb, B}_PKa.

A correção de Lowe para o protocolo NSPK é simples, mas profunda: a resposta de Bob na etapa 2 deve incluir a identidade B de Bob, tornando-se {Na, Nb, B}_PKa. Agora, quando Alice recebe a resposta, ela verifica se a identidade B incluída corresponde à parte com a qual pretendia entrar em contato. Mallory não pode substituir a resposta dele — precisaria da chave privada de Alice para construir um {Na, Nb, M}_PKa válido que passe pela verificação de Alice. Esta lição é generalizada como o Princípio de Needham-Abadi: as mensagens de autenticação devem vincular explicitamente a identidade do remetente, sem depender apenas do contexto para identificá-lo.

A descoberta da falha do NSPK por Lowe foi auxiliada pelo verificador de modelos FDR (Refinamento de Falhas-Divergências), que explora exaustivamente todas as possíveis execuções do protocolo, incluindo intervenções de adversários. Isso motivou o desenvolvimento de ferramentas de análise formal de protocolos: o Proverif (baseado no cálculo pi aplicado) pode provar ou refutar propriedades de autenticação e sigilo em sessões infinitas. O Tamarin Prover usa reescrita de multiconjuntos e oferece suporte a protocolos complexos, como TLS 1.3 e Signal. AVISPA e Scyther são outras ferramentas. Projetos modernos de protocolos (TLS 1.3, Signal, Noise) passam por verificação formal antes da implantação — um legado direto do episódio NS/Lowe.

Os ataques ao NS esclareceram a distinção entre objetivos de autenticação. Autenticação de entidade: provar que uma parte está ativa no momento e participando do protocolo (a novidade é importante). Autenticação da origem dos dados: provar que uma mensagem específica foi criada por uma parte específica (isso pode não implicar que ela esteja ativa). O ataque de Lowe compromete a autenticação de entidade — Alice acredita estar se autenticando com Bob, mas na verdade está se autenticando com Mallory, que retransmite as mensagens para Bob. As especificações modernas de protocolos declaram os objetivos com precisão: "Alice está autenticada perante Bob como a iniciadora desta sessão." Objetivos vagos levam a especificações ambíguas que passam por revisões informais, mas falham na análise formal.

Outra classe de ataques relacionados ao NS é o ataque de reflexão: Mallory reenvia para Alice as mensagens recebidas de Alice. Se o protocolo for simétrico (ambas as partes usam a mesma chave e o mesmo formato de mensagem), Alice poderá aceitar o próprio desafio como uma resposta válida de Bob. Defesa: usar direções de chave diferentes (chaves separadas de criptografia e descriptografia para cada direção) ou incluir indicadores de função nas mensagens (o criptografador inclui "eu sou o iniciador" na mensagem). Protocolos modernos como TLS incluem cadeias de caracteres específicas da função nas chaves derivadas por HKDF (usando "c e traffic" para o cliente e "s hs traffic" para o servidor) para impedir a reflexão.

Os ataques de entrelaçamento combinam mensagens de várias sessões de protocolo simultâneas para forjar uma autenticação. Se Alice executar duas sessões simultâneas, Mallory poderá misturar mensagens de ambas para criar uma sessão combinada consistente, mas inválida, que autentica Mallory. Defesa: vinculação à sessão — cada mensagem deve ser vinculada criptograficamente ao contexto da sessão (por exemplo, incluir um identificador de sessão ou usar uma chave exclusiva por sessão). O TLS impede o entrelaçamento por meio da mensagem Finished, que é um MAC sobre a transcrição completa da sessão atual. Qualquer mensagem entrelaçada altera a transcrição, invalidando o valor Finished.

Os protocolos Needham-Schroeder influenciaram diretamente o projeto do Kerberos (marcas de tempo para impedir reenvios, emprestadas da correção de Denning-Sacco), do TLS (o MAC da transcrição da mensagem Finished impede entrelaçamento e reflexão), do Signal Protocol (vinculação à sessão por meio do estado do mecanismo de atualização) e do Noise Protocol Framework (vinculação da identidade nos padrões de negociação). Os ataques ao NS estabeleceram que argumentos informais de segurança são insuficientes — todo protocolo deve ser analisado contra um adversário ativo que controla a rede e pode reenviar, reordenar e modificar mensagens. Esse modelo de adversário (Dolev-Yao) é hoje padrão na verificação formal de protocolos.

Que mudança simples Lowe propôs para corrigir a vulnerabilidade do protocolo NS de chave pública?

O protocolo Needham-Schroeder simétrico (1978) introduziu a distribuição de chaves de sessão baseada em TTP. O ataque de Denning-Sacco (1981) encontrou uma vulnerabilidade de reenvio — corrigida com marcas de tempo no Kerberos. O protocolo NSPK de chave pública sofreu um ataque MITM descoberto por Lowe (1995) por meio da verificação de modelos — corrigido com a inclusão da identidade do remetente nas mensagens. Esses ataques estabeleceram a verificação formal (Proverif, Tamarin) como essencial para o projeto de protocolos. Lições principais: as mensagens devem vincular a identidade do remetente, as sessões devem ser isoladas umas das outras, os ataques de reflexão são impedidos pela derivação direcional de chaves e os ataques de entrelaçamento são impedidos por MACs da transcrição.