Formal Modeling of Security Policies for Mobile Access Solutions

Abstract

[EN] Current technology allows us to have a great deal of computation power in the palm of our hand in the form of smartphones. Such powerful and versatile devices are the perfect tools to, e.g., authenticate users in both virtual and physical systems. Key2phone is a smartphone solution designed to facilitate authorized users to access restricted spaces by turning their smartphones into electronic keys. This master’s thesis focuses on the study of the safety and security properties of the Key2phone electronic lock. First, a model of the Key2phone protocol is implemented by using the Maude language, which is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming. Then, a reachability analysis is performed in the Maude system, which ensures the safety of the system by proving that no states considered unsafe can be reached. Finally, liveness properties are checked by using the Maude LTL logical model checker (LMC).

El objetivo de este trabajo es realizar el análisis y elicitación de requisitos de seguridad y protección que deben ser considerados para un sistema de interacción y gestión de accesos que convierte el teléfono móvil en una llave para cerraduras electrónicas, puertas y portones. Se parte de una especificación de requisitos inicial que, en primer lugar, será revisada y completada para, posteriormente, proceder a su validación mediante alguna herramienta de análisis de sistemas de transición o comprobación de modelos.

[CA] La tecnologia actual ens permet tindre un gran potencial de computaci´o en la palma de la m`a. Estos dispositius, vers`atils i potents, s´on la ferramenta perfecta per a, per exemple, autoritzar usuaris tant en sistemes virtuals com a f´ısics. Key2phone ´es una soluci´o per a smartphone dissenyada per a facilitar l’acc´es d’usuaris autoritzats a espais restringits, convertint els seus smartphones en claus electr`oniques. Esta tesi de m`aster se centra en l’estudi de les propietats de seguretat del sistema Key2phone usant el llenguatge de programaci´o Maude, que ´es un llenguatge reflectiu d’alt rendiment que suporta programaci´o i especificacions tant de l`ogica ecuacional com de reescriptura. Llavors, es realitza una an`alisi d’alcanzabilidad, que comprova la seguretat del sistema, provant que no s’aconseguixen estats del sistema considerats insegurs. Finalment, es verifiquen propietats de vivor i seguretat usant la ferramenta Maude LTL logical model checker (LMC).