- Title: Formal Analysis of Mobile Multi-Factor Authentication with Single Sign-On Login
- Authors: Roberto Carbone, Silvio Ranise, Giada Sciarretta, Luca Viganò
- DOI: 10.1145/3386685
- Acceptance News: Link
Abstract
Over the last few years, there has been an almost exponential increase in the number of mobile applications that deal with sensitive data, such as applications for e-commerce or health. When dealing with sensitive data, classical authentication solutions based on username-password pairs are not enough, and multi-factor authentication solutions that combine two or more authentication factors of different categories are required instead. Even if several solutions are currently used, their security analyses have been performed informally or semi-formally at best, and without a reference model and a precise definition of the multi-factor authentication property. This makes a comparison among the different solutions both complex and potentially misleading. In this paper, we first present the design of two reference models for native applications based on the requirements of two real-world use-case scenarios. Common features between them are the use of one-time password approaches and the support of a single sign-on experience. Then, we provide a formal specification of our threat model and the security goals, and discuss the automated security analysis that we performed. Our formal analysis validates the security goals of the two reference models we propose and provides an important building block for the formal analysis of different multi-factor authentication solutions.Complementary Material
ASLan++ Specs
In our paper, we present two reference models that we have derived from two real use-case scenarios (see Section 4):
- RM_TOTP, which involves mobile native applications and the use of a Time-based OTP approach, and
- RM_CR, which involves an electronic identity card and a Challenge-Response approach.
To analyze these reference models, we have modeled them using ASLan++, a high-level language that formalizes the interactions between the different protocol roles.
For both the reference models we have performed three different analyses: on the security assumptions and on the multi-factor and OTP goals (see Section 6).
Download:
-
The AVANTSSAR deliverable D2.3 “ASLan++ specification and tutorial” is available here.
-
ASLan++ file and analyses performed for RM_TOTP are available here.
-
ASLan++ file and analyses performed for RM_CR are available here.
Tools
SATMC (SAT-based Model Checker) is an open and flexible platform for model-checking security protocols via reduction to SAT. SATMC takes as input a security protocol and can determine whether the concurrent execution of a finite number of sessions of the specified protocol satisfies the expected security properties inspite of the interference of a malicious intruder. The verification of the security properties is performed interfacing with state-of-the-art SAT solvers (MiniSat and zChaff are currently supported) and is based on the use of LTL logic.
For our analyses, we used SATMC (Version 3.5.7) launched within Eclipse using the STIATE Plugin (Version 1.0.0.1).
Download:
- SATMC + STIATE Plugin + instructions to add STIATE Plugin in Eclipse are available here.
