The Tokeneer Project

Download Tokeneer...
23.2MB zip File

Here’s what’s included:

  • The “Core” Tokeneer ID System Software
  • The test cases derived from the system test specification
  • The “Support” Tokeneer ID System Software
  • The test tokens and biometric data
  • The project documents

Tools to get the most out of Tokeneer

SPARK Toolset

In order to reproduce the proofs for Tokeneer, create new proofs, or change Tokeneer and prove properties in the updated version you will need the SPARK Toolset.

You can use the SPARK Pro toolset:
If you are a free software developer or an academic you can use the SPARK GPL 2012 edition toolset available on AdaCore’s Libre site.

 

Ada Development Environment

To run Tokeneer (currently available on Windows only) you will need an Ada compiler such as the one that comes with the GNAT Pro Ada Development Environment.

If you are a free software developer or an academic you can use the compiler in the latest GNAT GPL release available from AdaCore’s Libre site.

Specialized Tools for Type Checking and Formatting Z Documents

Three of the Tokeneer project documents use the Z notation. To reproduce or modify these documents, you will need the MikTex typesetting system and the FUZZ typechecker.