This repository hosts the verified formal models written in BoogiePL. It is provided as supplementary material for following paper:

Rui Wang, Yuchen Zhou, Shuo Chen, Shaz Qadeer, David Evans, and Yuri Gurevich (2013, August). Explicating SDKs: Uncovering Assumptions Underlying Secure Authentication and Authorization. In Proceedings of the 22th conference on Security symposium.