Reasoning About Authorization and Security
Final rept. 1 Jan 2005-30 Jun 2008
CORNELL UNIV ITHACA NY
Pagination or Media Count:
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 NRLs MLWeb project.