Lógica de Burrows–Abadi–Needham

A lógica de Burrows–Abadi–Needham (também conhecida como a lógica BAN) é um conjunto de regras para definir e analisar protocolos de troca de informação. Especificamente, a lógica BAN ajuda seus usuários a determinar se a informação trocada é confiável, segura contra espionagem, ou ambos. A lógica BAN começa com a suposição de que todas as trocas de informações acontecem em mídia vulnerável a adulteração e a monitoramento público. Isso evoluiu para o popular mantra de segurança "Não confie na rede."

Uma típica sequência da lógica de BAN inclui três etapas:

1. Verificação da origem da mensagem 

2. Verificação da recenticidade (freshness) da mensage

3. Verificação da confiabilidade da origem. 

A lógica BAN usa postulados e definições – como todos os sistemas axiomáticos – para analisar protocolos de autenticação. O uso da lógica BAN muitas vezes acompanha uma formulação de uma notação de protocolo de segurança de um protocolo e é, às vezes, dado em papéis.

Tipo de linguagem

A lógica BAN e lógicas na mesma família são decidíveis (linguagem recursiva): existe um algoritmo formulando hipóteses BAN e tomando uma suposta conclusão, e isso responde se a conclusão é ou não derivável das hipóteses. Os algoritmos propostos usam uma variante de conjuntos mágicos.

Alternativas e críticas

A lógica BAN inspirou muitos outros formalismos similares, como a lógica GNY. Alguns desses tentam reparar uma fraqueza da lógica BAN: a falta de uma boa semântica com um sentido claro em termos de conhecimento e universos possíveis. No entanto, a partir de meados da década de 1990, protocolos criptográficos foram analisados em modelos operacionais (assumindo criptografia perfeita) usando verificadores de modelo, e vários "bugs" foram encontrados nos protocolos que foram "verificados" com a lógica BAN e formalismos relacionados. Em alguns casos, o protocolo foi fundamentado como seguro pela análise BAN, mas era na verdade inseguro. Isto levou ao abandono de lógicas da família BAN em favor de métodos de comprovação baseados em raciocínios de invariância padrão.

Regras básicas

As definições e suas implicações estão abaixo (P e Q são agentes de rede, X é uma mensagem, e K é uma chave de encriptação):

• P acredita em X: P age como se X fosse verdadeiro, e pode asseverar X em outras mensagens.
•  P tem jurisdição sobre X: deve-se confiar nas crenças de P sobre X. 
• P uma vez disse X: certa vez, P transmitiu (e nela acreditou) a mensagem X, por mais que P possa não mais acreditar em X.
•  P "vê" X: P recebe a mensagem X, e pode ler e repetir X.
• {X}K: X é encriptado com a chave K.
• #(X): X não foi previamente enviado em nenhuma mensagem (é recente).
• chave(K, P↔Q): P e Q podem se comunicar com a chave compartilhada K 

O significado dessas definições é captado em uma série de postulados:

• Se P acredita na chave(K, P↔Q) e P "vê" {X}K, então P acredita que (Q uma vez disse X) 
• Se P acredita que (Q uma vez disse X) e P acredita em #(X), então P acredita que (Q acredita em X). 

Aqui, P deve crer que X é recente. Caso não se saiba se X é recente, então essa pode ser uma mensagem obsoleta, retransmitida (replayed) por um invasor (attacker).

• Se P acredita que (Q tem jurisdição sobre X) e P acredita que (Q acredita em X), então P acredita em X
• Existem vários outros postulados técnicos relacionados à composição de mensagens. Por exemplo, se P acredita que Q uma vez disse <x, y="">, a concatenação de X e Y, então P também acredita que Q uma vez disse X, e P também acredita que Q uma vez disse Y. </x,>

Usando essa notação, as premissas por trás de um protocolo de autenticação podem ser formalizadas. Usando os postulados, pode-se provar que certos agentes acreditam que podem se comunicar usando certas chaves. Se isso não puder ser provado, o ponto de falha geralmente sugere que tenha havido um ataque que comprometeu o protocolo.

Análise de lógica BAN do protocolo “Wide Mouth Frog”

Um protocolo bem simples – o protocolo “sapo de boca larga” (Wide Mouth Frog protocol) - permite que dois agentes, A e B, estabeleçam comunicações seguras, usando um servidor confiável de autenticação, S, e "clocks' sincronizados relacionados. Usando a notação padrão o protocolo pode ser especificado da seguinte forma:

${\displaystyle }$

Agentes A e B equipados com chaves Kas e Kbs, respectivamente, para se comunicarem seguramente com S. Então, temos as seguintes premissas:

A acredita na chave (Kas, A↔S) 

S acredita na chave (Kas, A↔S) 

B acredita na chave (Kbs, B↔S) 

S acredita na chave (Kbs, B↔S) 

Agente A quer iniciar uma conversação segura com B. Ele, portanto, inventa uma chave, Kab, a qual usará para se comunicar com B. A acredita que essa chave é segura, uma vez que a chave foi feita por ele.

A acredita na chave(K_ab, A↔B)

B está disposto a aceitar esta chave, desde que tenha certeza de que ela veio de A.

B acredita que (A tem jurisdição sobre a chave(K, A↔B))

Além disso, B concorda em confiar que S irá retransmitir com precisão as chaves de A.

B acredita que (S tem jurisdição sobre (A acredita na chave(K, A↔B)))

Isto é, se B acredita que S acredita que A quer usar uma chave especifica para se comunicar com B, então B vai confiar em S e acreditar nisso também.

O objetivo é obter

B acredita na chave(K_ab, A↔B)

A lê o clock, obtendo o tempo atual t, e envia a seguinte mensagem:

1 A→S: {t, chave(K_ab, A↔B)}_Kas

Isto é, A manda sua chave de sessão escolhida e o tempo atual para S, criptografado com sua chave privada de servidor de autenticação Kas.

Já que S acredita na chave (K_as, A↔S), e S "vê" {t, chave(K_ab, A↔B)}_Kas, então S conclui que A, na verdade, uma vez disse {t, chave(K_ab, A↔B)}. (Particularmente, S acredita que a mensagem não foi adulterada por um invasor (attacker))

Já que os clocks estão sincronizados, podemos supor que

S acredita em #(t)

Já que S acredita em #(t) e S acredita que A uma vez disse {t, chave(K_ab, A↔B)}, S acredita que A na verdade acredita que a chave(K_ab, A↔B). (Particularmente, S acredita que a mensagem não foi retransmitida por um invasor que a tenha capturado em algum tempo passado.)

S , em seguida, encaminha a chave a B:

2 S→B: {t, A, A acredita na chave(K_ab, A↔B)}_Kbs

Porque a mensagem 2 é criptografada com K_bs, e B acredita na chave(K_bs, B↔S), B agora acredita que S uma vez disse {t, A, A acredita na chave(K_ab, A↔B)}. Já que os clocks estão sincronizados, B acredita em #(t), e assim #(A acredita na chave(K_ab, A↔B)). Já que B acredita que a afirmação de S é recente, B acredita que S acredita que (A acredita na chave(K_ab, A↔B)). Já que B acredita que S tem autoridade sobre o que A acredita, B acredita que (A acredita na chave(K_ab, A↔B)). Já que B acredita que A tem autoridade sobre as chaves de sessão entre A e B, B acredita na chave(K_ab, A↔B). B pode agora contactar A diretamente, usando K_ab como uma chave de sessão secreta .

Agora vamos supor que abandonamos o pressuposto de que os clocks estão sincronizados. Nesse caso, S recebe a mensagem 1 de A com {t, chave(K_ab, A↔B)}, mas ele não pode mais concluir que t é recente. Ele sabe que A enviou esta mensagem em algum tempo no passado (porque foi criptografada com K_as) mas não sabe se é uma mensagem recente, então S não acredita que A necessariamente quer continuar a usar a chave K_ab. Isso aponta diretamente para uma quebra no protocolo: Um invasor que pode capturar mensagens pode descobrir uma das antigas chaves de sessão K_ab. (Isso pode levar um longo tempo.) O invasor, em seguida, retransmite a antiga {t, chave(K_ab, A↔B)} mensagem, enviando-a para S. Se os clocks não estiverem sincronizados (talvez devido ao mesmo ataque), S pode acreditar nessa antiga mensagem  e pedir que B use a antiga e  comprometida chave mais uma vez.

O papel  "Lógica de Autenticação" original (link abaixo) contém esse exemplo e muitos outros, incluindo análises do protocolo "de aperto de mão " Kerberos (Kerberos handshake protocol) , e duas versões do Andrew Project RPC handshake (uma das quais é defeituosa).

Referências

[1] "Course material on BAN logic" (PDF). UT Austin CS.

[2] Monniaux, David (1999). "Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief". Proceedings of The 12th Computer Security Foundations Workshop.

[3] Boyd, Colin; Mao, Wenbo (1994). "On a Limitation of BAN Logic". EUROCRYPT '93 Workshop on the theory and application of cryptographic techniques on Advances in cryptology. Retrieved 2016-10-12.

Ler mais

• Burrows, Michael; Abadi, Martín; Needham, Roger. «A Logic of Authentication». CiteSeerX 10.1.1.115.3569 
• Source: The Burrows–Abadi–Needham logic