Formal Modeling and Verification of CloudProxy
This paper appeared in VSTTE 2014.
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: run_cloudproxy.sh 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.
1. Non-interference: ppty1.ucl
2. Data confidentiality: ppty2.ucl
3. Data integrity: ppty3.ucl
4. Keys protection: ppty4.ucl