Undertaking the Tokeneer Challenge in Event-B

This paper describes a case study on the use of a formal methods tool for checking security properties of Tokeneer, a U. S. National Security Agency (NSA) project developed by Praxis, and released in 2008. We modelled Tokeneer as a series of abstract mathematical models related re fi nement steps in Event-B. We used the Rodin toolset for modelling Tokeneer in Event-B and for discharging associated proof obligations, and we used the EventB2Java code generator to generate Java code for the Event-B model of Tokeneer. After that, we wrote a series of JUnit tests to validate if the Java implementation of Tokeneer adhered to the security properties of Tokeneer described in the documentation provided by Praxis. To the best of our knowledge, modelling Tokeneer in Event-B and checking that its implementation adheres to those security properties is something that hasn't been attempted before.