Model Checking for Verification of Mandatory Access Control Models and Properties