We study some of the concepts, protocols, and algorithms for access control
in distributed systems, from a logical perspective. We account for how a
principal may come to believe that another principal is making a request,
either on his own or on someone else’s behalf. We also provide a logical
language for access control lists, and theories for deciding whether requests
should be granted.
We describe a theory of authentication and a system that implements it. Our theory is based on
the notion of principal and a ‘speaks for’ relation between principals. A simple principal either
has a name or is a communication channel; a compound principal can express an adopted role or
delegated authority. The theory shows how to reason about a principal’s authority by deducing
the other principals that it can speak for; authenticating a channel is one important application.
We use the theory to explain many existing and proposed security mechanisms. In particular, we
describe the system we have built. It passes principals efficiently as arguments or results of remote
procedure calls, and it handles public and shared key encryption, name lookup in a large
name space, groups of principals, program loading, delegation, access control, and revocation.
The ACL model is unable to make correct access decisions for interactions involving more than
two principals, since required information is not retained across message sends. Though this
deficiency has long been documented in the published literature, it is not widely understood. This
logic error in the ACL model is exploited by both the clickjacking and Cross-Site Request
Forgery attacks that affect many Web applications.
Access control is central to computer security. Traditionally, we wish to restrict
the user to exactly what he should be able to do, no more and no less.
You might think that this only applies to legitimate users: where do attackers
fit into this worldview? Of course, an attacker is a user whose access should be
limited just like any other. Increasingly, of course, computers expose services
that are available to anyone – in other words, anyone can be a a legitimate user.
As well as users there are also programs we would like to control. For
example, the program that keeps the clock correctly set on my machine should
be allowed to set the clock and talk to other time-keeping programs on the
Internet, and probably nothing else1
Increasingly we are moving towards an environment where users choose what
is installed on their machines, where their trust in what is installed is highly
variable2 and where “installation” of software is an increasingly fluid concept,
particularly in the context of the Web, where merely viewing a page can cause
code to run.
In this paper I explore an alternative to the traditional mechanisms of roles
and access control lists. Although I focus on the use case of web pages, mashups
and gadgets, the technology is applicable to all access control.
Abstract—Web-based single sign-on (SSO) services such as
Google Sign-In and Log In with Paypal are based on the OpenID
Connect protocol. This protocol enables so-called relying parties
to delegate user authentication to so-called identity providers.
OpenID Connect is one of the newest and most widely deployed
single sign-on protocols on the web. Despite its importance, it has
not received much attention from security researchers so far, and
in particular, has not undergone any rigorous security analysis.
In this paper, we carry out the first in-depth security analysis
of OpenID Connect. To this end, we use a comprehensive generic
model of the web to develop a detailed formal model of OpenID
Connect. Based on this model, we then precisely formalize and
prove central security properties for OpenID Connect, including
authentication, authorization, and session integrity properties.
In our modeling of OpenID Connect, we employ security
measures in order to avoid attacks on OpenID Connect that
have been discovered previously and new attack variants that we
document for the first time in this paper. Based on these security
measures, we propose security guidelines for implementors of
OpenID Connect. Our formal analysis demonstrates that these
guidelines are in fact effective and sufficient.
Macaroons, recently introduced by Birgisson et al. [BPUE+14], are authorization credentials that
provide support for controlled sharing in decentralized systems. Macaroons are similar to cookies in that
they are bearer credentials, but unlike cookies, macaroons include caveats that attenuate and contextually
confine when, where, by who, and for what purpose authorization should be granted.
In this work, we formally study the cryptographic security of macaroons. We define macaroon schemes,
introduce corresponding security definitions and provide several constructions. In particular, the MACbased
and certificate-based constructions outlined in [BPUE+14], can be seen as instantiations of our
definitions. We also present a new construction that is privately-verifiable (similar to the MAC-based
construction) but where the verifying party does not learn the intermediate keys of the macaroon, a problem
already observed in [BPUE+14].
We also formalize the notion of a protocol for “discharging” third-party caveats and present a security
definition for such a protocol. The encryption-based protocol outlined by Birgisson et al. [BPUE+14] can
be seen as an instantiation of our definition, and we also present a new signature-based construction.
Finally, we formally prove the security of all constructions in the given security models.
The OAuth 2.0 protocol is one of the most widely deployed authorization/single sign-on (SSO) protocols
and also serves as the foundation for the new SSO standard OpenID Connect. Despite the popularity
of OAuth, so far analysis efforts were mostly targeted at finding bugs in specific implementations and
were based on formal models which abstract from many web features or did not provide a formal treatment
In this paper, we carry out the first extensive formal analysis of the OAuth 2.0 standard in an expressive
web model. Our analysis aims at establishing strong authorization, authentication, and session
integrity guarantees, for which we provide formal definitions. In our formal analysis, all four OAuth
grant types (authorization code grant, implicit grant, resource owner password credentials grant, and
the client credentials grant) are covered. They may even run simultaneously in the same and different
relying parties and identity providers, where malicious relying parties, identity providers, and browsers
are considered as well. Our modeling and analysis of the OAuth 2.0 standard assumes that security
recommendations and best practices are followed in order to avoid obvious and known attacks.
When proving the security of OAuth in our model, we discovered four attacks which break the security
of OAuth. The vulnerabilities can be exploited in practice and are present also in OpenID Connect.
We propose fixes for the identified vulnerabilities, and then, for the first time, actually prove the
security of OAuth in an expressive web model. In particular, we show that the fixed version of OAuth
(with security recommendations and best practices in place) provides the authorization, authentication,
and session integrity properties we specify.