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, keccak2.ml. Regarding the HOL implementations, he writes:

The first one is a bit closer to the reference implementation (not the specification!), while the second one is implemented in a slightly more clever way. (I'd recommend using the second one as a starting point for the implementation, and using keccak_ml/keccak_hol.sml, written in SML, as a starting point for the specification).

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 (MITB.ml). He has also formalised the hash function separately (Hash defined in sponge.ml).

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).

Next steps

• Prove various sanity checking properties in spongeScript.sml to validate the specification of Hash. [Done]
• Fix the MITB design and then verify Robert's security property that the only outputs are hashes. [Done]
• Prove an implementation meets the specification. [Done]
• Formalise the Keccak reference specification in HOL (starting from Section 2 of keccak.pdf).
• Get version of Robert's Keccak permutation plugged into the MITB model.
• Design and verify RTL level hardware (represented in HOL) that implements Robert's MITB machine.