Skip to content
Vetting Single Sign-On SDK Implementations via Symbolic Reasoning
Python XSLT JavaScript HTML CSS C++ Other
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.
setup notes


This is the official code used in paper Vetting Single Sign-On SDK Implementations via Symbolic Reasoning. This code is based on another project, PyExZ3 ( We have added serveral features to support the verification with user-defined conditions.

If you are using this work, please cite the following paper:

@inproceedings{yang2018vetting, title={Vetting Single Sign-On ${$SDK$}$ Implementations via Symbolic Reasoning}, author={Yang, Ronghai and Lau, Wing Cheong and Chen, Jiongyi and Zhang, Kehuan}, booktitle={27th ${$USENIX$}$ Security Symposium (${$USENIX$}$ Security 18)}, pages={1459--1474}, year={2018} }


Please follow the instructions in to setup the environment. Notice that we only support CVC4 as the theorem prover.

If you are using Mac or Ubuntu, you can follow platform-specific instructions for Ubuntu and Mac OS 10.14.


After configuring the environment, run the following code to check if the environment is cnofigured correctly.

python3 test/

For commandl line syntax, run the folllowing code to show the detailed syntax


Output is under directory /verify.

You can’t perform that action at this time.