After a short period of being not much more than a curiosity, the
World-Wide Web quickly became an important medium for discussion,
commerce, and business. Instead of holding just information that the
entire world could see, web pages also became used to access email,
financial records, and other personal or proprietary data that was
meant to be viewed only by particular individuals or groups. This
made it necessary to design mechanisms that would restrict access to
web pages. Unfortunately, most current mechanisms are lacking in
generality and flexibility---they interoperate poorly and can express
only a limited number of security policies.
We view access control on the web as a general distributed
authorization problem and develop a solution by adapting the
techniques of proof-carrying authorization, a framework for defining
security logics based on higher-order logic.
In this dissertation we present a particular logic for modeling
access-control scenarios that occur on the web. We give this
application-specific logic a semantics in higher-order logic, thus
ensuring its soundness, and use it to implement a system that
regulates access to web pages. Our system uncouples authorization
from authentication, allowing for better interoperation across
administrative domains and more expressive security policies. Our
implementation consists of a web server module and a local web proxy.
The server allows access to pages only if the web browser can
demonstrate that it is authorized to view them. The browser's local
proxy accomplishes this by mechanically constructing a proof of a
challenge sent to it by the server. Our system supports arbitrarily
complex delegation, and we implement a framework that lets the web
browser locate and use pieces of the security policy that have been
distributed across arbitrary hosts. Our system was built for
controlling access to web pages, but could relatively easily be
extended to encompass access control for other applications as well.