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