A Model Checking-based Approach for Security Policy Verification of Mobile Systems