Verification of cryptographic protocols implemented in Java Card

A large number of cryptographic protocols have been specified and implemented. However, many of them have been shown to be flawed, even long after they were published. This has generated a line of works concerning the formal specification and verification of protocols, e.g., Casper, Capsl, Casrul. Still, all these techniques and tools are based on conceptual views (or models) of protocols and provide no guarantee on their actual implementation. This paper reports on a method and analysis tool whose goal is precisely to bridge the gap between protocol models that can be proven flawless and their implementation. Our target in this work is Java Card applets: In this case, applications on a card represent principals involved in authentication protocols, with strong security requirements. We have defined a domain-specific language, called DEXTRA, for expressing requirements regarding the implementation of a protocol in Java Card. We have also developed a prototype analyzer to verify the compliance of a Java Card applet with respect to such a specification of a protocol implementation. The verifier relies on static program analysis techniques.