Intensive Model Used in Secure Protocol Analysis

Strand space inherits the merit of algebra method, which can prove the security of protocol more precisely. Meanwhile, it overcomes the shortcoming of inconvenience. But because of shortage of primitives, it can´t describe some protocols as IKE, let alone verification. This paper makes an improvement to the original strand space by adding the description of hash function and some definitions and lemmas about the description. So we can use the intensive model to analyze the protocols using hash function. At last, we analyze one IKE sub-protocol protocol.