Pantheon Repositório Institucional da UFRJ
Coleta, preserva e divulga a produção acadêmica digital em todas as áreas do conhecimento.
São os ativos do repositório, além de teses e dissertações da UFRJ, artigos científicos, livros eletrônicos, capítulos de livros e trabalhos apresentados em eventos por professores, pesquisadores, funcionários administrativos e alunos de mestrado e doutorado.
Use este identificador para citar ou linkar para este item:
http://hdl.handle.net/11422/13170| Tipo: | Dissertação |
| Título: | Model checking dolev-yao multi-agent epistemic logic |
| Título(s) alternativo(s): | Verificador de modelos para lógica epistêmica Dolev-yao. |
| Autor(es)/Inventor(es): | Oliveira, Anna Carolina Carvalho Moreira de |
| Orientador: | Benevides, Mario Roberto Folhadela |
| Coorientador: | Barbosa, Valmir Carneiro |
| Coorientador: | Lopes, Bruno |
| 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á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 |
| Resumo: | 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 |
| Palavras-chave: | knowledge security logic epistemic strips planning checker |
| Assunto CNPq: | CNPQ::ENGENHARIAS |
| Programa: | Programa de Pós-Graduação em Engenharia de Sistemas e Computação |
| Unidade produtora: | Instituto Alberto Luiz Coimbra de Pós-Graduação e Pesquisa de Engenharia |
| Editora: | Universidade Federal do Rio de Janeiro |
| Data de publicação: | Mar-2018 |
| País de publicação: | Brasil |
| Idioma da publicação: | eng |
| Tipo de acesso: | Acesso Aberto |
| Aparece nas coleções: | Engenharia de Sistemas e Computação |
Arquivos associados a este item:
| Arquivo | Descrição | Tamanho | Formato | |
|---|---|---|---|---|
| AnnaCarolinaCarvalhoMoreiraDeOliveira.pdf | 494.2 kB | Adobe PDF | Visualizar/Abrir |
Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.