Model checking dolev-yao multi-agent epistemic logic
Anna Carolina Carvalho Moreira de Oliveira · 2018
Utilizamos a internet para quase tudo, inclusive para coisas que exigem um alto nivel de sigilo, como por exemplo transacoes bancarias. Isso nos faz pensar na seguranca necessaria para manter seguro esse ambiente, que constantemente sofre ataques. Por esse motivo o estudo da criptografia esta em constante avanco. Mas alem disso e importante tambem que os protocolos de seguranca nao contenha vulnerabilidade. Dolev e Yao em 1983 conseguiram perceber que no protocolo de chave publica, que e amplamente utilizado ate hoje, e possivel um usuario malicioso descobrir o conteudo de uma comunicacao entre outros usuario da rede sem quebra da chave criptografica, somente atraves de trocas de mensagens. Baseado no modelo apresentado nesse artigo, nos desenvolvemos uma extensao da logica epistemica, que expressa conhecimento e crenca, para avaliar se os protocolos sao seguros. E em cima desse nosso novo sistema, nos o traduzimos para a linguagem de strips, onde podemos automaticamente testar todas as possiveis acoes de um intruso para descobrir se sera possivel ele conseguir o conteudo da mensagem. E com esse novo formato do nosso sistema, nos desenvolvemos um verificador de modelo