Resumo do Artigo Beyond Stack Smashing Recent Advances in Exploiting

Jonathan Pincus é pesquisador sênior da Microsoft Research, e Brandon Baker, engenheiro de segurança de desenvolvimento da Microsoft. Neste artigo, eles descrevem três famílias de ataques derivados do estouro de buffers.

O estouro de buffers ocorre quando um programa tenta ler ou escrever além do limite declarado de um array (o referido buffer). Nas linguagens C e C++ não existe nenhum tipo de checagem de extrapolação de limites, ao contrário do que acontece com as linguagens Pascal, Java e C# por exemplo. O estouro de buffer pode ainda ser caracterizado como estouro de buffer da pilha ou estouro de buffer do heap, dependendo do tipo de memória utilizada – no primeiro caso trata-se de variáveis estáticas, localizadas na pilha de execução, ao passo que no segundo caso trata-se de variáveis dinâmicas, localizadas no heap.

A abordagem tradicional do estouro de buffer é o stack smashing: a modificação do endereço de retorno presente na pilha de execução de maneira a alterar o fluxo de execução do programa. Ao invés de apontar para o retorno, o endereço aponta para código malicioso armazenado em determinado local pelo atacante.

No artigo, os autores apresentam 3 novos tipos de ataques desta natureza, afim de que a compreensão do funcionamento dos ataques leve a melhores estratégias de segurança. A seguir, cada um deles é brevemente apresentado.

Arc injection
Este ataque é orientado a dados. Ao invés de também inserir código executável malicioso para que seja desviado o fluxo de execução até ele, um atacante pode apenas fornecer dados tais que quando o programa original operar sobre os mesmos, o objetivo do ataque também será atingido. Um exemplo deste tipo de ataque são comandos de sistema que o programa atacado passa a utilizar para criar novos processos, o que permite a execução arbitrária de código.

Um exemplo deste ataque é o estouro de buffer para desviar o fluxo de execução para uma chamada SYSTEM() presente no código do próprio programa, onde as verificações de integridade dos parâmetros podem ser puladas e o parâmetro é um dado armazenado pelo atacante.

Pointer Subterfuge
Este ataque consiste em alterar o valor de ponteiros. Existem pelo menos quatro versões deste tipo de ataque:

- Function-Pointer Clobbering: Alteração do valor de um ponteiro para um local com código malicioso;

- Data-Pointer Modification: Alteração de locais arbitrários da memória como isca, na expectativa de que tais locais sejam utilizados em alguma atribuição, fazendo com que se obtenha poder também sobre outras áreas da memória que forem fisgadas;

- Exception-Handler Hijacking: Quando um programa lança uma exceção, o Windows examina uma lista encadeada que armazena manipuladores de exceção e invoca um ou mais via ponteiros para o tratamento da exceção. O ataque consiste em alterar tal ponteiro via estouro de buffer, permitindo que ao invés de invocar um manipulador de exceção, o fluxo de execução seja desviado.

- Virtual Pointer (VPTR) Smashing: A maioria dos compiladores C++ implementa funções virtuais através de uma tabela de funções virtuais (VTBL) associada a cada classe. A VTBL é um array de ponteiros para funções utilizados em tempo de execução para implementar o despacho dinâmico. Objetidos individuais apontam para a VTBL apropriada através de ponteiros virtuais (VPTR) armazenado no header do objeto. Substituindo-se o VPTR de um objeto com um ponteiro para código malicioso faz com que o fluxo seja desviado na próxima vez em que uma função virtual for invacada.

Heap Smashing

Ao contrário do que se pensava até recentemente, não são apenas os buffers da pilha de execução vulneráveis a este tipo de ataque. Alocadores de memória dinâmica mantém headers para cada bloco do heap, ligados duplamente em listas encadeadas de blocos alocados e liberados. Tais headers são atualizados a cada operação sobre a memória (alocação e liberação).

Se houverem três blocos de memória contíguos X, Y e Z, e houver estouro de buffer em X de forma que os ponteiros do header de Y sejam modificados, pode ocorrer modificação de uma parte arbitrária da memória quando X, Y e Z forem liberados.

Referência
Pincus, J.; Baker, B. Beyond Stack Smashing: Recent Advances in Exploiting Buffer Overruns. Security & Privacy, IEEE Volume 2, Issue 4, July-Aug. 2004 Page(s): 20 – 27. Disponível em: http://ieeexplore.ieee.org/iel5/9141/29316/01324594.pdf. Acesso em 02 de Junho de 2010.

Reflections on Trusting Trust by Ken Thompson

Ken Thompson recebeu o prêmio Turing pela ACM (Association for Computing Machinery) em 1983 pelo desenvolvimento da teoria de sistemas operacionais e pela implementação do sistema operacional UNIX. O autor se auto-denomina um programador, e em três etapas descreve a criação de um trojan. Um programa que se auto-replica, através de um compilador

Na primeira etapa o autor descreve a criação de um programa que se auto-replique. Na segunda etapa, o autor utiliza o exemplo do compilador C, desenvolvido em liguagem C para demonstrar que existem falhas sobre como compilar em C um novo compilador com instruções diferentes. Haveria inconsistências, uma vez que o compilador original não reconhecerá as novas instruções, o que leva a alterações em mais baixo nível no compilador original, possibilitando que ele seja compilado. Na etapa 3, o autor apresenta a introdução de código malicioso no novo compilador, o qual descompila o comando “login” e o compila novamente para aceitar uma senha mestra, além da senha correta. Se o código malicioso for auto-replicante e atacar o código-fonte de um compilador, é possível utilizar o binário malicioso como original e apagar o código fonte malicioso, não deixando rastros. Desta forma, teríamos um código-fonte limpo e um binário malicioso, que se auto-replicaria a cada compilação.

O autor chega à conclusão de que não se pode confiar em códigos não escritos por você mesmo, não importando o nível de verificação de códigos-fonte podem nos assegurar quando se utiliza códigos não confiáveis. À medida que o nível dos códigos abaixa (compilador, assembler, liguagem de montagem, carregador ou mesmo microcódigo de hardware), mais difícil é a detecção de possíveis “bugs”.

Por fim, o artigo conclui que a segurança fica comprometida quanto mais dependermos de códigos de terceiros. Ken afirma que apenas um código desenvolvido por você mesmo pode ser dito como um código confiável. O autor também enfatiza que o acesso não autorizado a computadores alheios é crime e deve ser levado a sério.

Pontos Principais do Artigo

• Não existe código confiável, exceto o de sua autoria;
• À medida em que o nível dos códigos-fonte diminui, mais difícil é a detecção de código malicioso;
• Ainda no ano de 1984 o autor já alertava sobre as falhas nos códigos penais a respeito de crimes digitais, e ainda alertava sobre a gestação de uma “situação explosiva”.

Referência

[1] Thompson, Ken. Reflections on Trusting Trust.Communications of the ACM, 1984, vol. 27, n. 8, 761-763. Disponível em: http://portal.acm.org/citation.cfm?id=358210.

Criptografia com o uso de curvas elípticas

1. Introdução

Confidencialidade, integridade, autenticidade e não-repúdio são requisitos de segurança desejáveis em sistemas, e a criptografia assimétrica ou de chave pública é uma ferramenta indispensável para prover esses requisitos. 0 método mesmo sendo um pouco lento, é seguro pois utiliza um par de chaves, sendo uma pública e outra privada. A chave privada é conhecida apenas pelo dono da mensagem ao passo que a chave pública é distribuiria livremente para todos. A implementação dos CCE (Criptossistemas de Curvas Elípticas) apresenta alguns desafios, dentre eles o nível de segurança desejada, a qual plataforma a implementação se destina. 0 desempenho da aplicação resultante sofre um grande impacto da escolha feita nesta fase. Este artigo faz um estudo de criptografia com chave pública baseada em curvas elípticas, comparando com outros métodos de criptografia assimétrica e por sua vez com criptografia simétrica, apresentando ao final um exemplo de criptografia com curvas elípticas. (MENDES,2007)

2. Origem

De forma independente, em 1985, N. Koblitz (KOBLITZ, 1987) e V. Miller (MILLER,1986), propuseram utilizar o grupo de pontos de uma curva elíptica sobre um corpo finito para implementar criptossistemas de chave pública. Esses sistemas,denominados criptossistemas de curvas elípticas (CCE), têm sua segurança baseada na suposta intratabilidade do problema do logaritmo discreto no grupo de pontos de uma curva elíptica (PLDCE).

Figura 1 - Ilustação de uma Curva Elíptica e a adição de uma EC (BURNETT, 2002)

Nos últimos anos, muitos avanços foram feitos na área dos CCE. 0 melhor algoritmo conhecido para o problema do logaritmo discreto em curvas elípticas é de tempo exponencial (POLLARD,1978). Embora existam alguns ataques (algoritmos de tempo sub-exponencial (MENEZES, OKAMATO e VANSTONE, 1993) e polinomial para certos tipos de curvas elípticas, esses ataques podem ser evitados por meio de testes simples, descritos em vários padrões ïndustriais (ANSl,1999).

O fato de não se conhecer um algoritmo geral de tempo sub-exponencial para o PLDCE, possibilita que parâmetros menores sejam usados nos CCE, relativos aos sistemas baseados no PLD. Por exemplo, NIST - National lnstitute of Standards in Technology (Instituto Nacional de Normas em Tecnologia) recomenda o uso de chaves de 3072 bits nos sistemas baseados no PLD e RSA (Rivest, Shamir, Adleman) para se obter um nível de segurança comparável ao fornecido por um algoritmo de chave simétrica de 128 bits. Entretanto, nos CCE são suficientes chaves de 256 bits para se obter o mesmo nível de segurança.

3. Funcionalidade

Na prática, quando se deseja enviar uma mensagem utilizando o algoritmo ECDH, o remetente da mensagem pega a chave pública do destinatário contendo informações suficientes para gerar seu próprio par de chaves temporários de ECDH.

Tanto o destinatário quanto o remetente possuem um par de chaves relacionadas
com as chaves pública e privada. Desta forma o remetente utiliza a sua chave privada e a chave pública do destinatário para gerar um "ponto secreto na curva", utilizando de alguma forma este ponto secreto como uma chave de sessão. Sabendo que um ponto é uma coordenada (x,y), os dois correspondentes terão que decidir antecipadamente quais bits, a partir deste número, devem ser utilizados como chave. A figura 2 ilustra a combinação de chaves entre o remetente e o destinatário da mensagem para obter um ponto secreto.

Para ler a mensagem, o remetente necessita da chave de sessão, que é obtida através da combinação da sua chave privada com a chave pública temporária do remetente, enviada junto com a mensagem criptografada. Caso um invasor tenha acesso á mensagem criptografada, o mesmo teria que possuir uma das duas chaves privadas, pois o fato de conhecer as duas chaves públicas não resolve a questão. o algoritmo ECDH se parece com o algoritmo DH, pois ambos combinam chave pública e privada de maneira especial para gerar um segredo compartilhado. A principal diferença está na matemática subjacente, e isso explica o nome Elliptic Curve Diffie-Hellman (BURNETT, 2002).

Figura 2 - Combinação de chaves entre o remetente e destinatário de uma mensagem para obter um ponto secreto.

4. Vantagens

Algumas vantagens que resultam do fato de se usar pequenos parâmetros nos CCE incluem velocidade, chaves e certificados pequenos. Para certas aplicações, onde a capacidade de processamento, a potência computacional, o espaço de armazenamento e a banda-passante estejam limitados, os CCE superam outros sistemas de chave pública.

Por todas estas razões, os CCE têm tido crescente aceitação,nos setores industriais, como alternativa aos ja estabelecidos RSA protocolo de troca de chaves Diffie-Hellman e DSA.

A criptografia de chave pública, nos últimos anos, se converteu numa das tecnologias básicas para a construção de aplicações muito sensíveis à segurança,tais como correio eletrônico, eleições eletrônicas e comércio eletrônico.

5. Desvantagens

É um método lento porque os algoritmos, pela sua natureza matemática,são computacionalmente intensivos;

Requer uma autoridade de certificação, para que se possa garantir a identidade e ter chaves públicas confiáveis.

6. Considerações Finais


As curvas elípticas é uma opção para aplicações em ambientes computacionais limitados como telefones celulares, cartões inteligentes, pagers entre outros.

A criptografia simétrica não é substituída pela assimétrica. 0 importante é reconhecer e identificar as limitações de cada método, de forma a usá-los de uma maneira complementar para prover a segurança necessária às partes envolvidas, por causa da sua limitação de processamento.

7. Bibliográfia

BURNETT,1997 BURNETT, Steve, PAINE, Stephe, Criptografia e Segurança: O Guia Oficial RSA, Rio de Janeiro, Campus, 2002
KOBLITZ, 1987 Koblitz, N. Elliptic curve cryptosystems, Mathematics of Computation, 48 pp 203-209, 1987
MENDES,2007 Mendes, Aline Venoso, Estudo da Criptografia com chave pública baseadas com chave elípticas, Dissertação de Mestrado, Universidades de Montes Claros,2007
MENEZES,1993 MENEZES, OKAMOTO, T. E VANSTONE. Reducing elliptic curve logarithms to logarithms in a finite fiel. IEEE Transactions on Information Theory, 39 pp 1639-1946, 1993
MILLER,1986 Miller, V., Uses of elliptic curves in cryptography, Advances in Cryptology proceedings of Crypto 85, LNCS pp.417-426 New York. Springer –Verlag,1986
POLLARD,1978 POLLARD, J. Monte Carlo methods for índex computation mod p, Mathematics of Computation, 32, PP 918-924, 1978

Especificação Formal de Protocolos de Segurança

1.INTRODUÇÂO

No presente artigo iremos falar sobre Especificação Formal de Protocolos de Segurança, que visa através da utilização de métodos formais, os quais são um conjunto de técnicas suportadas pela lógica matemática.

A importância do estudo do tema se dá por causa dos serviços realizados pela Internet como compras on-line (e-commerce), transações bancárias, ou mesmo no cotidiano dos brasileiros como a utilização de cartões como MIFARE (PHILIPS, 2010) utilizado em aplicações de sistema de bilhetagem eletrônica como o sistema BOM (Bilhete de Ônibus Metropolitano), cartões de ponto, cartões de crédito, supermercado, estacionamento e outras aplicações, necessitam de um protocolo confiável de comunicação para trafegar os dados com o máximo de segurança. Essas tecnologias facilitam a vida dos seus operadores.

Em contrapartida há um aumento no número de crimes relacionados às telecomunicações intitulados por alguns autores como crimes modernos (ZANIOLO,2007). Por isso, empresas, áreas governamentais, acadêmicas e militares sentem-se vulneráveis quando a segurança das informações é ignorada. Nas redes de comunicação as mensagens são trocadas entre as entidades e como o ambiente móvel é mais suscetível a ataques, já que usam o ar como meio de transmissão, qualquer um com um receptor apropriado pode interceptar as mensagens sem ser detectado. Expondo informações importantes, como senhas e documentos, a não ser que estejam protegidas de alguma forma.

Para garantir a segurança das informações foram desenvolvidos vários protocolos que utilizam técnicas de criptografia para a implementação de serviços de segurança tais como sigilo do conteúdo das mensagens e da identidade do usuário/entidade, autenticação dos participantes na comunicação, integridade dos dados e não-repúdio (SCHNEIER, 1996).

Porém, se o protocolo criptográfico não for projetado corretamente proporcionará a um intruso a oportunidade de ataque por meio dos seguintes processos: substituição, exclusão, alteração ou criação de mensagens, ou pelo ataque aos algoritmos criptográficos utilizados. Por isso, vários métodos formais têm sido propostos a fim de analisar e projetar protocolos criptográficos.

O principal objetivo deste artigo é mostrar para a área acadêmica e comercial a importância do emprego de métodos formais no desenvolvimento de protocolos criptográficos.

O artigo está dividido da seguinte forma: a seção 2 apresenta os Riscos de Senha; na seção 3 são mencionados os tipos de métodos formais encontrados na literatura; na seção 4 é realizada a análise formal de três protocolos de autenticação do ambiente celular (GSM, CDPD e UMTS). E, finalmente, na seção 5 são feitas as considerações finais.

2. RISCO DA SENHA


As senhas são ainda a base sobre os quais muitos sistemas da informação atribuem sua segurança, porque é o principal mecanismo usado para autenticar usuários humanos aos sistemas informáticos. Na forma de PINs, eles também são usados em muitos sistemas embarcados, a partir de máquinas de dinheiro através de sistemas móveis. Eles levantam muitos problemas, tais como a dificuldade das pessoas têm em escolher senhas difíceis de adivinhar, ou lembrar senhas geradas aleatoriamente pelo sistema.

Segundo (Anderson,2001) considera as limitações dos sistemas embarcados que utilizam senhas. A típica aplicação é o controle remoto usado para abrir a garagem ou para desbloquear as portas dos automóveis fabricados até meados da década de 1990. Esses controles remotos primitivos apenas transmitem seu número de série de 16 bits, que também atua como senha.

Um ataque que se tornou comum era usar um grabber "um dispositivo que gravaria um código e jogá-lo novamente mais tarde”. Esses dispositivos, chegou por volta de 1995 em Taiwan, que permitiam ladrões que espreitavam em um estacionamentos para gravar o sinal usado para bloquear uma porta do carro e, em seguida, jogá-lo novamente para desbloquear o carro uma vez que o proprietário havia deixado.

Uma solução na época foi usar códigos separados para bloquear e desbloquear. Mas isso ainda não era o ideal. Primeiro, o ladrão podia esperar fora do estabelecimento de sua casa e gravar o código de desbloqueio. Em segundo lugar, senhas de 16 bits são muito pequenas e fáceis de serem descobertas por grabber. Em meados da década de 1990, surgiram dispositivos que podiam tentar todos os códigos possíveis, um após o outro. Este código poderia ser descoberto, em média, cerca de 215 países, que em 10 combinações, levaria menos de uma hora para serem descobertos.

Um ladrão que atua em um estacionamento com uma centena de veículos, poderá ser recompensado em menos de um minuto com um carro piscando suas luzes.

3. UTILIZANDO UM CANAL SEGURO

Supondo que para transmissão de uma senha seja transmitida em um canal de comunicação seguro. Para canais inseguros e necessários o compartilhamento de chaves.

Vamos estudar pelo caso proposto: Supondo que em um ônibus utiliza-se um sistema de bilhetagem eletrônico através de cartões, onde cada passageiro possua um cartão que irradia para um leitor o número da identificação e a identificação criptografada. O leitor e o cartão possuem chaves em comum. Em notação de protocolos temos:


C -> L: C {C}kcs

onde:

C -> É o cartão
L -> É o leitor

{C}kcs -> chave que sifra o código do cartão. Essa chave é comum para C e L (cartão e Leitora)

O caso em tela tem alguns problemas pois o intruso pode capturar a irradiação da transação e simplesmente repetir essa irradiação. Uma forma para previnir esse tipo de ataque é introduzir um nonce (number used once – Numero usado uma só vez). Neste caso a notação de protocolos fica:

C ->L : C, {C,N}kcs


Onde N pode ser um número aleatório ou seqüencial.

No caso apresentado manda C, manda C e N. O número N tem que ser conhecido por C e S, de tal forma se alguém tentar repetir ele não tem o nunce. É o que o token de banco faz, o nunce e um número aleatório gerado por C e N. L tem que guardar um histórico de nunce. Isso pode ser problemático pois no caso de um erro de comunicação um lado incrementa e outro não ira perder a referencia.

Desafio e Resposta (Challenge – response) Neste caso o NONCE e gerado aleatoriamente pelo servidor e nenhum dos dois atores precisam armazenar estados.


L -> C:N

C ->L: C {C,N}kCs


Onde:

L : leitora

C: Cartão N: numero do Nonce

KCS -> chave de sifra.

Supondo que o cartão passa pelo leitor e recebe um nonce que vai ler L. L recebe C,N cifrado com kCs. Supondo que o desafio seja a função x+1, ou seja se o cartão manda o numero 5 o leitor retorna o número 6 então ele respondeu ao desafio, junto com a chave C, S.
ATAQUE MAN-IN-THE-MIDDLE


Este ataque consiste em um ataque que via um nonce do servidor para o cartão de outro passageiro e retransmite a resposta deste cartão para o servidor.




1. S-> M: N
2. M ->C: N
3. C-> M: C,{C,N}KCS
4. M -> S: C, ,{C,N}KCS


Dado os protocolo acima iremos explicar passo a passo:

1. Um dispositivo criado M ( dispositivo do invasor ) capta o nunce gerado do servidor

2. Passa o nunce gerado para um outro cartão.

3. O cartão responde para o dispositivo do invasor a chave do cartão , o nunce sifrado com a chave KCS.

4. M envia os dados capturados no passo 3 e envia para o servidor.


4. MÉTODOS FORMAIS

Os protocolos estão sujeitos a ocorrência de erros em qualquer fase de seu projeto (especificação, construção e verificação). Por isso não é incomum que sejam descobertas falhas em protocolos publicados e utilizados por vários anos. Como exemplo, protocolo de (NEEDHAM e SCHROEDER, 1978) foi utilizado durante 4 anos até que (DENNING e SACCO, 1981) demonstraram que ele estava sujeito ao ataque do homem no meio e propuseram um protocolo alternativo. Porém, em 1994 Abadi e Needham demonstraram que este protocolo também possuía falhas (BUTTYÁN, 1999).


O emprego de métodos formais na área de criptografia é recente. Grande parte dos trabalhos nesta área são desenvolvidos na década de 90 (MEADOWS, 1995). Estes métodos permitem fazer uma análise completa do protocolo criptográfico e sua função principal é especificar se os objetivos propostos pelos autores são alcançados. Muitas vezes um protocolo é construído para realizar a distribuição segura de uma chave de sessão e quando analisado verifica-se que essa meta não é atingida.


Existem 4 abordagens diferentes para a análise de protocolos criptográficos (RUBIN e HONEYMAN,1993), (MEADOWS, 2000) e (GRITZALIS, SPINELLIS e GEORGIADIS, 1999). A primeira é a menos popular enquanto que a terceira é a mais utilizada:

1. uso de linguagens de especificação e ferramentas de verificação: o objetivo principal desta abordagem é tratar um protocolo criptográfico como qualquer
programa e tentar provar sua corretude. O principal problema é que estes métodos não são específicos para a análise de protocolos de segurança. Dentre os métodos podem ser destacados: LOTOS (Language of Temporal Ordering Specification) e Ina Jo.(VARADHARAJAN, 1990) utilizou LOTOS para analisar alguns protocolos criptográficos, porém não conseguiu demonstrar qualquer resultado. O autor concluiu que essa ferramenta não era adequada para a análise de segurança.


2. uso de sistemas especialistas: nestes métodos a maioria dos protocolos são modelados como máquinas de estado. São exemplos: Interrogator e NRL Protocol Analyzer. Neles o projetista especifica um estado inseguro e através de pesquisas exaustivas, tenta construir um caminho para este estado. Eles obtiveram mais êxito do que os anteriores, porém, possuem como desvantagem a grande quantidade de possíveis eventos que devem ser examinados;

3. uso de modelos baseados em lógicas modais: estas abordagens analisam os conceitos de crença e de conhecimento dos participantes do protocolo criptográfico. São utilizados principalmente para os protocolos de autenticação e de distribuição de chaves. Dentre eles pode-se destacar: as lógicas BAN e GNY. Apesar de serem mais simples e intuitivas do que as outras abordagens, são eficazes. O artigo da lógica BAN encontrou vários erros e redundâncias em protocolos bastante utilizados. Porém, o analista deve ter cuidado, pois suposições incorretas podem conduzir a erros na análise;


4. uso de sistemas algébricos: nesta abordagem o protocolo criptográfico é modelado como um sistema algébrico, associando um estado como se fosse o conhecimento do participante. São complementares aos métodos de lógica modal, pois também realizam uma formalização de problemas por hipóteses e nas propriedades de autenticação. O primeiro trabalho nesta área é o de Dolev-Yao e os outros trabalhos desenvolvidos são versões estendidas desse modelo. O problema desses sistemas é que são restritos para a análise da maioria dos protocolos. Só podem ser utilizados para descobrir fraquezas de segredos e não permitem que os participantes se lembrem de informações de um estado para o próximo.

O custo-benefício em utilizar uma dessas abordagens, antes de publicar o protocolo, é melhor do que ter que fazer alterações posteriores, já que é mais barato usar os métodos no desenvolvimento do protocolo do que fazer o seu replanejamento.

4.1. LÓGICA BAN


A lógica BAN foi desenvolvida por Burrows, Abadi e Needham (por isso o nome) em 1989. É a primeira lógica a analisar formalmente os protocolos criptográficos, principalmente os de autenticação e distribuição de chaves (BURROWS, ABADI e NEEDHAM, 1990). É a lógica mais popular na literatura para a análise de crenças e de conhecimento entre os participantes dos protocolos criptográficos. Apesar das críticas recebidas ela encontrou erros em
vários protocolos, como o de Needham-Schroeder, CCITT X.509, Yahalom e Kerberos. A lógica BAN também é utilizada como validação dos protocolos propostos em (AZIZ e DIFFIE, 1994) que desenvolveram um protocolo de autenticação para o ambiente celular e em (MYRVANG, 2000) que desenvolveu um protocolo de autenticação para redes locais sem fio.

Outras lógicas começaram a ser desenvolvidas estendendo ou aplicando os mesmos conceitos da lógica BAN. A de maior sucesso entre elas é a GNY (GONG, NEEDHAM e YAHALOM, 1990).

A lógica GNY introduziu novos conceitos, como reconhecimento e posse de fórmulas e a expressão “não originada-aqui” que permite aos participantes detectar mensagens que foram enviadas em sessões anteriores.Porém, a lógica GNY é mais complexa, possui muitas regras (mais de 50) que devem ser aplicadas em cada fase do protocolo e mais difícil de ser utilizada. Alguns autores consideram-na impraticável A complexidade é o maior problema das lógicas estendidas da BAN.

Na dissertação de mestrado (SANTOS, 2002) foi realizada uma comparação entre as duas lógicas, chegando-se à conclusão que a lógica GNY, por conter muitas regras, pode tornar a análise mais suscetível a erros e redundâncias. A lógica BAN também consegue chegar nos mesmos resultados finais, além disso, ela é mais simples e mais fácil de aplicar e de empregar seus postulados. Por estes motivos, a autora decidiu utilizar a lógica BAN, para analisar três importantes protocolos de autenticação da rede celular: GSM (Global System for Mobile Communications), CDPD (Cellular Digital Packet Data) e UMTS (Universal Mobile Telecommunications System). Como a lógica BAN possui muitos símbolos, a autora utilizou uma versão mais intuitiva que será mantida neste trabalho. Por exemplo, a expressão: P Q #(X) é substituida por P acredita Q disse novo(X) (lê-se: P acredita que Q, há algum tempo, disse que X é nova).

As principais expressões da lógica BAN são:


1. P acredita X: o participante P acredita na fórmula X ou está autorizado a acreditar em X, isso significa que P pode agir como se X fosse verdadeira;
2. P recebeu X: P recebeu uma mensagem contendo X e P pode obter X da mensagem (normalmente depois de algum deciframento);
3. P disse X: P uma vez disse X. O participante P, há algum tempo, enviou uma mensagem contendo a fórmula X;
4. P controla X: P tem jurisdição sobre X. O participante P é uma autoridade sobre X e deve ser confiado deste modo;
5. novo(X): (lê-se “X é nova”) a fórmula X é nova, ou seja, a fórmula X foi usada numa mensagem anterior à execução atual do protocolo. Os identificadores são gerados com a finalidade de serem novos;
6. P k Q: (lê-se “k é uma chave satisfatória para P e Q”). A chave k nunca será descoberta por qualquer participante, exceto por P, Q ou por alguém em quem eles confiam;
7. {X}K : fórmula X cifrada com a chave K. As mensagens cifradas somente são legíveis e verificáveis pelo possuidor da chave.
A notação abaixo é usada numa troca de mensagem:

Mi A -> B: {X}k

onde i é a iésima mensagem do protocolo: A envia X cifrada com a chave k para B. Em todas estas expressões, X é uma mensagem ou uma fórmula.


5. Considerações Finais

Este trabalho mostrou que é importante a especificação de protocolos e a utilização de métodos formais e qual a importância de um canal seguro e do risco de senhas que podem ser descoberto através de dispositivos eletrônicos construídos para este fim.
A especificação formal de protocolos de segurança propiciam um canal seguro para a comunicação de informações utilizando os métodos formais, porém esta especificação deve ser testada exaustivamente para detecção de falhas antes de serem implementadas.
Este trabalho fez um levantamento na literatura o qual podemos constatar a importância de uma especificação de protocolo, pois várias aplicações poderão utilizar garantindo a privacidade dos dados.

6. Referências Bibliográficas

ANDERSON, 2001 ANDERSON, R. “Security Engineering: A Guide to Building Dependable Distributed Systems”. Wiley, 2001.

AZIZ e DIFFIE, 1994 AZIZ, Ashar e DIFFIE, Whitfield. Privacy and
Authentication for Wireless Local Area Networks.

IEEE Personal Communications. pp. 25-31.1994.
BUTTYAN, 1999 BUTTYÁN, Levente. Formal methods in the design of cryptographic Protocols. http://citeseer.nj.nec.com/context/1960161/0. Technical, Report SSC/. Novembro 1999.
.
DENNING e SACCO, 1981 DENNING, Dorothy E. e SACCO, Giovanni Maria.
Timestamps in Key Distribution Protocols. Communications of the ACM, vol. 24, no 8 pp. 533-536.Agosto 1981.

GRITZALIS, SPINELLIS e GEORGIADIS, 1999 GRITZALIS, S., SPINELLIS, D. e GEORGIADIS, P.
Security protocols over open networks and distributed systems: formal methods for their analysis, design and verification. Computer Communications, vol. 22, no 8, pp. 697-709. Maio 1999.

MAIFARE,2010 http://www.a3m.eu/pt/Cartoes-contactless-Mifare.html, Acessado em Março de 2010

MEADOWS, 1995 MEADOWS, Catherine. Formal verification of
cryptographic protocols: A survey. ASIACRYPT’94 ,
133-150, http://citeseer.nj.nec.com/134868.html. 1995.

MEADOWS, 2000 MEADOWS, Catherine. Open Issues in Formal Methods
for Cryptographic Protocol Analysis. DISCEX 2000:,
v. 1, p. 237-250. IEEE Computer Society Press. Janeiro
2000.

MYRVANG,2000 MYRVANG, Per Harald. An Infrastructure for
Authentication, Authorization and Delegation. 2000.
Tese, Universidade de TromsÆ, Faculdade de Ciência,
www.cs.uit.no/studier/gradseksamen/myrvang.html

NEEDHAM e SCHROEDER, 1978 NEEDHAM, R. M. e SCHROEDER, M. D. Using
Encryption for Authentication in Large Networks of
Computers. Communications of the ACM, 21 p 12.

RUBIN e HONEYMAN,1993 RUBIN, Aviel D. e HONEYMAN, Peter. Formal Methods for the Analysis of Authentication Protocols. Technical Report CITI TR 93-7. Outubro 1993. www.citi.umich.edu/u/honey/papers.html

SANTOS,2002 SANTOS, Myrna C. M dos. Análise Formal de Protocolos de Autenticação para Redes Celulares. Dissertação de Mestrado. Instituto Militar de Engenharia, 2002.

SCHNEIDER,1996 SCHNEIER, Bruce. Applied Cryptography – Protocols,
Algorithms and Source Code in C – 2 a Edição. John Wiley & Sons, Inc. 1996. ISBN 0-471-12845-7.

VARADHARAJAN, 1990 VARADHARAJAN, V. Use a formal description technique in the specification of authentication protocols. Computer Standards and Interfaces, vol. 9,
pp. 203-215. 1990

ZANIOLO,2007 Zaniolo, Pedro Augusto, Crimes Modernos o Impacto da Tecnologia no Direito, Jurua Editora, 2007