An Action-based Approach to the Formal Specification and Automated Analysis of Business Processes under Authorization Constraints