Problem 3 (Total = 55 points) Manipulate ACL formulas for model checking

We assume that the principal expression datatype is defined as in Problem 2.
We continue to define the Access control formula via the following declaration:

> data Form = Var PropVar
> | Not Form
> | Or Form Form
> | And Form Form
> | Imply Form Form
> | Equiv Form Form
> | Says Prin Form
> | Contr Prin Form
> | For Prin Prin
> deriving Show

In addition, propositional variables are of type Char:

> type PropVar = Char

a. (20 point) Write a function is_ACL_prin, which will take

-- a list of simple principals plst (of type [PName])
-- a principle expression pr


as input, verify if each simple principal in plst
is a part of the principal expression pr.

For example:

> princLst :: [PName]
> princLst = ["Al","Marcy"]

> eg3a :: Prin
> eg3a= Name "Marcy"

> testEg3a :: Bool
> testEg3a = is_ACL_prin princLst eg3a

You will get:

*Main> testEg3a
True

*** Put your answer below. For codes, DO NOT FORGET to add the > symbol.

> is_ACL_prin :: [PName]-> Prin -> Bool
> is_ACL_prin [] _ = False
> is_ACL_prin (x:xs) (Name y) | x==y = True | otherwise = is_ACL_prin(xs) (Name y)

--------------------------------------------------------------------------------

b. (25 point)

First, note that when we specify a specific Kripke model M = (W, I, J), we need to
also state

-- a list of simple principals (of type [PName]) which are included in the model
-- a list of propositional variables (of type [PropVar]) which are included in
the model

By using the function ACL_prin (part a) or otherwise, write a Boolean function
is_ACL_Form, which will take

-- a list of simple principals plst (of type [PName])
-- a list of propositional variables proplst (of type [PropVar])
-- an ACL formula (of type Form)

as input, verify if a formula is a valid ACL formula for the model M, where

-- each simple principal in M is a member of plst, and
-- each propositional variable in M is a member of proplst.



*** Put your answer below. For codes, DO NOT FORGET to add the > symbol.

--------------------------------------------------------------------------------

c. (10 point) Create two formulas f1, f2 (ACL formulas), in Haskell, based on
the model given in ACST, example 2.8 as test cases. The formula f1 is an ACL
formula for the model but f2 is a ACL formula (of type Form) which is not
a formula for the model.

Show the two fomulas and the test results in the space provided below.