Pantheon Institutional repository
Collect, preserve and disseminate digital academic production in all areas of knowledge.
Comprise the assets of the repository, in addition to theses and dissertations at UFRJ, scientific articles, electronic books, book chapters and papers presented at events for teachers, researchers, administrative staff and students of master's and doctoral degrees.
Please use this identifier to cite or link to this item:
http://hdl.handle.net/11422/13170| Type: | Dissertação |
| Title: | Model checking dolev-yao multi-agent epistemic logic |
| Other Titles: | Verificador de modelos para lógica epistêmica Dolev-yao. |
| Author(s)/Inventor(s): | Oliveira, Anna Carolina Carvalho Moreira de |
| Advisor: | Benevides, Mario Roberto Folhadela |
| Co-advisor: | Barbosa, Valmir Carneiro |
| Co-advisor: | Lopes, Bruno |
| Abstract: | 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ário 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 |
| Keywords: | knowledge security logic epistemic strips planning checker |
| Subject CNPq: | CNPQ::ENGENHARIAS |
| Program: | Programa de Pós-Graduação em Engenharia de Sistemas e Computação |
| Production unit: | Instituto Alberto Luiz Coimbra de Pós-Graduação e Pesquisa de Engenharia |
| Publisher: | Universidade Federal do Rio de Janeiro |
| Issue Date: | Mar-2018 |
| Publisher country: | Brasil |
| Language: | eng |
| Right access: | Acesso Aberto |
| Appears in Collections: | Engenharia de Sistemas e Computação |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| AnnaCarolinaCarvalhoMoreiraDeOliveira.pdf | 494.2 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.