Date: Mon, 22 Mar 2004 13:59:21 -0600 (CST) From: Sandip Ray Subject: This week in ACL2 Greetings, This week, Bill Young will talk about modeling security policies in ACL2. We will meet as usual in ACES 6.442 at 4:00 on Wednesday. Here is the title and abstract for this talk: -------------------------------------------------------------------- Using ACL2 to Model Noninterference-Style Security Policies Noninterference policies provide an expressive and flexible format for specifying secure systems. However, much of the published research on noninterference uses fairly arcane formalisms. In the late 1990's, Bevier and Young modeled noninterference using a spare and elegant behavioral-style system model. This has been extended to encompass models of security with transitive and intransitive security policies, deterministic and nondeterministic systems, and possibilistic and probabilistic inferences. Each version has supporting "unwinding theorems" and all proofs have been checked with ACL2.