"Automated Game-Theoretic Verification of Security Systems" - Supporting Material

Paper: "Automated Game-Theoretic Verification of Security Systems"
by Chunyan Mu

Models and Properties

Included below are the models and properties for case study included in the submission.

• Simple example (see examples on p.11-14)
  
  
  • Model: eg.prism
  • Properties: eg.props
  
  
• Crowds anonymity network (4 players including 2 malicious players)
  
  
  • Model: crowds-dtmc-n4m2.prism
  • Properties: crowds-dtmc-n4m2.props

The Tool

A source code release of our prototype tool is available here: prism-4.3.nash-src.tar.gz.

This can be built in exactly the same way as normal versions of PRISM. See the installation instructions.

The examples above can be found in the examples directory.

Here is an example of how to build the distribution and run an example:

tar xvfz prism-nash.tar.gz
cd prism-nash/prism/
make
cp ext/phc-mac phc (for mac user)
cp ext/phc-linux phc (for linux user)
chmod u+x phc
bin/prism examples/crowds-dtmc-n4m2.prism examples/crowds-dtmc-n4m2.props -param x1=0:1,x2=0:1 -nash out