Accession Number:

ADA571991

Title:

Logical Specification of the GLBA and HIPAA Privacy Laws

Descriptive Note:

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA CYLAB

Personal Author(s):

• DeYoung, Henry
• Garg, Deepak
• Kaynar, Dilsun
• Datta, Anupam

Report Date:

2010-04-29

Pagination or Media Count:

129.0

Abstract:

Despite the wide array of frameworks proposed for the formal specification 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. Specifically, we formalize xx6802 and 6803 of GLBA and xx164.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 xed 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.

Descriptors:

• *ACCOUNTABILITY
• *INFORMATION SECURITY
• *LAW ENFORCEMENT
• HEALTH
• INSURANCE
• LOGIC
• MODELS
• POWER
• REAL TIME
• REQUIREMENTS
• SECURITY
• SPECIFICATIONS

Subject Categories:

• Sociology and Law
• Theoretical Mathematics
• Computer Systems Management and Standards

Distribution Statement:

APPROVED FOR PUBLIC RELEASE