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

• URL: http://arxiv.org/abs/2502.05530v1
• Date: Sat, 08 Feb 2025 11:29:53 GMT
• Title: User Identification Procedures with Human Mutations: Formal Analysis and Pilot Study (Extended Version)
• Authors: Megha Quamara, Luca Vigano,
• Abstract summary: We 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. As a proof-of-concept, we consider a real-life pilot study involving an AI-driven, virtual receptionist kiosk for authenticating visitors.
• Score: 0.0
• License:
• 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.

Related papers

• A Multi-Level Corroborative Approach for Verification and Validation of Autonomous Robotic Swarms [0.9937570340630559]
  We propose a holistic, multi-level modelling approach for formally verifying and validating autonomous robotic swarms. Our formal macroscopic models, used for verification, are characterized by data derived from actual simulations. Our work combines formal verification with experimental validation involving real robots.
  arXiv  Detail & Related papers  (2024-07-22T08:40:05Z)
• Analyzing Adversarial Inputs in Deep Reinforcement Learning [53.3760591018817]
  We present a comprehensive analysis of the characterization of adversarial inputs, through the lens of formal verification. We introduce a novel metric, the Adversarial Rate, to classify models based on their susceptibility to such perturbations. Our analysis empirically demonstrates how adversarial inputs can affect the safety of a given DRL system with respect to such perturbations.
  arXiv  Detail & Related papers  (2024-02-07T21:58:40Z)
• Biometrics Employing Neural Network [0.0]
  Fingerprints, iris and retina patterns, facial recognition, hand shapes, palm prints, and voice recognition are frequently used forms of biometrics. For systems to be effective and widely accepted, the error rate in recognition and verification must approach zero. Artificial Neural Networks, which simulate the human brain's operations, present themselves as a promising approach.
  arXiv  Detail & Related papers  (2024-02-01T03:59:04Z)
• Online Decision Mediation [72.80902932543474]
  Consider learning a decision support assistant to serve as an intermediary between (oracle) expert behavior and (imperfect) human behavior. In clinical diagnosis, fully-autonomous machine behavior is often beyond ethical affordances.
  arXiv  Detail & Related papers  (2023-10-28T05:59:43Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  This paper aims to improve model-based anomaly detection in CPPS by combining the learned timed automaton with a formal knowledge graph about the system. Both the model and the detected anomalies are described in the knowledge graph in order to allow operators an easier interpretation of the model and the detected anomalies.
  arXiv  Detail & Related papers  (2023-08-25T15:25:57Z)
• Interactive System-wise Anomaly Detection [66.3766756452743]
  Anomaly detection plays a fundamental role in various applications. It is challenging for existing methods to handle the scenarios where the instances are systems whose characteristics are not readily observed as data. We develop an end-to-end approach which includes an encoder-decoder module that learns system embeddings.
  arXiv  Detail & Related papers  (2023-04-21T02:20:24Z)
• Towards Assessing and Characterizing the Semantic Robustness of Face Recognition [55.258476405537344]
  Face Recognition Models (FRMs) based on Deep Neural Networks (DNNs) inherit this vulnerability. We propose a methodology for assessing and characterizing the robustness of FRMs against semantic perturbations to their input.
  arXiv  Detail & Related papers  (2022-02-10T12:22:09Z)
• Data-driven behavioural biometrics for continuous and adaptive user verification using Smartphone and Smartwatch [0.0]
  We propose an algorithm to blend behavioural biometrics with multi-factor authentication (MFA) This work proposes a two-step user verification algorithm that verifies the user's identity using motion-based biometrics.
  arXiv  Detail & Related papers  (2021-10-07T02:46:21Z)
• Evaluating the Safety of Deep Reinforcement Learning Models using Semi-Formal Verification [81.32981236437395]
  We present a semi-formal verification approach for decision-making tasks based on interval analysis. Our method obtains comparable results over standard benchmarks with respect to formal verifiers. Our approach allows to efficiently evaluate safety properties for decision-making models in practical applications.
  arXiv  Detail & Related papers  (2020-10-19T11:18:06Z)
• Towards Quantum-Secure Authentication and Key Agreement via Abstract Multi-Agent Interaction [7.673465837624366]
  Current methods for authentication and key agreement based on public-key cryptography are vulnerable to quantum computing. We propose a novel approach based on artificial intelligence research in which communicating parties are viewed as autonomous agents. We release PyAMI, a prototype authentication and key agreement system based on the proposed method.
  arXiv  Detail & Related papers  (2020-07-18T04:22:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.