Formal Modeling and Verification of CloudProxy


This paper appeared in VSTTE 2014.

UCLID Models

To prove a property in the CloudProxy model, you will need to append the property file under the Properties section to the CloudProxy model file (under the CloudProxy Model section). We have provided a shell script: that will append each of the property files to the model file and check for all the four properties. You may want to edit the output paths in the script.

CloudProxy Model



1. Non-interference: ppty1.ucl
2. Data confidentiality: ppty2.ucl
3. Data integrity: ppty3.ucl
4. Keys protection: ppty4.ucl