| Speaker : | Guillaume Nibert |
| Sorbonne Université | |
| Date: | 10/05/2023 |
| Time: | 10:30 am - 11:30 am |
| Location: | Room 4B01 |
Abstract
Scyther is an open source Python tool for proving and verifying security protocols. It offers the possibility to integrate adversaries to compromise protocols and to visualise the result associated with the corruption of these protocols. It has also been used to analyse the IKEv1 and IKEv2 protocols [1] used in VPNs and various authentication protocols [2]. In this workshop we will learn how to use the tool and prove some protocols.
Website: https://people.cispa.io/cas.cremers/scyther/index.html
Source code: https://github.com/cascremers/scyther
References:
[1] C. Cremers, Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2 in Computer Security–ESORICS 2011: 16th European Symposium on Research in Computer Security, Leuven, Belgium, September 12-14, 2011. Proceedings 16, Springer, 2011, pp. 315–334. Available at: https://people.cispa.io/cas.cremers/downloads/papers/Cr2011-IKE.pdf [accessed on May 4, 2023]
[2] [1] D. Basin, C. Cremers, and S. Meier, Provably repairing the ISO/IEC 9798 standard for entity authentication, Journal of Computer Security, vol. 21, no. 6, pp. 817–846, 2013. Available at: https://people.cispa.io/cas.cremers/downloads/papers/BCM2012-iso9798.pdf [accessed on May 4, 2023]