Automated verification of security policies in mobile code