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.

Author: Mattias Ulbrich, ulbrich@kit.edu