Abstract: In order to implement security analysis of access control policy rapidly, predicate abstract with verification space division was presented, i. e. transfer pristine state machine model analysis to abstract state machine model which contains fewer states. Furthermore,verification space division was introduced to decrease the dimensions of model checking. Endorsed by both theoretic analysis and experiment, time and space requirement are effectively reduced. Compared with the known methods,our methodology is more efficiency and less human interacted.

Key words: Access control, Predicate abstract, Security analysis, Model checking, Trust evaluation