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