Verificação Automática dos Protocolos de Segurança Needham-Schroeder, WMF e CSA com a ferramenta Scyther

Abstract

Protocolos de segurança (e.g., Needham-Schroeder, WMF, CSA, SSH,TLS) representam o alicerce das comunicações do mundo atual. Um dos desafiosde projeto destes protocolos é garantir a sua própria segurança. Felizmente,existem ferramentas desenvolvidas especificamente para a verificação formal eautomática de protocolos de segurança, como a Scyther, CryptoVerif, AVISPA eTamarim Prover. Entretanto, estas ferramentas são ainda pouco conhecidas eutilizadas na prática por projetistas de protocolos e estudantes de computação.Este trabalho tem por objetivo contribuir para diminuir esta lacuna através daintrodução e demonstração prática de utilização da ferramenta Scyther, desenvolvidapara auxiliar na verificação automática de protocolos de segurança,utilizando três protocolos distintos (Needham-Schroeder, WMF e CSA).