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

TL;DR

The paper tackles how human errors affect user identification procedures by modeling them as security ceremonies and extending the mutation-based analysis to include a new disorder mutation. It automates analysis with the X-Men tool (an extension of the Tamarin Prover) to automatically generate and test mutated ceremony models, demonstrated on a two-factor authentication case study using an AI-driven receptionist kiosk. Key contributions include introducing disorder as a mutation, extending X-Men, and validating the approach through a pilot study that uncovers vulnerabilities arising from visitor mistakes. The work advances rigorous, automated, human-centric security analysis and points to timing and compositional extensions for more comprehensive end-to-end ceremony validation.

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.

Figures (6)

• Figure 1: Sequence diagram showing RK's expected behavior when a Guest requests building access.
• Figure 2: Role-scripts for the UI ceremony agents.
• Figure 3: Agent rules for agent $G$ in UI ceremony.
• Figure 5: Tool support architecture and approach artefacts.
• Figure 6: Three attack scenarios for the UI ceremony.