sip@cs.princeton.edu

We have designed and implemented a general and powerful distributed authentication framework based on higher-order logic. Authentication frameworks --- including Taos, SPKI, SDSI, and X.509 --- have been explained using logic. We show that by starting with the logic, we can implement these frameworks, all in the same concise and efficient system. Because our logic has no decision procedure --- although proof checking is simple --- users of the framework must submit proofs with their requests.

As a prototype application we have developed modules that extend a standard web server and a standard web browser to use proof-carrying authorization to control access to web pages. Our framework makes it possible to locate and use pieces of the security policy that have been distributed across arbitrary hosts. The web browser generates proofs iteratively by repeatedly fetching proof components until a proof can be constructed. We provide for iterative authorization, by which a server can require a browser to prove a series of challenges. Our prototype implementation includes a series of optimizations, such as speculative proving and modularizing and caching proofs, which allows proof-carrying authorization to be used with minimal performance and bandwidth overheads.

Ongoing work includes further development of our prototype application (download page). We will investigate the use of oblivous transfer for fetching proof components without revealing unnecessary information and refine our security logic to reduce its trusted base and increase its generality. We are also exploring the idea of using a higher-order logic as a bridge between security logics in a way that would enable authentication frameworks based on different logics to interact and share resources.

Proof-Carrying Authentication. Andrew W. Appel and Edward W. Felten, 6th ACM Conference on Computer and Communications Security, November 1999.

A Proof-Carrying Authorization System. Lujo Bauer, Michael A. Schneider, and Edward W. Felten. Technical report CS-TR-638-01, Department of Computer Science, Princeton University, April 2001.

A General and Flexible Access-Control System for the Web. Lujo Bauer, Michael A. Schneider, and Edward W. Felten. In Proceedings of the 11th USENIX Security Symposium, San Francisco, CA, August 2002. [PDF, PS]

Access Control for the Web via Proof-carrying Authorization. Lujo Bauer. Ph.D. Thesis, Princeton University, September 2003.