Formal Specification and Automatic Analysis of Business Processes under Authorization Constraints: an Action-based Approach