Logical Specification of the GLBA and HIPAA Privacy Laws (CMU-CyLab-10-007)

Despite the wide array of frameworks proposed for the formal specification and analysis of privacy laws, there has been comparatively little work on expressing large fragments of actual privacy laws in these frameworks. We attempt to bridge this gap by presenting what we believe to be the most complete logical formalizations of the Gramm-Leach-Bliley Act (GLBA) and the Health Insurance Portability and Accountability Act (HIPAA) to date. Specifically, we formalize §§6802 and 6803 of GLBA and §§164.502, 164.506, 164.508, 164.510, 164.512, 164.514, and 164.524 of HIPAA. The remaining sections of both laws are not stated in terms of operational requirements, and therefore cannot be formalized in our model. Along the way, we also give a novel extension of an existing privacy logic with real-time features and fixed point operators; these provide the expressive power necessary to capture legal clauses found in GLBA and HIPAA involving bounded-time obligations and reuse of information.