Distributed System Security via Logical Frameworks

Publications

Distributed system security via logical frameworks. In Information Security Research: New Methods for Protecting Against Cyber Threats, pages 108–115. Department of Defense, Wiley Publishing, 2007. Lujo Bauer, Frank Pfenning, and Michael K. Reiter. [PDF]

Device-enabled authorization in the Grey system. In Proceedings of the 8th Information Security Conference (ISC’05), pages 431–445, Singapore, September 2, 2005. Springer Verlag LNCS 3650. Reprinted in: Information Security Research: New Methods for Protecting Against Cyber Threats, pp. 116–130, Department of Defense, Wiley Publishing, 2007. Lujo Bauer, Scott Garriss, Jonathan M. McCune, Michael K. Reiter, Jason Rouse, and Peter Rutenbar. [PDF]

Avoiding Causal Dependencies via Proof Irrelevance in a Concurrent Logical Framework. Technical Report CMU-CS-07-107, Carnegie Mellon University, February 2007. Ruy Ley-Wild and Frank Pfenning. [PDF]

The Focused Inverse Method for Linear Logic. PhD thesis, Carnegie Mellon University, December 2006. Available as technical report CMU-CS-06-162. Kaustuv Chaudhuri. [PDF]

A linear logic of affirmation and knowledge. In D. Gollman, J. Meier, and A. Sabelfeld, editors, Proceedings of the 11th European Symposium on Research in Computer Security (ESORICS’06), pages 297–312, Hamburg, Germany, September 2006. Springer LNCS 4189. Deepak Garg, Lujo Bauer, Kevin Bowers, Frank Pfenning, and Michael Reiter. [PDF]

A logical characterization of forward and backward chaining in the inverse method. In U. Furbach and N. Shankar, editors, Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR’06), pages 97–111, Seattle, Washington, August 2006. Springer LNCS 4130. Extended and revised version to appear in a special issue of the Journal of Automated Reasoning with selected papers from IJCAR 2006. Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. Version from March 2006: [PDF]

Non-Interference in Constructive Authorization Logic. Proceedings of the 19th Computer Security Foundations Workshop (CSFW'06), Venice, Italy, July 2006. To appear. Deepak Garg and Frank Pfenning.
[PDF] [Formalization]

Consumable credentials in logic-based access-control systems. In Proceedings of the 14th Annual Network and Distributed System Security Symposium (NDSS’07), pages 143–157, San Diego, California, February 2007. Internet Society. Preliminary version available as Technical Report CMU-CYLAB-06-002, Carnegie Mellon University, February 2006. Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter. [PDF]

Focusing the inverse method for linear logic. In L.Ong, editor, Proceedings of the 14th Annual Conference on Computer Science Logic (CSL’05), pages 200–215, Oxford, England, August 2005. Springer Verlag LNCS 3634. Kaustuv Chaudhuri and Frank Pfenning. [PDF] [Implementation]

A Focusing Inverse Method Prover for First-Order Linear Logic. 20th International Conference on Autmated Deduction (CADE-20), pages 69-83, Tallinn, Estonia, July 2005. Springer Verlag LNCS 3632. Kaustuv Chaudhuri and Frank Pfenning. [PDF] [Propositional] and [first-order-prover] implementations.

Distributed proving in access-control systems. In V.Paxon and M.Waidner, editors, Proceedings of the 2005 Symposium on Security and Privacy (S&P’05), pages 81–95, Oakland, California, May 2005. IEEE Computer Society Press. Lujo Bauer, Scott Garriss and Michael K. Reiter. [PDF]

Monadic concurrent linear logic programming. In A.Felty, editor, Proceedings of the 7th International Symposium on Principles and Practice of Declarative Programming (PPDP’05), pages 35–46, Lisbon, Portugal, July 2005. ACM Press. Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins. [PDF] [Prototype] implementation.


Talks

Constructive Authorization Logics. Invited talk at the 4th Workshop on Foundations of Computer Security (FCS'05), Chicago, Illinois, July 2005. [PDF]

Distributed System Security via Logical Frameworks. Invited talk at the 5th Workshop on Issues in the Theory of Security (WITS'05), Long Beach, California, January 2005. Frank Pfenning. Slides [PDF]

ONR Meeting Presentation - 08/17/2004 - [PDF]


Related Work by Project Members

Lujo Bauer

Access control for the web via proof-carrying authorization. Ph.D. Thesis, Princeton University, November 2003. Lujo Bauer. [PDF]

A general and flexible access-control system for the web. In Proceedings of the 11th USENIX Security Symposium, August 2002. Lujo Bauer, Michael A. Schneider, and Edward W. Felten. [PDF]

Frank Pfenning

CLF: A Dependent Logical Framework for Concurrent Computations. Draft Manuscript, July 2004. Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. [PDF]

Specifying Properties of Concurrent Computations in CLF. 4th International Workshop on Logical Frameworks and Meta-Languages (LFM'04), Cork, Ireland, July 2004. Joint work with Iliano Cervesato, David Walker, and Kevin Watkins. Slides [PDF]

A Concurrent Logical Framework: The Propositional Fragment. In Types for Proofs and Programs. Springer-Verlag LNCS, 2004. Selected papers from the Third International Workshop Torino, Italy, April 2003. To appear. Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. [PDF]

A Concurrent Logical Framework II: Examples and Applications. Technical Report CMU-CS-02-102, March 2002, revised May 2003. Iliano Cervesato, Frank Pfenning, David Walker, and Kevin Watkins. [PDF]

A Concurrent Logical Framework I: Judgments and Properties. Technical Report CMU-CS-02-101, March 2002, revised May 2003. Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. [PDF]


[ Home | Publications | Software | Links ]