Análise do modelo de ataques ao protocolo Signal: uma abordagem usando lógica e mCRL2

Figueiredo, André Gustavo Lima; Lourenço, Vanessa Escócio

Please use this identifier to cite or link to this item:


			http://hdl.handle.net/11422/13432

Type:	Trabalho de conclusão de graduação
Title:	Análise do modelo de ataques ao protocolo Signal: uma abordagem usando lógica e mCRL2
Author(s)/Inventor(s):	Figueiredo, André Gustavo Lima Lourenço, Vanessa Escócio
Advisor:	Benevides, Mário Roberto Folhadela
Co-advisor:	Bastos, Valéria Menezes
Abstract:	O objetivo deste trabalho foi analisar possíveis ataques ao protocolo Signal através de modelagens utilizando a ferramenta mCRL2. O protocolo Signal é constituído pelos protocolos Extended Triple Diffie-Hellman e o Double Ratchet, ambos criados em 2013. O Signal, um dos primeiros protocolos a implementar criptografia ponta-a-ponta, é amplamente utilizado nos principais aplicativos de troca de mensagens, como o Whatsapp. Devido à sua popularidade, o protocolo foi escolhido neste trabalho para verificarmos se ele é realmente seguro, ou seja, se um invasor pode interceptar todas as mensagens trocadas entre dois usuários. A ferramenta mCRL2 permitiu a especificação, visualização, simulação e verificação formal do protocolo. Neste trabalho discutimos algumas estratégias de interceptações conhecidas, juntamente com uma análise dos resultados obtidos com o uso da ferramenta mCRL2.
Keywords:	Protocolos de comunicação Criptologia mCRL2 (linguagem de especificação)
Subject CNPq:	CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::MATEMATICA DA COMPUTACAO
Production unit:	Instituto de Computação
Publisher:	Universidade Federal do Rio de Janeiro
Issue Date:	16-Jun-2020
Publisher country:	Brasil
Language:	por
Right access:	Acesso Aberto
Appears in Collections:	Ciência da Computação

Files in This Item:

File	Description	Size	Format
AGLFigueiredo.pdf		1 MB	Adobe PDF	View/Open

Show full item record Recommend this item View Statistics

Pantheon Institutional repository