  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.
