{pt_PT=Automation of Secrecy Proofs for Security of Protocols} {} EVALUATED

Detalhes: {pt=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. , en=Security protocols are distributed algorithms for achieving security goals, like secrecy or authentication, even when communicating over an insecure network. They play a critical role in modern network and business infrastructures. This thesis focuses on the automated verification of security protocols based in the technique for symbolic adversaries proposed by Bana. This technique aims to deal with non-Dolev-Yao attacks and computational attacks. Dolev-Yao model is basically an intruder model that defines the abilities of an intruder in the communication over an insecure network. This technique to deal with this issue uses an intruder model that instead of defining what are the abilities of the intruder, defines the axioms that the intruder cannot violate. This technique aims to combine the best of symbolic models with the best of computational models, achieving computational soundness. There already exists a tool that implements this technique, but besides using a forward search approach to explore the state space of a protocol, it also bounds the number of instances. To deal with this issue we're going to use backtracking, that is commonly used in other verification tools. For the purpose of not only implementing Bana technique, but also to exceed Scary limitations, we developed a tool that uses a backward approach to explore the state space, supporting this way an unlimited number of sessions. Also this tool relies on Scary to guarantee that the execution of our tool is coherent with a certain set of axioms, like the freshness axiom, the non-malleability axiom, and so forth. }

Discussão: novembro 11, 2015, 14:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

AUTOR

Miguel Abreu Malafaia Mendes Belo (ist169566)

ORIENTADOR

Pedro Miguel dos Santos Alves Madeira Adão

Departamento de Engenharia Informática (DEI)

Professor Auxiliar