Security policies are one of the most fundamental elements of computer security. Their design has to cope with composition of components in security systems and interactions between them. Consequently, a modular approach for specification and verification of security policies is necessary and the composition of modules must consistently ensure fundamental properties of security policies, in a rigorous and systematic way. This paper shows how to use extended Petri net process (EPNP) to specify and verify security policies in a modular way. It defines a few fundamental policy properties, namely completeness, termination, consistency and confluence, in Petri net terminology and relates them to classical notions. According to XACML combiners and to property preserving Petri net process algebra (PPPA), several policy composition operators are specified and property preserving results are stated for the policy correctness verification. The approach is illustrated on the design of a complex policy.