Model checking is a method of formally verifying properties of finite state machines. By describing operating system structure and system authorization policies using finite state machines, model checking may be used to verify useful properties of policies, improving the chances of developing a secure system. The technique is demonstrated on authorization systems from an Active Network, and from a simplified UNIX-like environment.