Verificação Automática de Protocolos de Segurança com a ferramenta Scyther

• Tadeu Jenuario UNIPAMPA
• João Otávio Chervinski UNIPAMPA
• Giulliano Paz UNIPAMPA
• Diego Kreutz UNIPAMPA

DOI: https://doi.org/10.5753/errc.2019.9233

Resumo

Protocolos de segurança (e.g. Needham-Schroeder, IKE, IPSec, SSH, Kerberos, TLS) representam o alicerce das comunicações do mundo atual. Protocolos como o IKE e o TLS permitem a troca de chaves na internet e propriedades de segurança essenciais para as comunicações (e.g. confidencialidade, integridade e autenticidade). Um dos grandes desafios no projeto desses protocolos é garantir a sua própria segurança, ou seja, garantir que o protocolo seja livre de vulnerabilidades. Atualmente, existem algumas ferramentas desenvolvidas especificamente para a verificação formal automática de protocolos de comunicação e segurança, como a Scyther, CrytoVerif, Tamarin Prover e AVISPA. Entretanto, essas são ainda pouco conhecidas e utilizadas na prática por projetistas de protocolos. Este trabalho tem por objetivo contribuir no fechamento desta lacuna através da introdução e demonstração prática de utilização da ferramenta Scyther, projetada para auxiliar na verificação automática de protocolos de segurança.

Palavras-chave: Análise de protocolos de segurança, Criptografia e criptoanálise: algoritmos, protocolos, técnicas e aplicações Gestão de Identidades

Referências

Affeldt, R. and Marti, N. (2013). Towards Formal Verification of TLS Network Packet Processing Written in C. In 7th PLPV, pages 35–46. ACM.

Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuéllar, J., Drielsma, P. H., Héam, P.-C., Kouchnarenko, O., Mantovani, J., et al. (2005). The AVISPA tool for the automated validation of internet security protocols and applications. In International conference on computer aided verification, pages 281–285. Springer.

Blanchet, B., Smyth, B., Cheval, V., and Sylvestre, M. (2018). ProVerif 2.00: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial. https://bit.ly/2OUlH7f.

Chudnov, A., Collins, N., Cook, B., Dodds, J., Huffman, B., MacCárthaigh, C., Magill, S., Mertens, E., Mullen, E., Tasiran, S., Tomb, A., and Westbrook, E. (2018). Continuous Formal Verification of Amazon s2n. In Computer Aided Verification, pages 430–446.

Cremers, C., Horvat, M., Scott, S., and v. d. Merwe, T. (2016). Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication. In IEEE SP.

Cremers, C. J. F. (2006). Scyther: Semantics and verification of security protocols. Eindhoven University of Technology Eindhoven.

Dalal, N., Shah, J., Hisaria, K., and Jinwala, D. (2010). A comparative analysis of tools for verification of security protocols. Int. J. of Comm., Network and System Sciences, 3(10):779.

Kreutz, D., Yu, J., Ramos, F. M. V., and Esteves-Verissimo, P. (2019). ANCHOR: Logically centralized security for software-defined networks. ACM Trans. Priv. Secur., 22(2):8:1–8:36.

Li, L., Sun, J., Liu, Y., Sun, M., and Dong, J. (2018). A Formal Specification and Verification Framework for Timed Security Protocols. IEEE Trans. on Soft. Engineering, 44(8):725–746.

Lowe, G. (1995). An Attack on the Needham- Schroeder Public- Key Authentication Protocol. Information processing letters, 56(3).

Needham, R. M. and Schroeder, M. D. (1978). Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12):993–999.