Secure authenticated key agreement protocol for WMEN based on protocol composition logic

This paper formally analyzes the WMEN authenticated key agreement scheme SKE using protocol composition logic (PCL) and detects interleaving attack exists in the protocol. According to identity-based key agreement, a novel WMEN security authenticated and key agreement protocol is deduced based on the protocol derivation system (PDS). Modular correctness and security of the novel protocol are proved by protocol composition logic (PCL). At the same time, the new scheme is analyzed and compared with the original scheme. Experiments show that the new scheme is identity-authenticated, key-secretive and forward-secure. Besides, it can defense the interleaving attack effectively.