Accession Number:



Privacy Policy Specification and Audit in a Fixed-Point Logic - How to Enforce HIPAA, GLBA and All That

Descriptive Note:

Corporate Author:


Report Date:


Pagination or Media Count:



Organizations such as hospitals and banks that collect and use personal information are required to comply with privacy regulations like the Health Insurance Portability and Accountability Act HIPAA and the Gramm-Leach-Bliley Act GLBA. With the goal of speci cation and enforcement of such prac- tical policies, we develop the logic PrivacyLFP, whose syntax is an extension of the xed point logic LFP with operators of linear temporal logic. We model organizational processes by assigning role-based responsibilities to agents that are also expressed in the same logic. To aid in designing such processes we develop a semantic locality criterion to characterize responsibilities that agents or groups of agents have a strategy to discharge, and easily checkable, sound syntactic characterizations of responsibilities that meet this criterion. Policy enforcement is achieved through a combination of techniques a a design-time analysis of the organizational process to show that the privacy policy is respected if all agents act responsibly, using a sound proof system we develop for PrivacyLFP and b a posthoc audit of logs of organizational activity that identi es agents who did not live up to their responsibilities, using a model checking procedure we develop for PrivacyLFP. We illustrate these enforcement techniques using a representative example of an organizational process.

Subject Categories:

  • Theoretical Mathematics
  • Computer Systems Management and Standards

Distribution Statement: