This page contains complementary material related to the following paper:

• Title: An Automated Multi-Layered Methodology to Assist the Secure and Risk-Aware Design of Multi-Factor Authentication Protocols
• Authors: Marco Pernpruner, Roberto Carbone, Giada Sciarretta, Silvio Ranise
• DOI: 10.1109/TDSC.2023.3296210
• Acceptance News: Link

Abstract

Authentication protocols represent the entry point to online services, so they must be sturdily designed in order to allow only authorized users to access the underlying data. However, designing authentication protocols is a complex process: security designers should carefully select the technologies to involve and integrate them properly in order to prevent potential vulnerabilities. In addition, these choices are usually restricted by further factors, such as the requirements associated with the scenario, the regulatory framework, the dimensions to balance (e.g., security vs. usability), and the standards to rely on. We come to the rescue by presenting an automated multi-layered methodology we have developed to assist security designers in this phase: by repeatedly evaluating their protocols, they can select the security mitigations to consider until they reach the desired security level, thus enabling a security-by-design approach. For concreteness, we also show how we have applied our methodology to a real use case scenario in the context of a collaboration with the Italian Government Printing Office and Mint.

Complementary Material

Threat Model

Considering Table 3, which displays the threat model that we have identified for our analyses, we now show the relationship between the Authentication Threats identified by NIST and our threat model.

Authentication Threat in NIST SP 800-63B	Attacker in our threat model
Assertion Manufacture or Modification	Not considered, since the authentication assertion is digitally signed by the IdPServer and cannot be tampered with.
Theft	Considered in PCT, MDT and CT.
Duplication	Considered in D, though eID cards cannot be duplicated due to EA3.
Eavesdropping	Considered in ES.
Offline Cracking	Not considered, due to the restricted number of possible attempts while inserting the eID card's PIN.
Side Channel Attack	Not considered, as the eID card's private key cannot be extracted (due to EA4).
Phishing	Considered in SE, MB and MM.
Social Engineering	Considered in SE.
Online Guessing	Not considered, due to the restricted number of possible attempts while inserting the eID card's PIN and the OTP.
Endpoint Compromise	Considered in MB and MM.
Unauthorized Binding	Not considered, as eID cards can be associated only to their legitimate owners (due to EA1).

Symbolic Analysis

The symbolic 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 1.0.0.1).

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.

Approximations

When formally modelling the use case scenario, we have adopted the following approximations:

In the real protocol...	In the formal model...
The IdPServer sends a webpage to the browser (steps 6, 24b).	The IdPServer sends itself (the entity IdPServer) to the browser.
The browser displays a webpage to the user (steps 7, 24c).	The browser sends itself (the entity Browser) to the user.
The user inserts her userId in the browser (step 8).	The user sends herself (the entity User) to the browser.
The eICApp displays an activity to the user (steps 14, 24a).	The eICApp sends itself (the entity EICApp) to the user.
The user reads the QR code through the eICApp (step 12), which extracts the parameters and uses them to generate the challenge (13).	The user sends to the eICApp the parameters to generate the challenge.
The user places the eID card near the mobile device in order to make them interact through NFC.	The user sends a specific string (useEIC) to the eID card.
The interaction between the eICApp the the eID cards occurs in 4 steps: the former sends the PIN (step 17), the latter sends a feedback on its correctness (step 18), the former sends the challenge (step 19) and the latter sends both its certificate and the response (step 20).	The PIN and the challenge are sent at the same time; the eID card provides the response only if the PIN is correct.
In addition to the challenge, the eICApp sends the eID card's certificate to the IdPServer (step 21).	Public keys are supposed to be known, so there is no need to send the eID card's certificate.