Model checking specifications of smart cards

Formally verifying a product in an early phase of the design process has several advantages. First, errors and contradictions in the specification can be found early. Second, an unambiguous common understanding of the specification is created. In summary, the quality and security of a product can be significantly increased. This paper describes how formal verification can be integrated into the industrial design process of a smart card in a practical way. The described method allows to reach high assurance levels in Common Criteria certifications.