audit-cylab-tr

Privacy Policy Specification and Audit in a Fixed-Point Logic - How to enforce HIPAA, GLBA and all that Henry DeYoung, Deepak Garg, Limin Jia, Dilsun Kaynar, Anupam Datta May 11, 2010 CMU-CyLab-10-008 CyLab Carnegie Mellon University Pittsburgh, PA 15213 Privacy Policy Speci cation and Audit in a Fixed-Point Logic{ How to enforce HIPAA, GLBA and all thatHenry DeYoung Deepak Garg Limin Jia Dilsun Kaynar Anupam DattaMay 12, 2010AbstractOrganizations such as hospitals and banks that collect and use personal information are required tocomply 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 logicLFP with operators of linear temporal logic. We model organizational processes by assigning role-basedresponsibilities 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 responsibilitiesthat meet this criterion. Policy enforcement is achieved through a combination of techniques: (a) adesign-time analysis of the organizational process to show that the privacy policy is ...