Informações:

Publicações do PESC

Título
Model Checking Dolev-Yao Multi-Agent Epistemic Logic
Linha de pesquisa
Inteligência Artificial
Tipo de publicação
Dissertação de Mestrado
Número de registro
Data da defesa
27/3/2018
Resumo

Utilizamos a internet para quase tudo, inclusive para coisas que exigem um alto nível de sigilo, como por exemplo transações bancárias. Isso nos faz pensar na segurança necessária para manter seguro esse ambiente, que constantemente sofre ataques. Por esse motivo o estudo da criptografia está em constante avanço. Mas além disso é importante também que os protocolos de segurança não contenha vulnerabilidade. Dolev e Yao em 1983 conseguiram perceber que no protocolo de chave pública, que é amplamente utilizado até hoje, é possível um usuário malicioso descobrir o conteúdo de uma comunicação entre outros usuários da rede sem quebra da chave criptográfica, somente através de trocas de mensagens. Baseado no modelo apresentado nesse artigo, nós desenvolvemos uma extensão da lógica epistêmica, que expressa conhecimento e crença, para avaliar se os protocolos são seguros. E em cima desse nosso novo sistema, nós o traduzimos para a linguagem de strips, onde podemos automaticamente testar todas as possíveis ações de um intruso para descobrir se será possível ele conseguir o conteúdo da mensagem. E com esse novo formato do nosso sistema, nós desenvolvemos um verificador de modelo.

Abstract

We use the web for almost everything, including for actions that require high level of secrecy, for example, banking transactions. It make us think about the necessary security to keep this environment safe, that constantly suffers cyber attacks. For this reason, the study of cryptography is always in advance. Besides, It is important do not have vulnerability in security protocol too. In 1983, Dolev and Yao realize that in public key protocol, which is widely used even nowadays, a malicious user in a network can discover the contents of communications between other users simply by eavesdropping on the exchange of messages. Based on the model introduced in the Dolev and Yao's article, we propose an epistemic logic extension to evaluate if a security protocol is safe. We transcripted this extension to strips language, where we can automatically test every possible intruder actions to discover contents of messages. And with this new notation we developed a model checker.

Arquivo
Topo