Abstract

The widespread use of digital identities in our everyday life, along with the release of sensitive data on many online transactions, calls for Identity Management (IdM) solutions that are secure, privacy-aware, and compatible with new technologies, such as mobile and cloud computing. While there exist many secure IdM solutions for web applications, their adaptation in the mobile context is a new and open challenge. The majority of mobile IdM solutions currently used are based on proprietary protocols and their security analysis lacks standardization in the structure, definitions of notions and entities, and specific considerations to identify the attack surface that turns out to be quite different from well understood web scenarios. This makes a comparison among different solutions very complex or, in the worst case, misleading. To overcome these difficulties, we propose a novel methodology for the design and security assessment of mobile IdM solutions. The design space is characterized by the identification of: (i) national (e.g., SPID for Italy) and European (e.g., eIDAS) laws, regulations and guideline principles that are particularly relevant to digital identity and privacy; (ii) a list of security and usability requirements that are related to IdM solutions (e.g., single sign-on and multi-factor authentication); (iii) a set of implementation mechanisms that are relevant to authentication and authorization on mobile devices and simplify the satisfaction of the requirements in (ii). All the designed solutions use as blueprint a reference model resulting from a rational reconstruction of the mobile IdM solution adopted by Facebook and a study of the OAuth specification for native applications. Regarding the security assessment, our methodology supports analyses ranging from semi-formal to formal. For the former, an IdM designer is required to specify the security relevant parts of the protocol using message sequence charts, the threat model and the security properties; these offer the starting point to argue whether the protocol satisfies the specified properties. For the latter, an IdM designer is required to specify the protocol flow, the attacker properties and the security properties using one of the available formal specification languages for the description of cryptographic and browser-based protocols, and verify the security property violations using an automated tool for protocol analysis. To validate our approach, we applied it to four different real-world scenarios that represent different functional and usability requirements: 1. TreC: a multi-factor authentication solution with a single sign-on experience for mobile e-Health applications. 2. Smart Community: a secure delegated access solution in the context of smart-cities. 3. DigiMat-Lab (Istituto Poligrafico e Zecca dello Stato): a mobile multi-factor authentication solution that uses as second factor the Italian electronic identity card. 4. FIDES: an IdM solution that combines federation and cross-border aspects in the context of the European single digital market. The custom designs obtained by applying our methodology in the four scenarios above show the generality and effectiveness of our methodology. When using formal analysis, we have re-used the specification language and tools developed in the context of the AVANTSSAR EU-founded project.