Privacy promises that can be kept: a policy analysis method with application to the HIPAA privacy rule

Organizations collect personal information from individuals to carry out their business functions. Federal privacy regulations, such as the Health Insurance Portability and Accountability Act (HIPAA), mandate how this collected information can be shared by the organizations. It is thus incumbent upon the organizations to have means to check compliance with the applicable regulations. Prior work by Barth et. al. introduces two notions of compliance, weak compliance (WC) and strong compliance (SC). WC ensures that present requirements of the policy can be met whereas SC also ensures obligations can be met. An action is compliant with a privacy policy if it is both weakly and strongly compliant. However, their definitions of compliance are restricted to only propositional linear temporal logic (pLTL), which cannot feasibly specify HIPAA. To this end, we present a policy specification language based on a restricted subset of first order temporal logic (FOTL) which can capture the privacy requirements of HIPAA. We then formally specify WC and SC for policies of our form. We prove that checking WC is feasible whereas checking SC is undecidable. We then formally specify the property WC entails SC, denoted by Δ, which requires that each weakly compliant action is also strongly compliant. To check whether an action is compliant with such a policy, it is sufficient to only check whether the action is weakly compliant with that policy. We also prove that when a policy ℘ has the Δ-property, the present requirements of the policy reduce to the safety requirements imposed by ℘. We then develop a sound, semi-automated technique for checking whether practical policies have the Δ-property. We finally use HIPAA as a case study to demonstrate the efficacy of our policy analysis technique.