Web application

The tool SecProver is available online here.

User manual

From scratch:

1. Select the DTM-tab, and type-in an ActionGUI data model M in Δ.

2. Select the STM-tab, and type-in an ActionGUI security model M in Δ.

3. Select the SecProver-tab, and add as many OCL boolean expressions (invariants) exp1,..., expn as you want by (repeatedly) clicking on the Add-button and typing-in the desired expression expi.

Notice that you can always modify or remove OCL boolean expressions already typed-in by clicking on the buttons Remove and Modify.

4. Select the OCL to FOL-tab, and add an OCL expression expn+1 (additional constraint) and select the type, by clicking the radio-bottom. Note that the OCL expression should be boolean.

5. Select the information related to the analysis to check: i.e: action, resource, role and type.

6. Select an SMT solver (currently, either Z3 or Yices; or directly SMT2).

7. Generate the environment....  with the syntax of the selected SMT solver.

From a stored project

To store the SecProver project that you have typed in the SecProver web application as an SecProver project, simply click on the button Save and download the generated XML file (by default, memento.xml) to your local disk.

To restore an SecProver project, simply click on the button Load and upload the project from your local disk.