
Faculty:
Andrew Appel,
Edward Felten
Students:
Michael Schneider,
Lujo Bauer,
EunYoung Lee
We have designed and implemented a general and powerful distributed
authentication framework based on higherorder 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 proofcarrying
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 proofcarrying 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 higherorder logic as a bridge between security logics
in a way that would enable authentication frameworks based on
different logics to interact and share resources.
ProofCarrying Authentication.
Andrew W. Appel and Edward W. Felten,
6th ACM Conference on Computer and Communications Security,
November 1999.
A
ProofCarrying Authorization System. Lujo Bauer, Michael
A. Schneider, and Edward W. Felten. Technical report CSTR63801,
Department of Computer Science, Princeton University, April 2001.
A General and Flexible AccessControl 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 Proofcarrying Authorization. Lujo Bauer.
Ph.D. Thesis, Princeton University, September 2003.
