Companion Web site for our paper in FACS 2012:

Department of Computer Science

Iowa State University

- For all
*x*∈*S*: next(_{2}*x*) = false only if

*x*= true initially;

for all*y*∈*S*,^{+}*y*= true;

and for all*z*∈*S*∪^{-}*S*,_{1}*z*= false. - For all
*x*∈*S*: next(_{1}*x*) = true only if

*x*= false initially;

for all*y*∈*S*,^{+}*y*= true;

and for all*z*∈*S*∪^{-}*S*,_{2}*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.

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

- Copy the downloaded JAR file to the location where you want to run the program.
- 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. - Issue the following command:

`java -jar facs12-cadence.jar -v`*nVariables*-s*nStatements*-r*nResults*-t*nTrials*: the number of variables (credentials) to consider*nVariables*: the number of CI-net statements to generate*nStatements*: the number of most-preferred variable sets to compute*nResults*: the number of random CI-nets to generate and process*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.

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).