Formal specification and verification of control software for cryptographic equipment
D. Richard Kuhn, James F. Dray · 2002
A description is given of the application of formal specification and verification methods to two microprocessor-based cryptographic devices: a 'smart token' system that controls access to a network of workstations, and a message authentication device implementing the ANSI X9.9 message authentication standard. Formal specification and verification were found to be practical, cost-effective tools for detecting potential security weaknesses, and helped to significantly strengthen the security of the access control system.>