User Identification Procedures with Human Mutations: Formal Analysis and Pilot Study (Extended Version)

TL;DR

This paper presents a formal, human-centric analysis of user identification procedures, modeling human errors as mutations, and demonstrates the approach with a pilot study involving an AI-driven virtual receptionist kiosk.

Contribution

It introduces a mutation-based formal analysis method for user identification procedures, implemented in the X-Men tool, to account for human errors affecting system security.

Findings

Successfully modeled human errors in identification procedures

Automated analysis with the X-Men tool detects potential vulnerabilities

Validated approach through a real-world pilot study with a virtual kiosk

Abstract

User identification procedures, essential to the information security of systems, enable system-user interactions by exchanging data through communication links and interfaces to validate and confirm user authenticity. However, human errors can introduce vulnerabilities that may disrupt the intended identification workflow and thus impact system behavior. Therefore, ensuring the integrity of these procedures requires accounting for such erroneous behaviors. We follow a formal, human-centric approach to analyze user identification procedures by modeling them as security ceremonies and apply proven techniques for automatically analyzing such ceremonies. The approach relies on mutation rules to model potential human errors that deviate from expected interactions during the identification process, and is implemented as the X-Men tool, an extension of the Tamarin prover, which automatically generates models with human mutations and implements matching mutations to other ceremony participants for analysis. As a proof-of-concept, we consider a real-life pilot study involving an AI-driven, virtual receptionist kiosk for authenticating visitors.