Automated Analysis of Scenario-Based Specifications of Distributed Access Control Policies with Non-mechanizable Activities