Smartcard Diagnostics Software Programs

Smartcard PC/SC Diagnostic Program - This smartcard diagnosis tool allows checking your smart card reader configuration and is able to generate a report.

JCAVE - A tool for model checking of JavaCard applets against correctness specifications in Linear Temporal Logic (LTL)

JCAVE is a framework for model checking JavaCard applets on the bytecode level. From a set of JavaCard applets it extracts their method call graphs using a static analysis tool. The resulting structure is translated into a pushdown system for which the model checking problem for Linear Temporal Logic (LTL) is decidable, and for which there are efficient model checking tools available.

The model checking approach is tailored to the analysis of inter applet (intra card) communications and can also be used to check behavioural properties of individual applets.

The JavaCard Applet Verification Environment is a set of tools that are connected together in a single verification framework. A small shell-like script has been implemented in order to connect the Static Analysis Tool with the model checker. It will be further referred to as the Applet Verifier script or simply as the Applet Verifier.