Logical Specification of the GLBA and HIPAA Privacy Laws
Henry DeYoung, Deepak Garg, Dilsun Kaynar, and Anupam Datta.
Technical Report CMU-CYLAB-10-007, April 2010.
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.
Technical Report CMU-CyLab-10-008, May 2010.


Reasoning about the Consequences of Authorization Policies in a Linear Epistemic Logic
Henry DeYoung and Frank Pfenning.
Workshop on Foundations of Computer Security (FCS), Los Angeles, California, August 2009.
Extended version available as Technical Report CMU-CS-09-140.


An Authorization Logic with Explicit Time
Henry DeYoung, Deepak Garg, and Frank Pfenning.
21st IEEE Computer Security Foundations Symposium (CSF).
Pittsburgh, Pennsylvania. June, 2008.
Long version with detailed proofs available as Technical Report CMU-CS-07-166.
A Logic for Reasoning About Time-Dependent Access Control Policies
Henry DeYoung.
Senior Research Thesis.
Carnegie Mellon University, May 2008.
Available as Technical Report CMU-CS-08-131.