Trusting Trusted hardware:
Towards a Formal Model for Programmable Secure Coprocessors

Sean W. Smith and Vernon Austel
IBM T. J. Watson Research Center
http://www.usenix.org/publications/library/proceedings/ec98/full_papers/smith/smith_html/smith.html

- hardware for full certification at FIPS 140-1 level 4

Generic Secure Coprocessor

Generic secure coprocessor is formed by: Physical tamper causes zeroing the memory.

FLASH contains several layers:

Properties

System Configuration

The system configuration is a tuple of relevant properties: Valid configuration = a configuration that can be reached from a valid configuration through a series of valid transitions
Necessary trust set = those parties who, if they abuse or distribute their secrets, can make it impossible for B to make this distinction

Correctness for architecture components