Pantheon Repositorio Institucional
Recopila, preserva y difundi la producción académica digital en todas las áreas del conocimiento.
Comprende los activos del repositorio, además de tesis y disertaciones en la UFRJ, artículos científicos, libros electrónicos, capítulos de libros y trabajos presentados en eventos para los profesores, investigadores, personal administrativo y estudiantes de maestría y doctorado.
Por favor, use este identificador para citar o enlazar este ítem:
http://hdl.handle.net/11422/11605| Especie: | Dissertação |
| Título : | A tableaux method for dolev-yao multi-agent epistemic logic |
| Otros títulos: | Um método tableaux para lógica epistêmica multi-agente dolev-yao |
| Autor(es)/Inventor(es): | Fernandez, Luiz Cláudio Frederico |
| Tutor: | Benevides, Mario Roberto Folhadela |
| Resumen: | Dada a importância dos protocolos de segurança no nosso cotidiano, os esforços para desenvolver mecanismos e modelos para verificação de tais protocolos são sempre relevantes. Neste trabalho, nós propomos a Lógica Epistêmica Multi-Agente Dolev-Yao, uma extensão da Lógica Epistêmica Multi-Agente, destinada para a análise de protocolos de segurança e inspirada no modelo Dolev-Yao, o trabalho precursor sobre criptografia formal. Nós provamos a corretude e completude do nosso sistema, também demonstrando o seu uso. Em seguida, um método tableaux para essa lógica é apresentado, também incluindo sua corretude e completude. Por último, mostramos uma prova de terminação para o nosso método, além de alguns exemplos. |
| Resumen: | Given the increasing importance of security protocols in our daily lives, the efforts to develop mechanisms and models for verification of such protocols are always relevant. In this work, we propose the Dolev-Yao Multi-Agent Epistemic Logic, which is an extension of Multi-Agent Epistemic Logic, aimed to analyze security protocols and inspired by Dolev-Yao model, the seminal work in formal cryptography. We prove the soundness and completeness of our system, also demonstrating its use. Then, a tableaux method for this logic is presented, including the proofs of soundness and completeness. Finally, we provide a termination argument for our method and show some examples. |
| Materia: | Criptologia Rede de telecomunicações Lógica Segurança |
| Materia CNPq: | CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::MATEMATICA DA COMPUTACAO |
| Programa: | Programa de Pós-Graduação em Engenharia de Sistemas e Computação |
| Unidade de producción: | Instituto Alberto Luiz Coimbra de Pós-Graduação e Pesquisa de Engenharia |
| Editor: | Universidade Federal do Rio de Janeiro |
| Fecha de publicación: | abr-2018 |
| País de edición : | Brasil |
| Idioma de publicación: | eng |
| Tipo de acceso : | Acesso Aberto |
| Aparece en las colecciones: | Engenharia de Sistemas e Computação |
Ficheros en este ítem:
| Fichero | Descripción | Tamaño | Formato | |
|---|---|---|---|---|
| 885780.pdf | 347.73 kB | Adobe PDF | Visualizar/Abrir |
Los ítems de DSpace están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.