En los últimos años el uso de dispositivos móviles tales como teléfonos celulares y asistentes de datos se ha popularizado a nivel mundial. El avance de la tecnología determina como tendencia para los próximos que estos dispositivos tendrán mayor capacidad de procesamiento y almacenamiento, convirtiéndose en elementos esenciales para el mundo de los negocios y el trabajo de las personas. En el desarrollo de sistemas y aplicaciones para dispositivos móviles se hace necesario el uso de una tecnología especializada que tenga en cuenta aspectos tales como las limitaciones de los recursos computacionales, la heterogeneidad de las plataformas de hardware, las comunicaciones móviles y, especialmente, la preservación de la confidencialidad e integridad de los datos personales. La mayor parte de los dispositivos móviles se basa en la edición de la tecnología Java para sistemas integrados, denominada Java 2Micro Edition (J2ME). La característica fundamental de esta edición es el uso de una máquina virtual, especialmente diseñada y adaptada para aprovechar al máximo los escasos recursos con los que cuentan los dispositivos integrados. El presente trabajo analiza formalmente el funcionamiento del módulo que se encarga de controlar el acceso a funciones de un dispositivo móvil. Formalmente denominado en inglés Access Control, el módulo es parte de la dupla configuración-perfil CLDC – MIDP y es utilizado en dispositivos móviles tales como teléfonos celulares, pagers y asistentes de datos personales (PDA’s). Concretamente, el trabajo extiende una especificación formal desarrollada en el Cálculo de Construcciones Inductivas, usando el asistente de pruebas Coq, del modelo de seguridad de MIDP 2.0. Se formaliza el evento de llamada de un método de una suite a una función o API del dispositivo, se demuestra que la extensión es conservativa y se analizan propiedades relevantes de seguridad relativas a la extensión. Finalmente, se refina la especificación junto con la extensión propuesta y se certifica un algoritmo escrito en Coq como una implementación del módulo de control de accesos de MIDP 2.0.