Jul 20th, 2012
Addition of SPARKSkein to SPARK Library
A new package, SPARK.Crypto, has been added to the SPARK library. The top level package contains basic type definitions. The child package SPARK.Crypto.Hash.Skein contains a SPARK implementation of the Skein secure cryptographic hash algorithm. The implementation has been proved free from runtime exceptions, and the proof artefacts are included with the code in the library. For more information see http://www.skein-hash.info.