Skip to content

Latest commit

 

History

History
37 lines (25 loc) · 2.31 KB

TOPS2020.md

File metadata and controls

37 lines (25 loc) · 2.31 KB
Raw
title paper people peopleOrder
Formal Analysis of Mobile Multi-Factor Authentication with Single Sign-On Login
TOPS2020
RobertoCarbone
SilvioRanise
GiadaSciarretta
LucaViganò
surname

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.