Certificates of Resource Usage on Mobile Telephones

Resources on Java-enabled mobile telephones are controlled by permissions that grant an applet a certain number of accesses to a resource. Such permissions can be given by the operator or can be obtained dynamically during execution by querying the user interactively. In this talk, we describe a formal model of such interactive access control with an emphasis on how to handle permissions with multiplicities. Based on this model, we present a proof system in which it is possible to engineer a formal proof that an applet will not consume resources for which it does not have permissions. Such proofs will then serve as a basis for constructing compact certificates attesting the correct behaviour of a down-loaded applet.