Tearing Java Cards
Engelbert Hubbers, Wojciech Mostowski, Erik Poll · 2006
This paper reports on investigations into the JAVA CARD transaction mechanism, especially on the interaction with so-called nonatomic methods in the JAVA CARD API. This work started with efforts to develop a formalisation of the transaction mechanism that could be used to formally verify the correctness of applications that use these mechanisms to protect themselves from card tears—the sudden loss of power caused by removing a smart card from a terminal. During work to formalise the JAVA CARD platform we came across ambiguities in the official specification, and subsequent experiments with real cards revealed that behaviour of cards varies a lot, and some JAVA CARDs fail to meet the official specification. We will discuss the outcome of our experiments with real cards and attempts to formalise the official specifications. In particular, we show how we can break the security of the reference implementation of PIN objects on some smart cards, and how our formal specification can be used to verify the behaviour of JAVA CARD code, even in the presence of card tears, using the KeY program verifier or using model checking.