Deepak Garg

Recently Accepted Papers

• Policy Auditing over Incomplete Logs: Theory, Implementation and Applications. With Limin Jia and Anupam Datta. Accepted to the ACM Conference on Computer and Communications Security (CCS 2011). [Full version with proofs: Technical Report CMU-CyLab-11-002 and arXiv.org:1102.2521v3]. © ACM

Published Papers by Year

2011

• A Proof-Carrying File System with Revocable and Use-Once Certificates. With Jamie Morgenstern and Frank Pfenning. International Workshop on Security and Trust Management (STM), 2011.
• New Modalities for Access Control Logics: Permission, Control and Ratification. With Valerio Genovese. International Workshop on Security and Trust Management (STM), 2011. [Full version with proofs]
• Verification of Information Flow and Access Control Policies via Dependent Types. With Aleks Nanevski and Anindya Banerjee. IEEE Symposium on Security and Privacy (Oakland), 2011. [Full version: Technical report IMDEA-SW-TR-2010.0] © IEEE
• On Adversary Models and Compositional Security. With Anupam Datta, Jason Franklin, Limin Jia and Dilsun Kaynar. IEEE Security and Privacy Magazine, special issue on the Science of Security, 2011. © IEEE

2010

• 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 Society (WPES), 2010. [Full version: Technical report CMU-CyLab-10-007]. © ACM
• Stateful 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
• Compositional 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

2009

• PCAL: Language support for proof-carrying authorization systems. With Avik Chaudhuri. European Symposium on Research in Computer Security (ESORICS), 2009. [Full version: Technical Report CMU-CS-09-141] © Springer-Verlag
• A logic of secure systems and its application to trusted computing. With Anupam Datta, Jason Franklin and Dilsun Kaynar. IEEE Symposium on Security and Privacy (Oakland), 2009. [Full version: Technical Report CMU-CyLab-09-001] © IEEE

2008

• An authorization logic with explicit time. With Henry DeYoung and Frank Pfenning. IEEE Symposium on Computer Security Foundations (CSF), 2008. [Full version: Technical Report CMU-CS-07-166, 2007] © IEEE
• Principal-centric reasoning in constructive authorization logic. Workshop on Intuitionistic Modal Logic and Applications (IMLA), 2008. [Full version: Technical Report CMU-CS-09-120, 2009].
• A logic for reasoning about networked secure systems. With Anupam Datta, Jason Franklin and Dilsun Kaynar. FCS-ARSPA-WITS Workshop, 2008. [Full version with proofs] Superseded by the Oakland 2009 paper.
• A modal deconstruction of access control logics. With Martín Abadi. International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), 2008. [Full version with proofs] © Springer-Verlag

2007

• Consumable credentials in logic-based access-control systems. With Kevin D. Bowers, Lujo Bauer, Frank Pfenning and Michael K. Reiter. Network & Distributed System Security Symposium (NDSS), 2007.

2006

• A linear logic of authorization and knowledge. With Lujo Bauer, Kevin D. Bowers, Frank Pfenning and Michael K. Reiter. European Symposium on Research in Computer Security (ESORICS), 2006. [Extended version] © Springer-Verlag
• Non-interference in constructive authorization logic. With Frank Pfenning. IEEE Computer Security Foundations Workshop (CSFW), 2006. © IEEE

2005

• Type-directed concurrency. With Frank Pfenning. International Conference on Concurrency Theory (CONCUR), 2005. [Full version: Technical Report CMU-CS-05-104] © Springer-Verlag

2004

• Effective chemistry for synchrony and asynchrony. With Akash Lal and Sanjiva Prasad. IFIP International Conference on Theoretical Computer Science (IFIP-TCS), 2004. © Kluwer

Edited Volumes

• Proceedings of the 5th ACM SIGPLAN Workshop on Programming Languages and Analysis of Security (PLAS 2010). Editors Anindya Banerjee and Deepak Garg. June, 2010. ISBN: 978-1-60558-827-8. © ACM

Theses

• Proof Theory for Authorization Logic and Its Application to a Practical File System. Ph.D. Dissertation, 2009. Available as Technical Report CMU-CS-09-168. [Typeset for: Letter size, A4 size] [Implementation]

Technical Reports

• Privacy policy 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.
• A logical representation of common rules for controlling access to classified information. With Frank Pfenning, Denis Serenyi and Brian Witten. Technical Report CMU-CS-09-139, 2009.
• Proof-search in an authorization logic. Technical Report CMU-CS-09-121, 2009.
• 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.

Notes/Misc/Drafts

• Typed language support for proof-carrying authorization. Notes for 18-739: Foundations of Security and Privacy. November, 2009.
• An introduction to proof-carrying authorization. Notes for 18-739: Foundations of Security and Privacy. December, 2007.