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

Detalhes bibliográficos
Ano de defesa: 2018
Autor(a) principal: Fernandez, Luiz Cláudio Frederico
Orientador(a): Não Informado pela instituição
Banca de defesa: Não Informado pela instituição
Tipo de documento: Dissertação
Tipo de acesso: Acesso aberto
Idioma: eng
Instituição de defesa: Universidade Federal do Rio de Janeiro
Brasil
Instituto Alberto Luiz Coimbra de Pós-Graduação e Pesquisa de Engenharia
Programa de Pós-Graduação em Engenharia de Sistemas e Computação
UFRJ
Programa de Pós-Graduação: Não Informado pela instituição
Departamento: Não Informado pela instituição
País: Não Informado pela instituição
Palavras-chave em Português:
Criptologia
Rede de telecomunicações
Lógica
Segurança
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::MATEMATICA DA COMPUTACAO
Link de acesso: http://hdl.handle.net/11422/11605
Resumo: 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.

Registros relacionados