Improvement of SET protocol model and formal analysis via SMV
Jianlin Zhang · Computer Engineering and Applications Journal · 2010
The simplified model of payment process of the SET protocol is used to build up its formal model and finite state machine model,as well as CTL formulations of the security properties are presented.Under the assumption of the network environment being controlled by intruder,the symbolic model checking ware (SMV) is applied for analyzing the authentication,confidentiality and integrity,attacks are found.Then,the influence of attacks is discussed.Finally,the protocol model is optimized. The result of analysis and checking indicates the importance of dual signature on SET protocol.