Reasoning About Authorization and Security
Abstract
This project had three main thrusts: (1) to create a language for expressing authorization policies that satisfied numerous desiderata, including being expressive, being easy to use, having precise semantics, and allowing for accountability: (2) to add the ability to express knowledge based specifications to Nuprl, a well-developed language that has been used extensively to prove that programs satisfy their specifications, with the intent of then using Nuprl to automatically synthesize security protocols satisfying appropriate specifications; (3) to understand the extent to which it is possible to achieve robust security in the presence of rational adversaries. With regard to (1), a language Lithium has been developed (jointly with Vicky Weissman) that satisfies many of the desiderata. Lithium was chosen as the language for NRL's MLWeb project.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 2008
- Accession Number
- ADA495347
Entities
People
- Joseph Halpern
Organizations
- Cornell University