Companion Web site for our paper in FACS 2012:

Model Checking of Qualitative Sensitivity Preferences to Minimize Credential Disclosure

Authors

Zachary J. Oster, Ganesh Ram Santhanam, Vasant Honavar, and Samik Basu
Department of Computer Science
Iowa State University

Encoding CI-nets as Kripke structures for Cadence SMV

Given a CI-net statement S+, S- : S1 > S2, the patterns that we used to encode a CI-net statement in the SMV language are:

  1. For all xS2: next(x) = false only if
    x = true initially;
    for all yS+, y = true;
    and for all zS-S1, z = false.
  2. For all xS1: next(x) = true only if
    x = false initially;
    for all yS+, y = true;
    and for all zS-S2, 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)


Experimental Method

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

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.


Graphical Summaries of Results

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

Cadence SMV time and memory usage for consistency checking: 5 statements per CI-net Cadence SMV time and memory usage for consistency checking: 10 statements per CI-net

Finding next-most-preferred set of credentials

Cadence SMV memory usage for different numbers of variables

Cadence SMV memory usage for finding next-most-preferred set: 5 statements per CI-net Cadence SMV memory usage for finding next-most-preferred set: 10 statements per CI-net

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

Cadence SMV memory usage for finding next-most-preferred set: 5 statements per CI-net Cadence SMV memory usage for finding next-most-preferred set: 10 statements per CI-net

Cadence SMV time usage for different numbers of variables

Cadence SMV time usage for finding next-most-preferred set: 5 statements per CI-net Cadence SMV time usage for finding next-most-preferred set: 10 statements per CI-net

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

Cadence SMV time usage for finding next-most-preferred set: 5 statements per CI-net Cadence SMV time usage for finding next-most-preferred set: 10 statements per CI-net