Formal analysis and verification for compositional protocols based on operational semantics of security protocol
Rongsheng Dong · Journal of Guilin University of Electronic Technology · 2007
Compositionality of security protocol is an open issue in the area of security protocol formal analysis and verification.This paper proposes a new approach for formal analyzing and verifying the compositionality of security protocol.The compositional protocol of Yahalom and Denning-Sacco is modeled as operational semantics model.Its properties are automatically verified by Scyther,which is a tool based on the operational semantics of security protocol.As a result,a new multi-protocol attack to the security of Yahalom protocol is found,which indicates that it is effective in analyzing and checking the property of compositional protocols by operational semantics of security protocol.