Introduction

SSPA is an automatic symbolic verification tool designed for stateful security protocols. Its main features are as follows.

  ●  A large range of crypto primitives can be specified in SSPA, including symmetric encryption, asymmetric encryption, hash, signature, zero knowledge proof and etc.

  ●  SSPA gives unbounded verification to the reachability properties. Protocol states can be handled in SSPA in a natural and intuitive way.

Downloads

1. ✦SSPA v0.0.3 (Alpha)       
   

2. ✦Mac OS X Darwin-x86_64-v0.0.3.zip
   

3. ✦Ubuntu N.A.
   

4. ✦Windows Windows_NT-x86-v0.0.3.zip
   

5. ✦Readme README.md
   

6. ✦Manual MANUAL.md

Related Papers

A Verification Framework for Stateful Security Protocols

Li Li, Naipeng Dong, Jun Pang, Jun Sun, Guangdong Bai, Yang Liu and Jin Song Dong

Models and experiment results: model.zip

Tool Version used in the experiment: Darwin-x86_64-v0.0.3.zip