Automating Access Control Logics in Simple Type Theory with LEO-II

Details Automating Access Control Logics in Simple Type Theory with LEO-II Automating Access Control Logics in Simple Type Theory with LEO-II

2009-01-23

arxiv.org/abs/0901.3574v2

SEKI Report SR-2008-01 (ISSN 1437-4447), Saarland University, 2008

Computer Science

Logic in Computer Science

ii + 20 pages

Scientific paper

Garg and Abadi recently proved that prominent access control logics can be translated in a sound and complete way into modal logic S4. We have previously outlined how normal multimodal logics, including monomodal logics K and S4, can be embedded in simple type theory (which is also known as higher-order logic) and we have demonstrated that the higher-order theorem prover LEO-II can automate reasoning in and about them. In this paper we combine these results and describe a sound and complete embedding of different access control logics in simple type theory. Employing this framework we show that the off the shelf theorem prover LEO-II can be applied to automate reasoning in prominent access control logics.

Affiliated with

Also associated with

No associations

Rating

Automating Access Control Logics in Simple Type Theory with LEO-II does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Automating Access Control Logics in Simple Type Theory with LEO-II, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automating Access Control Logics in Simple Type Theory with LEO-II will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-65403