Protocol security in a composition protocol environment has always been an open problem in the field of formal analysis and verification of security protocols. As a well-known tool to analyze and verify the logical consistency of concurrent systems, SPIN (Simple Promela Interpreter) has been widely used in the analysis and verification of the security of a single protocol. There is no special research on the verification of protocol security in a composition protocol environment. To solve this problem, firstly, a formal analysis method for composition protocol based on SPIN is proposed, and a formal description of protocol operation semantics is given. Then the attacker model is formalized, and a message specification method based on field detection and component recognition is presented to alleviate the state explosion problem. Finally, the NSB protocol and the NSL protocol are used as examples for compositional analysis. It is demonstrated that the proposed method can effectively verify the security of the protocol in a composition protocol environment and enhance the efficiency of composition protocol verification.

The verification of security protocols is an important basis for network security. Now, some security protocols add timestamps to messages to defend against replay attacks by network intruders. Therefore, verifying the security properties of protocols with timestamps is of great significance to ensure network security. However, previous formal analysis method of such protocols often extracted timestamps into random numbers in order to simplify the model before modeling and verification, which probably cause time-dependent security properties that are ignored. To solve this problem, a method for verifying security protocols with timestamps using model checking technique is proposed in this paper. To preserve the time-dependent properties of the protocol, Promela (process meta language) is utilized to define global clock representing the protocol system time, timer representing message transmission time, and the clock function representing the passage of time; in addition, a mechanism for checking timestamps in messages is built using Promela. To mitigate state space explosion in model checking, we propose a vulnerable channel priority method of using Promela to build intruder model. We take the famous WMF protocol as an example by modeling it with Promela and verifying it with model checker SPIN (Simple Promela Interpreter), and we have successfully found two attacks in the protocol. The results of our work can make some security schemes based on WMF protocol used in the Internet of things or other fields get security alerts. The results also show that our method is effective, and it can provide a direction for the analysis of other security protocols with timestamp in many fields.