Security policies are one of the most fundamental elements of computer security. This paper uses colored Petri net process (CPNP) to specify and verify security policies in a modular way. It defines fundamental policy properties, i.e., completeness, termination, consistency and confluence, in Petri net terminology and gets some theoretical results. According to XACML combiners and property-preserving Petri net process algebra (PPPA), several policy composition operators are specified and property-preserving results are stated for the policy correctness verification.