Published papers are copyrights of their respective
- Experiences in
the logical specification of the HIPAA and GLBA privacy
laws. With Henry DeYoung, Limin Jia, Dilsun Kaynar,
and Anupam Datta. Workshop on Privacy in the Electronic
version: Technical report CMU-CyLab-10-007].
authorization logic - proof theory and a case
study. With Frank Pfenning. International Workshop
on Security and Trust Management (STM), LNCS Volume
6710, 2010. For details and proofs see chapters 4 and 8 of
my dissertation. © Springer-Verlag
system security with interface-confined
adversaries. With Jason Franklin, Dilsun Kaynar, and
Anupam Datta. Electronic Notes in Theoretical Computer
Science (ENTCS), Volume 265: Proceedings of the 26th
Conference on Mathematical Foundations of Programming
Semantics (MFPS), 2010. [Full version:
Technical Report CMU-CyLab-10-004]. © Elsevier
- A proof-carrying file
system. With Frank Pfenning. IEEE Symposium on
Security and Privacy (Oakland), 2010. [Implementation] [Expanded, outdated
version: Technical Report CMU-CS-09-123] For details
and proofs see chapters 4, 5 and 7 of my dissertation. © IEEE
Technical reports related to published papers are listed
above with their respective papers.
specification and audit in a fixed-point logic - How to
enforce HIPAA, GLBA and all that. With Henry
DeYoung, Limin Jia, Dilsun Kaynar, and Anupam
Datta. Technical report CMU-CyLab-10-008, 2010.
representation of common rules for controlling access to
classified information. With Frank Pfenning, Denis
Serenyi and Brian Witten. Technical Report
Proof-search in an
authorization logic. Technical Report CMU-CS-09-121,
Towards a theory of secure
systems. With Anupam Datta, Jason Franklin and Dilsun Kaynar.
Technical Report CMU-CyLab-08-003, 2008. Superseded by the
Oakland 2009 paper.
From indexed lax
logic to intuitionistic logic. With Michael Carl
Tschantz. Technical Report CMU-CS-07-167, 2007.
These are unpublished notes or drafts. They are provided
as is. Please do not cite them.