Proving and analysing security protocols with Scyther

Speaker : Guillaume Nibert
Sorbonne Université
Date: 10/05/2023
Time: 10:30 am - 11:30 am
Location: Room 4B01


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.

Source code:


[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: [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: [accessed on May 4, 2023]