An Automatically Verified Prototype of the Tokeneer ID Station Specification