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.
In order to set up a list of libraries that you have access to,
you must first login
or sign up.
Then set up a personal list of libraries from your profile page by
clicking on your user name at the top right of any screen.