Model Checking of Qualitative Sensitivity Preferences to Minimize Credential Disclosure

Authors

1. For all x ∈ S₂: next(x) = false only if
   x = true initially;
   for all y ∈ S⁺, y = true;
   and for all z ∈ S^-∪S₁, z = false.
2. For all x ∈ S₁: next(x) = true only if
   x = false initially;
   for all y ∈ S⁺, y = true;
   and for all z ∈ S^-∪S₂, z = false.

The SMV code used to encode the running example (the client's credential disclosure preferences) as a Kripke structure is contained in the following file:
cinet-facs12.smv (plain text, approx. 5K)

To test our method, we randomly generated CI-nets with between 5 and 20 variables and either 5 or 10 statements, then used the Consistency Checker component of our tool to determine which of the randomly-generated CI-nets were consistent. Once 20 consistent CI-nets were identified, we used the Rank Order Generator component of our tool. For each consistent CI-net, we identified the first-best through 25th-best sets of credentials to disclose (with respect to the client's disclosure preferences as modeled by the CI-net). Time and memory usage data were collected each time the underlying model checker, Cadence SMV, was called.

For more information about our tool, please see Section 5 of our paper.

Download the experimental tool

To run the tool on a computer with a current Java Runtime Environment installed:

1. Copy the downloaded JAR file to the location where you want to run the program.
2. Create a subdirectory (subfolder) called results in the location where you will run the program. As you might have guessed, result files will be stored in this subdirectory.
3. Issue the following command:
   java -jar facs12-cadence.jar -v nVariables -s nStatements -r nResults -t nTrials
   • nVariables: the number of variables (credentials) to consider
   • nStatements: the number of CI-net statements to generate
   • nResults: the number of most-preferred variable sets to compute
   • nTrials: the number of random CI-nets to generate and process

Note that this tool is primarily meant to explore the feasibility of our proposed approach; we can't guarantee that the software will behave exactly as expected, although it has worked well in our experience. If you do find a bug or if you have any questions about the tool, please let us know via email; we'll do our best to respond.

Each of our charts has versions for CI-nets with 5 statements and 10 statements. We have placed both versions side-by-side for your convenience.

Each line represents the mean value computed over all 20 trials for each combination of variables and statements.

If you have any problems viewing these graphs, please email the site's maintainer, Zach Oster (zjoster@iastate.edu).

Consistency checking: Cadence SMV time and memory usage

Finding next-most-preferred set of credentials

Cadence SMV memory usage for different numbers of variables

Cadence SMV memory usage for each of the first 25 non-trivial results (in descending order of preference)

Cadence SMV time usage for different numbers of variables

Cadence SMV time usage for each of the first 25 non-trivial results (in descending order of preference)