<p>Correct certificate revocation practices are essential to each public-key infrastructure. While there exist a number of protocols to achieve revocation in PKI systems, there has been very little work on the theory behind it: Which different types of revocation can be identified? What is the intended effect of a specific revocation type to the knowledge base of each entity?</p><p>As a first step towards a methodology for the development of reliable models, we present a graph-based formalism for specification and reasoning about the distribution and revocation of public keys and certificates. The model is an abstract generalization of existing PKIs and distributed in nature; each entity can issue certificates for public keys that they have confidence in, and distribute or revoke these to and from other entities.</p><p>Each entity has its own public-key base and can derive new knowledge by combining this knowledge with certificates signed with known keys. Each statement that is deduced or quoted within the system derives its support from original knowledge formed outside the system. When such original knowledge is removed, all statements that depended upon it are removed as well. Cyclic support is avoided through the use of support sets.</p><p>We define different revocation reasons and show how they can be modelled as specific actions. Revocation by removal, by inactivation, and by negation are all included. By policy, negative statements are the strongest, and positive are the weakest. Collisions are avoided by removing the weaker statement and, when necessary, its support.</p><p>Graph transformation rules are the chosen formalism. Rules are either interactive changes that can be applied by entities, or automatically applied deductions that keep the system sound and complete after the application of an interactive rule.</p><p>We show that the proposed model is sound and complete with respect to our definition of a valid state.</p> / Report code: LIU-TEK-LIC-2006:1

Correct certificate revocation practices are essential to each public-key infrastructure. While there exist a number of protocols to achieve revocation in PKI systems, there has been very little work on the theory behind it: Which different types of revocation can be identified? What is the intended effect of a specific revocation type to the knowledge base of each entity? As a first step towards a methodology for the development of reliable models, we present a graph-based formalism for specification and reasoning about the distribution and revocation of public keys and certificates. The model is an abstract generalization of existing PKIs and distributed in nature; each entity can issue certificates for public keys that they have confidence in, and distribute or revoke these to and from other entities. Each entity has its own public-key base and can derive new knowledge by combining this knowledge with certificates signed with known keys. Each statement that is deduced or quoted within the system derives its support from original knowledge formed outside the system. When such original knowledge is removed, all statements that depended upon it are removed as well. Cyclic support is avoided through the use of support sets. We define different revocation reasons and show how they can be modelled as specific actions. Revocation by removal, by inactivation, and by negation are all included. By policy, negative statements are the strongest, and positive are the weakest. Collisions are avoided by removing the weaker statement and, when necessary, its support. Graph transformation rules are the chosen formalism. Rules are either interactive changes that can be applied by entities, or automatically applied deductions that keep the system sound and complete after the application of an interactive rule. We show that the proposed model is sound and complete with respect to our definition of a valid state. / <p>Report code: LIU-TEK-LIC-2006:1</p>