Relational Verification of Identity Disclosure Using Alloy
摘要
Data are increasingly released for secondary use, yet identity disclosure remains a persistent concern even after standard de-identification. Disclosure risk often arises not from isolated attributes, but from the relational structure of a release design and its interaction with external information. Statistical guarantees and empirical testing may therefore fail to expose structural risks at design time. This paper treats identity disclosure as a design-level relational property. We model data schemas, de-identification policies, and re-identification assumptions as explicit relations. Disclosure is reduced to a bounded relational reachability problem and analysed using Alloy as an executable verification engine. Satisfiable instances produce concrete disclosure witnesses, while unsatisfiability establishes bounded non-disclosure within the analysed scope. A healthcare-inspired setting illustrates that disclosure can emerge purely from relational composition, even when conventional criteria are satisfied. By recasting identity disclosure as a verifiable relational property, this work complements statistical privacy models with assumption-aware design-time verification. This reframing enables disclosure to be verified at design time, prior to data release.