A Formal Semantics for SPKI


Jon Howell and David Kotz. A Formal Semantics for SPKI. Technical Report number TR2000-363, Dartmouth Computer Science, March 2000. ©Copyright the authors. Revision of howell:calculus-tr. Later revised as howell:spki.


We extend the logic and semantics of authorization due to Abadi, Lampson, et al. to support restricted delegation. Our formal model provides a simple interpretation for the variety of constructs in the Simple Public Key Infrastructure (SPKI), and lends intuition about possible extensions. We discuss both extensions that our semantics supports and extensions that it cautions against.

Citable with [BibTeX]

Projects: [snowflake]

Keywords: [security]

Available from the publisher: [page]

Available from the author: [bib] [pdf] [ps.gz]
This pdf was produced by the publisher and its posting here is permitted by the publisher.

[Kotz research]