A tableaux method for dolev-yao multi-agent epistemic logic

Fernandez, Luiz Cláudio Frederico

Please use this identifier to cite or link to this item: http://hdl.handle.net/11422/11605

Full metadata record

DC Field	Value	Language
dc.contributor.advisor	Benevides, Mario Roberto Folhadela	-
dc.contributor.author	Fernandez, Luiz Cláudio Frederico	-
dc.date.accessioned	2020-03-24T15:21:01Z	-
dc.date.available	2023-12-21T03:06:57Z	-
dc.date.issued	2018-04	-
dc.identifier.uri	http://hdl.handle.net/11422/11605	-
dc.description.abstract	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.	en
dc.language	eng	pt_BR
dc.publisher	Universidade Federal do Rio de Janeiro	pt_BR
dc.rights	Acesso Aberto	pt_BR
dc.subject	Criptologia	pt_BR
dc.subject	Rede de telecomunicações	pt_BR
dc.subject	Lógica	pt_BR
dc.subject	Segurança	pt_BR
dc.title	A tableaux method for dolev-yao multi-agent epistemic logic	en
dc.title.alternative	Um método tableaux para lógica epistêmica multi-agente dolev-yao	pt_BR
dc.type	Dissertação	pt_BR
dc.contributor.authorLattes	http://lattes.cnpq.br/1827844477217464	pt_BR
dc.contributor.referee1	Zaverucha, Gerson	-
dc.contributor.referee2	Veloso, Sheila Regina Murgel	-
dc.description.resumo	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.	pt_BR
dc.publisher.country	Brasil	pt_BR
dc.publisher.department	Instituto Alberto Luiz Coimbra de Pós-Graduação e Pesquisa de Engenharia	pt_BR
dc.publisher.program	Programa de Pós-Graduação em Engenharia de Sistemas e Computação	pt_BR
dc.publisher.initials	UFRJ	pt_BR
dc.subject.cnpq	CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::MATEMATICA DA COMPUTACAO	pt_BR
dc.embargo.terms	aberto	pt_BR
Appears in Collections:	Engenharia de Sistemas e Computação

Files in This Item:

File	Description	Size	Format
885780.pdf		347.73 kB	Adobe PDF	View/Open

Show simple item record Recommend this item View Statistics

Pantheon Institutional repository