caa a22 4500 475797604 CHVBK 20180406123728.0 cr unu---uuuuu 170329e20001201xx s 000 0 eng 10.1023/A:1026538301096 doi (NATIONALLICENCE)springer-10.1023/A:1026538301096 The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications [Elektronische Daten] [Denis Sabatier, Pierre Lartigue] 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 applications is paramount, the use of the B formal method brings high confidence and provides mathematical proof that the design of the transaction mechanism fulfills the security requirements. Kluwer Academic Publishers, 2000 smart card nationallicence B method nationallicence proof nationallicence backup nationallicence rollback nationallicence transaction nationallicence EEPROM nationallicence Sabatier Denis Steria Méditerranée—Equipe AtelierB 530, rue F.Joliot, 13791, Aix-en-Provence, France aut Lartigue Pierre Gemplus Research Lab—Av Pic de Bertagne, 13881, Gemenos, France aut Formal Methods in System Design Kluwer Academic Publishers 17/3(2000-12-01), 245-272 0925-9856 17:3<245 2000 17 10703 https://doi.org/10.1023/A:1026538301096 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1026538301096 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Sabatier Denis Steria Méditerranée—Equipe AtelierB 530, rue F.Joliot, 13791, Aix-en-Provence, France aut NATIONALLICENCE 700 1- Lartigue Pierre Gemplus Research Lab—Av Pic de Bertagne, 13881, Gemenos, France aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 17/3(2000-12-01), 245-272 0925-9856 17:3<245 2000 17 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer