Model Checking Dolev-Yao Multi-Agent Epistemic Logic

Utilizamos a internet para quase tudo, inclusive para coisas que exigem um alto nível de sigilo, como por exemplo transações bancárias. Isso nos faz pensar na segurança necessária para manter seguro esse ambiente, que constantemente sofre ataques. Por esse motivo o estudo da criptografia está em constante avanço. Mas além disso é importante também que os protocolos de segurança não contenha vulnerabilidade. Dolev e Yao em 1983 conseguiram perceber que no protocolo de chave pública, que é amplamente utilizado até hoje, é possível um usuário malicioso descobrir o conteúdo de uma comunicação entre outros usuários da rede sem quebra da chave criptográfica, somente através de trocas de mensagens. Baseado no modelo apresentado nesse artigo, nós desenvolvemos uma extensão da lógica epistêmica, que expressa conhecimento e crença, para avaliar se os protocolos são seguros. E em cima desse nosso novo sistema, nós o traduzimos para a linguagem de strips, onde podemos automaticamente testar todas as possíveis ações de um intruso para descobrir se será possível ele conseguir o conteúdo da mensagem. E com esse novo formato do nosso sistema, nós desenvolvemos um verificador de modelo.