Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Model-Driven Security Analysis of Self-Sovereign Identity Systems

Yepeng Ding, Hiroyuki Sato

TL;DR

The paper addresses the lack of systematic security analysis for self-sovereign identity architectural patterns. It proposes a model-driven framework that formalizes patterns and threats as Labeled Transition Systems on system graphs and verifies security properties via model checking, with automatic generation of Java skeletons. A threat model comprising passive and active attacks is defined and instantiated over eight common SSI patterns, and SecureSSI, a standalone IDE, demonstrates typical vulnerable patterns and attacker models to support practical assessment of SSI deployments. This work enables rigorous, reusable security analysis for evolving SSI architectures and provides tooling to bridge formal verification with real-world implementation.

Abstract

Best practices of self-sovereign identity (SSI) are being intensively explored in academia and industry. Reusable solutions obtained from best practices are generalized as architectural patterns for systematic analysis and design reference, which significantly boosts productivity and increases the dependability of future implementations. For security-sensitive projects, architects make architectural decisions with careful consideration of security issues and solutions based on formal analysis and experiment results. In this paper, we propose a model-driven security analysis framework for analyzing architectural patterns of SSI systems with respect to a threat model built on our investigation of real-world security concerns. Our framework mechanizes a modeling language to formalize patterns and threats with security properties in temporal logic and automatically generates programs for verification via model checking. Besides, we present typical vulnerable patterns verified by SecureSSI, a standalone integrated development environment, integrating commonly used pattern and attacker models to practicalize our framework.

Model-Driven Security Analysis of Self-Sovereign Identity Systems

TL;DR

The paper addresses the lack of systematic security analysis for self-sovereign identity architectural patterns. It proposes a model-driven framework that formalizes patterns and threats as Labeled Transition Systems on system graphs and verifies security properties via model checking, with automatic generation of Java skeletons. A threat model comprising passive and active attacks is defined and instantiated over eight common SSI patterns, and SecureSSI, a standalone IDE, demonstrates typical vulnerable patterns and attacker models to support practical assessment of SSI deployments. This work enables rigorous, reusable security analysis for evolving SSI architectures and provides tooling to bridge formal verification with real-world implementation.

Abstract

Best practices of self-sovereign identity (SSI) are being intensively explored in academia and industry. Reusable solutions obtained from best practices are generalized as architectural patterns for systematic analysis and design reference, which significantly boosts productivity and increases the dependability of future implementations. For security-sensitive projects, architects make architectural decisions with careful consideration of security issues and solutions based on formal analysis and experiment results. In this paper, we propose a model-driven security analysis framework for analyzing architectural patterns of SSI systems with respect to a threat model built on our investigation of real-world security concerns. Our framework mechanizes a modeling language to formalize patterns and threats with security properties in temporal logic and automatically generates programs for verification via model checking. Besides, we present typical vulnerable patterns verified by SecureSSI, a standalone integrated development environment, integrating commonly used pattern and attacker models to practicalize our framework.
Paper Structure (25 sections, 1 theorem, 2 equations, 4 figures, 2 tables)

This paper contains 25 sections, 1 theorem, 2 equations, 4 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Self-Sovereign Identity
  4. Architectural Patterns
  5. Threat Model
  6. Passive Threat Model
  7. Active Threat Model
  8. Model-Driven Analysis
  9. Modeling Method
  10. Structure Modeling
  11. Behavior Modeling
  12. Action Elimination
  13. Behavior Specification
  14. Pattern Modeling
  15. Workflow
  16. ...and 10 more sections

Key Result

Theorem 4.1

For any system graph $\mathfrak{S}$ without terminal state declarators, there is an interpretation based on a labeled transition system defined in Definition def:lts.

Figures (4)

  • Figure 1: Overview of the workflow of modeling architectural patterns.
  • Figure 2: NuSMV running report in Example \ref{['eg:protocol_model']}.
  • Figure 3: The overview of the MitM attack in Example \ref{['eg:threat_model']}.
  • Figure 4: NuSMV running report in Example \ref{['eg:threat_model']}.

Theorems & Definitions (6)

  • Definition 4.1: Labeled Transition System
  • Definition 4.2: System Graph
  • Theorem 4.1: Interpretability
  • proof
  • Example 4.1: Protocol Modeling
  • Example 4.2: Attacker Modeling