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
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.
Andrew W. Appel and Edward W. Felten,
6th ACM Conference on Computer and Communications Security,
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.
Access Control for the Web via Proof-carrying Authorization. Lujo Bauer.
Ph.D. Thesis, Princeton University, September 2003.