SPiM

SPiM: a tool for interpolation-based formal verification of security protocols

Craig's interpolation has been successfully applied in formal methods for model checking and test-case generation for sequential programs. The concurrency implicit in the formalization of security protocols and the possible presence of an intruder, however, make them unsuitable to the direct application of such methods. We present a tool that (i) translates protocol specifications into sequential programs, where attack states of the protocol are represented as goal locations, and (ii) applies an interpolation-based method to the analysis of such programs

SPiM experiments (case studies, graphs and results)
Download SPiM source code

Download VM (VirtualBox) with SPiM

• Download and install VirtualBox
• Download the VM from here
• Import the VM in VirtualBox (howto)
• Username and Password: spim
• cd ~/SPiM_tool; java translator.Main <specification.aslan++>

INSTALL FROM SOURCE CODE

• SPiM has been tested on Linux only
• 0. Requirements:
  • Install Java 7
  • Download and extract Z3, iZ3 (it already contains libfoci.so)
  • Add z3/lib to the env variable LD_LIBRARY_PATH
• 1. Download the SPiM source code form the link above
• 2. cd <Donwload directory>; tar -xvzf SPiM_tool.tar.gz
• 3. javac se/*.java; cd translator; javacc Parser.jj; cd ..; javac -Xlint:unchecked translator/*.java;
• 4. java translator.Main <specification.aslan++> [-gv graphs/specification]