Logic and Practice of Trust Management

Abstract

Trust management systems allow decentralized authorization of security critical actions in modern distributed systems. Examples include SDSI/SPKI, KeyNote, and RT. A variety of logics have been used to specify the semantics of trust management systems, being sufficiently expressive to capture their meaning in a natural manner, and providing them with rigorous mathematical foundations. We propose LolliMon, a linear logic programming language, as a new foundation for RT trust management, since it possesses unique features allowing a simple and scalable implementation of the system that is easily proven correct. In particular, conditional subgoals, linear hypotheses, and a mix of bottom-up and top-down proof strategies, allow for a seamless integration of authorization steps and non-local certificate retrieval, commonly called certificate chain discovery. This technique is easily adapted to a variety of enhancements of the basic system. Furthermore, we show how strategies! for minimizing the cost of certificate retrieval can be encoded in the logical specification, providing efficiency without compromising mathematical rigor for security.

This is joint work with Peter Chapin (UVM), X. Sean Wang (UVM), and Jeff Polakow (AIST, CVS, JST).

Bio

Christian Skalka received a BA in Philosophy and Mathematics from St. John's College in Santa Fe, NM in 1991, after which he worked on the Human Genome Project at the Los Alamos National Laboratories and the National Institutes of Health. He began graduate study in 1996, first earning an MS in Logic, Computation and Methodology at Carnegie Mellon University, then earning a PhD in Computer Science at the Johns Hopkins University in 2002 under Scott Smith, where his thesis was entitled "Types for Programming Language Based Security". He is currently an Assistant Professor at the University of Vermont, where his research focuses on type theory, computer security, and logic in computer science.