Download SPV User Manual and Quick Start Guide

sees(b, m1))), where a plays A and runs a local session with b plays B and m1 for N, and Oa express
a’s observations when reaching the final step of the protocol. Similarly, K2ABN stands for two level
ones Oa > know(a, know(b, (said(a, m2) + sees(a, m2)))) , where a, A, b, B and Oa are the same as
above and m2 is for N in a corresponding local session of b. The partial epistemic specifications we
have verified are shown in the table 3.
Table 3: Some verified epistemic specifications of SPV
As for the SET purchase protocol, we notice that we do not intend to offer more detailed analysis
as done in Isabelle; what we want know from these experiments is whether an automatic
justification-oriented approach can be scaled to the size of the SET purchase phase protocol.
The experiments results show that SPV is powerful and friendly to users. It is open, flexible and
scalable. We believe that this tool will be an interesting contribution to the security verification and
formal methods communities.
22