Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Ciência da Computação, Florianópolis, 2017 / Made available in DSpace on 2017-06-27T04:22:41Z (GMT). No. of bitstreams: 1
345978.pdf: 978430 bytes, checksum: e7dbdcc1dd284e84bcac339aae3f6488 (MD5)
Previous issue date: 2017 / Abstract : Security ceremonies are extensions of security protocols, including all that is out-of-bounds for protocols. Nowadays we lack a base description language and a detailed threat model for security ceremonies in order to be able to use symbolic evaluation methods and verify claims embedded in ceremonies. Our goal is to contribute with a syntax and detailed threat model for ceremonies description in order to establish our proposal for a new attacker type named Distributed Attacker (DA in brief). Moreover, we also developed a strategy for symbolic evaluation of our attacker model using First-Order Logic (FOL) and an automatic theorem prover. Lastly, we present scenarios formally analysed with our methodology, including cases we could not have with standard Dolev-Yao or Multi-Attacker models. For instance, our most interesting scenario is when several attackers gather only pieces of an user's credentials and, by putting together their knowledge, collude to attack this user's email account.<br> / Protocolos de segurança são subconjuntos das chamadas cerimônias de segurança. Atualmente não se tem uma linguagem de descrição e um modelo de ameaça detalhado para cerimônias de segurança, necessários para o uso de métodos de avaliação simbólica e verificação de suposições presentes em cerimônias. O objetivo desta dissertação é contribuir com uma sintaxe para descrição de mensagens de cerimônias e apropriado modelo de ameaça a fim de estabelecer a proposta para um novo tipo de atacante (nomeado Atacante Distribuído). Adicionalmente, uma estratégia para execução de avaliação simbólica também foi desenvolvida, utilizando lógica de primeira ordem e um provador de teoremas automático. Por fim, cenários formalmente analisados com o modelo de atacante proposto são exibidos, incluindo casos não passíveis de serem simulados com modelos padrão como Dolev-Yao ou Multi-Attacker. Por exemplo, o caso mais interessante é o que apresenta vários atacantes com conhecimento apenas de partes das credenciais de um usuário, mas que ao colaborar entre si conseguem atacar a conta de email desse usuário.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufsc.br:123456789/176799 |
| Date | January 2017 |
| Creators | Martimiano, Taciane |
| Contributors | Universidade Federal de Santa Catarina, Martina, Jean Everson, Moraes, Ricardo Alexandre Reinaldo de |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | 89 p.| il., tabs. |
| Source | reponame:Repositório Institucional da UFSC, instname:Universidade Federal de Santa Catarina, instacron:UFSC |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0019 seconds