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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Relational Verification of Identity Disclosure Using Alloy

  • Seungil Yang,
  • Peter Rivière,
  • Toshiaki Aoki

摘要

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.