Formal Modeling and Verification of the Android Security Framework