Modelo de atacante Dolev-Yao e criptografia simbólica

Proposto por Danny Dolev e Andrew Yao em 1983, o modelo Dolev-Yao é o modelo de adversário padrão para a análise simbólica de protocolos. O invasor controla toda a rede.

O invasor Dolev-Yao pode: interceptar qualquer mensagem, armazenar mensagens, repetir mensagens antigas, forjar novas mensagens a partir de componentes conhecidos, mas não pode comprometer as primitivas criptográficas subjacentes.

Nos modelos simbólicos, a criptografia é uma caixa-preta perfeita: o atacante não consegue descriptografar sem a chave, fatorar números grandes nem falsificar assinaturas. Isso simplifica a análise, mas pode não detectar ataques no nível da implementação.

As mensagens são modeladas como termos: enc(k, m), sig(sk, m), hash(m), pair(a, b). O atacante conhece determinados termos e deriva novos usando regras definidas (regras de dedução).

O conhecimento do atacante é fechado sob dedução: se ele conhece enc(k,m) e k, pode derivar m. Se conhece pair(a,b), pode derivar a e b. O fecho do conhecimento inicial = tudo o que o atacante pode aprender.

A segurança do protocolo é expressa assim: "o conhecimento do atacante nunca contém o segredo s em nenhum estado alcançável". Sigilo = alcançabilidade. Autenticação = ausência de determinados padrões de rastros maliciosos.

Protocolo de duas partes: A→B: {Na, A}_{K_B}; B→A: {Na, Nb}_{K_A}; A→B: {Nb}_{K_B}. Na álgebra de termos: Alice envia enc(pubkey_B, pair(Na, A)). Verificamos que, após a execução, somente B conhece Na.

O cálculo pi aplicado (Abadi e Fournet, 2001) é uma álgebra de processos para modelar protocolos. Os processos se comunicam por canais; o atacante controla os canais públicos. ProVerif e Tamarin usam esse formalismo.

Um protocolo seguro no modelo de Dolev-Yao ainda pode ser computacionalmente inseguro se a instanciação criptográfica for fraca. O teorema da solidez computacional (Cortier et al.) estabelece uma ponte para classes específicas de primitivas.

Dolev-Yao não consegue modelar: propriedades algébricas (por exemplo, a comutatividade de XOR), ataques por canal lateral, erros de implementação ou falhas probabilísticas. Extensões como o modelo de teoria equacional lidam com algumas propriedades algébricas.

Qual capacidade o atacante de Dolev-Yao NÃO possui?

Dolev-Yao dá ao atacante controle total da rede, mas pressupõe criptografia perfeita. As mensagens são termos em uma álgebra; a segurança é uma propriedade de alcançabilidade. O cálculo pi aplicado fornece a linguagem formal. Limitações: não consegue modelar relações algébricas, canais laterais nem erros de implementação.