KRAKATOA is a tool for static verification of Java programs annotated in JML (Java Modeling Language), a behavioral specification language tailored to Java and based on first order predicate logic. In a first step, we show how we modeled the transactions within KRAKATOA, by generating on-the-fly (i.e. on each applet) specifications of the API methods for transactions.

In a second step, we consider security problems that can be caused by a card tear. We propose new JML constructs allowing to express properties to satisfy when a method is interrupted by a card tear, also taking non-atomic methods into account. We present a modeling of these constructs in KRAKATOA, and show it is practicable for the detection of potential security holes, or to prove the absence of risk.