Confidentiality for mobile code: The case of a simple payment protocol

We propose an approach to support confidentiality for mobile implementations of security-sensitive protocols us-ing Java/JVM. An applet which receives and passes on con-fidential information onto a public network has a rich set of direct and indirect channels available to it. The problem is to constrain applet behaviour to prevent those leakages that are unintended while preserving those that are specified in the protocol. We use an approach based on the idea of cor-relating changes in observable behaviour with changes in input. In the special case where no changes in (low) be-haviour are possible we retrieve a version of noninterfer-ence. Mapping our approach to JVM a number of particular concerns need to be addressed, including the use of object libraries for IO, the use of labelling to track input/output of secrets, and the choice of proof strategy. We use the bisimu-lation proof technique. To provide user feedback we employ a variant of proof-carrying code to instrument a security assistant which will let users of an applet inquire about its security properties such as the destination of data input into different fields. 1