PV1 SPAN: Stochastic Protocol Analyzercomputes whether two protocols are indistinguishable

"... [A] formal verification engine for model checking indistinguishability (trace equivalence) and state-based safety properties of randomized security protocols in the symbolic model."

Application domain/field

Type of tool

Model checker

Expected input

Expected output

true or false indicating whether two randomized security protocols are indistinguishable.


Uses KISS, AKISS, Maude, Apfloat
Protocol Security


Repository: https://github.com/bauer-matthews/SPAN

Related papers

Model Checking Indistinguishability of Randomized Security Protocols

Last publication date

18 July 2018

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.