Model Checking of Security-sensitive Business Processes