A formal model of access control for mobile interactive devices

Abstract. This paper presents an access control model for program-ming applications in which the access control to resources can employ user interaction to obtain the necessary permissions. This model is in-spired by and improves on the Java security architecture used in Java-enabled mobile telephones. We consider access control permissions with multiplicities in order to allow to use a permission a certain number of times. An operational semantics of the model and a formal definition of what it means for an application to respect the security model is given. A static analysis which enforces the security model is defined and proved correct. A constraint solving algorithm implementing the analysis is pre-sented.