A tableaux method for dolev-yao multi-agent epistemic logic
Luiz C. F. Fernandez · 2018
Dada a importância dos protocolos de seguranca no nosso cotidiano, os esforcos para desenvolver mecanismos e modelos para verificacao de tais protocolos sao sempre relevantes. Neste trabalho, nos propomos a Logica Epistemica Multi-Agente Dolev-Yao, uma extensao da Logica Epistemica Multi-Agente, destinada para a analise de protocolos de seguranca e inspirada no modelo Dolev-Yao, o trabalho precursor sobre criptografia formal. Nos provamos a corretude e completude do nosso sistema, tambem demonstrando o seu uso. Em seguida, um metodo tableaux para essa logica e apresentado, tambem incluindo sua corretude e completude. Por ultimo, mostramos uma prova de terminacao para o nosso metodo, alem de alguns exemplos.