KnowledgeBase » SEMINAR » ID = 659

Analyzing Access Control Logics Using Evidence Semantics

by Robert L. Constable
2011-2012

It is known that access control logics can be given a clear semantics using realizability. Abadi has written about this as well as several other authors, and there is a mapping of Abadi's particular logic, CDD, into system F. However, in his paper Variations in Access Control Logic from 2008 [PDF from Springer], he does not employ realizability. I will interpret his results using evidence semantics because the proofs can be made simpler, they suggest implementation ideas, and because his results illustrate a principle that Mark and I advance: the natural logic of distributed computing is intuitionistic.