| title | paper | people | ||||
|---|---|---|---|---|---|---|
An Automated Multi-Layered Methodology to Assist the Secure and Risk-Aware Design of Multi-Factor Authentication Protocols |
TDSC2022 |
|
{% include toc.md %}
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). |
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.
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. |