Formal Modeling and Reasoning about the Android Security Framework