Z. Dai, X. He, J. Ding, and S. Gao (USA)
Security protocol, SAM framework, model checking, formal verification
Secure distributed systems rely on secure information flow between different hosts, thus placing a heavy requirement on the underlying security protocols. In this paper, we use SAM, a dual formalism based on Petri nets and temporal logic, to provide a systematic approach to specify and analyze security protocols and their desired properties. We illustrate our approach through a case study.