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

Maintained by
Mike
Gordon.

This page last updated on Thu Nov 14 2013.