- Title: A Multi-Layered Methodology to Assist the Secure and Risk-Aware Design of Authentication Protocols: Application to Passwordless Solutions based on eID Cards
- Authors: Marco Pernpruner, Roberto Carbone, Giada Sciarretta and Silvio Ranise
AbstractPassword-based authentication has been extensively proven to suffer from many trivial attacks, mainly based on the fact that users set easy passwords and keep the same ones for every online service. Moreover, in sensitive contexts, online services require not only to securely authenticate users, but also to have guarantees on their real identity. Electronic identity cards (in short, eID cards) are among the most promising techniques to solve these issues, given the security features they are equipped with, which also allow for electronic identification. In this work, we define a methodology to analyse the security and risk of authentication procedures, in order to provide security designers with the information they need to fully understand the security level of their protocols, both from a quantitative and qualitative perspective. For concreteness, we apply the methodology to the world of passwordless authentication relying on eID cards protected with PIN or biometrics. In particular, we analyse two protocols -- based on push notifications and QR codes -- that we have designed to let users authenticate from their personal computer's browser by using their mobile device as a card reader. We also propose some suitable security mitigations and evaluate their role in the context of our protocols.
The state-based layer of our methodology requires to model protocols through the specification language ASLan++, a high-level language that formalizes the interactions between the different protocol roles. These models have then been given in input to SATMC (SAT-based Model Checker), 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 184.108.40.206).
ASLan++ file and analyses outputs are available here.
SATMC + STIATE Plugin + instructions to add STIATE Plugin in Eclipse are available here.
The AVANTSSAR deliverable D2.3 “ASLan++ specification and tutorial” is available here.