Mac In The Box (MITB)

This is an update of the state of the MITB project following Robert's summer visit and some subsequent formalisation and proof done by Mike.

During his summer visit Robert produced an implementation of Keccak in SML and also two in HOL: keccak.sml, Regarding the HOL implementations, he writes:

Robert also designed a state machine to implement MITB and suggests that a good security property to prove is that the only outputs from MITB that can be produced have the form Hash(some-string). The first design fails this.

Robert also wrote a note which documents what he did during his visits, together with some of his thoughts on possible security proofs: notes_robert.pdf.

Mike has formalised a version of Robert's specification in HOL, parametrised on a function representing the permutation component of the Keccak algorithm ( He has also formalised the hash function separately (Hash defined in

Mike also proved that a temporal logic specification of a possible API is implemented by the state-machine implementation and that Robert's security property holds. There is a draft report on this work (embarrassingly awful proofs are in the file

Next steps


Maintained by Mike Gordon.
This page last updated on Thu Nov 14 2013.