Mostrar código-fonte de Lógica de Burrows–Abadi–Needham

{{mais fontes|data=dezembro de 2016}}
{{Wikificação|data=dezembro de 2016}}
'''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:<ref>{{citar web|url=http://www.cl.cam.ac.uk/~rja14/Papers/SEv2-c03.pdf|publicado=UT Austin CS|título=Course material on BAN logic}}</ref>
1. Verificação da origem da mensagem <div>2. Verificação da recenticidade ([[:en:Replay_attack|freshness]]) da mensage
3. Verificação da confiabilidade da origem. 
</div>A lógica BAN usa [[postulados]] e [[Definição|definições]] – como todos os [[sistemas axiomáticos]] – para analisar [[:en:Communications_protocol|protocolos]] de [[:en:Authentication|autenticação]]. O uso da lógica BAN muitas vezes acompanha uma formulação de uma [[:en:Security_protocol_notation|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 [[:en:Recursive_language|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 [[:en:Datalog|conjuntos mágicos]].<ref>{{Citar periódico|url=http://citeseer.ist.psu.edu/monniaux99decision.html}}</ref>

== 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 [[:en:Key_(cryptography)|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” ([[:en:Wide_Mouth_Frog_protocol|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:[[Ficheiro:Wide Mouth Frog protocol 2.svg|esquerda|180x180px]][[Ficheiro:Wide Mouth Frog protocol.svg|esquerda|180x180px]]
:<math></math>
:

Agentes A e B equipados com chaves K<small>as</small> e K<small>bs</small>, respectivamente, para se comunicarem seguramente com S. Então, temos as seguintes premissas:
: A acredita na chave (K<small>as</small>, A↔S) 
: S acredita na chave (K<small>as</small>, A↔S) 
: B acredita na chave (K<small>bs</small>, B↔S) 
: S acredita na chave (K<small>bs</small>, 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''<sub>''ab''</sub>, ''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''<sub>''ab''</sub>, ''A''↔''B'')
A lê o clock, obtendo o tempo atual t, e envia a seguinte mensagem:
: 1 ''A''→''S'': {''t'', chave(''K''<sub>''ab''</sub>, ''A''↔''B'')}<sub>''Kas''</sub>
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''<sub>''as''</sub>, ''A''↔''S''), e ''S'' "vê" {''t'', chave(''K''<sub>''ab''</sub>, ''A''↔''B'')}<sub>''K''<sub>''as''</sub></sub>, então S conclui que A, na verdade, uma vez disse {''t'', chave(''K''<sub>''ab''</sub>, ''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''<sub>''ab''</sub>, ''A''↔''B'')}, S acredita que A na verdade acredita que a chave(''K''<sub>''ab''</sub>, ''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''<sub>''ab''</sub>, ''A''↔''B'')}<sub>''K<sub>bs</sub>''</sub>
Porque a mensagem 2 é criptografada com ''K''<sub>''bs''</sub>, e ''B''
acredita na chave(''K''<sub>''bs''</sub>, ''B''↔''S''), ''B'' agora acredita que ''S'' uma vez disse {''t'', ''A'', ''A'' acredita na chave(''K''<sub>''ab''</sub>, ''A''↔''B'')}.
Já que os clocks estão sincronizados, ''B'' acredita em #(''t''), e assim #(''A'' acredita na chave(''K''<sub>''ab''</sub>, ''A''↔''B'')). Já que ''B''
acredita que ''a ''afirmação de S é recente, ''B'' acredita que ''S'' acredita que
(''A'' acredita na chave(''K''<sub>''ab''</sub>, ''A''↔''B'')). Já que ''B''
acredita que ''S'' tem autoridade sobre o que ''A'' acredita, ''B ''acredita
que (''A'' acredita na chave(''K''<sub>''ab''</sub>, ''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''<sub>''ab''</sub>, ''A''↔''B''). ''B'' pode agora contactar ''A''
diretamente, usando ''K''<sub>''ab''</sub> 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''<sub>''ab''</sub>, ''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''<sub>''as''</sub>)
mas não sabe se é uma mensagem recente, então ''S'' não acredita que ''A''
necessariamente quer continuar a usar a chave
''K''<sub>''ab''</sub>. Isso aponta diretamente para uma quebra no
protocolo: Um invasor que pode capturar mensagens pode descobrir uma das antigas chaves de sessão ''K''<sub>''ab''</sub>. (Isso pode levar um longo tempo.) O invasor, em seguida, retransmite a antiga {''t'',
chave(''K''<sub>''ab''</sub>, ''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 [[:en:Andrew_Project|Andrew Project]] RPC handshake (uma das quais é defeituosa).

== Referências ==
[http://www.cl.cam.ac.uk/~rja14/Papers/SEv2-c03.pdf] [http://www.cl.cam.ac.uk/~rja14/Papers/SEv2-c03.pdf "Course material on BAN logic"] (PDF). UT Austin CS.

[https://citeseer.ist.psu.edu/myciteseer/login] Monniaux, David (1999). [http://citeseer.ist.psu.edu/monniaux99decision.html "Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief"]. ''Proceedings of The 12th Computer Security Foundations Workshop''.

[http://dl.acm.org/citation.cfm?id=188350] Boyd, Colin; Mao, Wenbo (1994). [http://dl.acm.org/citation.cfm?id=188350 "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 ==
* {{citar periódico| citeseerx = 10.1.1.115.3569 |título= A Logic of Authentication | url = http://ftp.digital.com/pub/DEC/SRC/research-reports/abstracts/src-rr-039.html | authorlink1 = Michael Burrows |primeiro1 = Michael |último1 = Burrows | authorlink2 = Martín Abadi |primeiro2 = Martín |último2 = Abadi | authorlink3 = Roger Needham |primeiro3 = Roger |último3 = Needham }}
*Source: [https://web.archive.org/web/20050902032746/http://www.pasta.cs.uit.no/thesis/html/ronnya/node31.html The Burrows–Abadi–Needham logic]

{{DEFAULTSORT:Burrows-Abadi-Needham logic}}
[[Categoria:Criptografia]]