MCRL2 PGP protocol model
A formalisation for the PGP protocol has been written as an MCRL2 model by Wytse Oortwijn from the VerCors team. You can find it here.
Event-B Formalisation
I have tried to formalise the natural language requirements into an Event-B model. It is not necessarily complete, and may not be fully in line with the natural language description. But it is a starting point for a discussion.
Formalisation of the key manager This Event-B model is an attempt to formalise the requirements of the VerifyThis Long Term Challenge 2020. It is deliberately kept on a very high level of abstraction, but should have enough detail to clarify the behaviour of the system.
[Read More]
Scala and Java Implementations
In the meantime, two different implementations of the key-server were created.
Gidon Ernst created a Scala version:
I created a full java version (incl. a REST interface)
Author: Alexander Weigl, weigl@kit.edu
Challenge start
At the KeY Symposium 2019 (Manigod, France), the VerifyThis Challenge has been announced.
The challenge is currently rudimentary and will be updated soon.
A mailing list is available for participants: verifythis-ltc@lists.kit.edu.
For question, you can directly get in touch with organisers via the Github issues or email (verifythis-ltc-request@lists.kit.edu).
Good luck.
Marieke Huisman, Raul Monti, Mattias Ulbrich, Alexander Weigl