The use of the B formal method for the design and the validation of the transaction mechanism for smart card applications

Abstract

This document describes an industrial application of the B method in smart card applications. In smart card memory, data modification may be interrupted due to a card withdrawal or a power loss, the EEPROM memory may result in an unstable state and the values subsequently read, may be erroneous. The transaction mechanism provides a secure means for modifying data located in the EEPROM. As the security in smart card application is paramount, the use of the B formal method brings high confidence and provides mathematical proofs that the design of the transaction mechanism fulfills the security requirements.