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

• Randomized security protocols
• Model checking
• Security protocols

Type of tool

Model checker

Expected input

• Protocol P
• Protocol P'

Expected output

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

Internals

Uses KISS, AKISS, Maude, Apfloat