Generalized certificate revocation

We introduce a language for creating and manipulating certificates, that is, digitally signed data based on public key cryptography, and a system for revoking certificates. Our approach provides a uniform mechanism for secure distribution of pubic key bindings, authorizations, and revocation information. An external language for the description of these and other forms of data is compiled into an intermediate language with a well-defined denotational and operational semantics. The internal language is used to carry out consistency checks for security, and optimizations for efficiency. Our primary contribution is a technique for treating revocation data dually to other sorts of information using a polarity discipline in the intermediate language.