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, keccak2.ml. 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
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 (MITB.ml). He has also formalised the hash function
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 proofs.ml).