Model-Driven Security Analysis of Self-Sovereign Identity Systems

TL;DR

This paper introduces a model-driven framework for analyzing the security of self-sovereign identity systems, formalizing architectural patterns and threats to improve dependability and security verification.

Contribution

It presents a novel formal analysis framework that automates security verification of SSI architectural patterns using model checking and integrates it into a practical development environment.

Findings

Verified security vulnerabilities in typical SSI patterns

Automated formal verification of security properties

Practical tool for secure SSI system design

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.