Dissertação

Automation of Secrecy Proofs for Security of Protocols EVALUATED

Protocolos de Segurança são algoritmos distribuídos para alcançar objectivos de segurança, como por exemplo, secretismo da informação trocada e autenticação, mesmo numa rede insegura. Estes têm um papel bastante importante nas estruturas de negócio e de rede modernas. Esta tese tem como foco a verificação automática de protocolos de segurança baseada na técnica de adversários simbólicos proposta por Bana. Esta técnica pretende lidar com ataques não-Dolev-Yao e ataques computacionais. O modelo Dolev-Yao é basicamente um modelo de atacante que define quais é que são as habilidades de um atacante numa comunicação dentro de uma rede insegura. Esta técnica lida com esta questão usando um modelo de atacante que em vez de definir quais é que são as habilidades de um atacante, define qual o conjunto de axiomas que o atacante não pode violar, sendo que procura combinar o melhor dos modelos simbólicos com o melhor dos modelos computacionais, obtendo solidez computacional. Existe uma ferramenta que implementa esta técnica, mas para além de usar uma procura para a frente para explorar o estado de espaços de um protocolo, limita o número de instâncias. Para lidar com este assunto iremos utilizar um algoritmo de procura para trás, que é vulgarmente usado noutras ferramentas, como por exemplo o Scyther. Não só com o intuito de implementar a técnica do Bana, mas também de ultrapassar as limitações do Scary, desenvolvemos uma ferramenta, que utiliza uma abordagem de procura para trás para explorar o state space, podendo lidar assim com um número ilimitado de instâncias.
Segurança de Protocolos, Verificação Automática, Solidez Computacional, Informação Secreta, Modelo de Atacante

Novembro 11, 2015, 14:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Pedro Miguel dos Santos Alves Madeira Adão

Departamento de Engenharia Informática (DEI)

Professor Auxiliar