Formal Specification and Analysis of the MIDP 3.0 Security Model

The Mobile Information Device Profile (MIDP) of the Java Platform Micro Edition (JME), provides a standard run-time environment for mobile phones and personal digital assistants. The third and latest version of MIDP introduces anew dimension in the security model of MIDP at the application level. For the second version of MIDP, Zanella, Betarte and Luna had proposed a formal specification of the security model in the Calculus of Inductive Constructions using the Coq Proof Assistant. This paper presents an extension of that formal specification that incorporates the changes introduced in the third version of MIDP. The obtained specification it is proven to preserve the security properties of the second version of MIDP and enables the research of new security properties for the version 3.0 of the profile.