With the progress in software refinement verification methods and theorem provers such as Isabella/HOL and VCC, researchers begin to study the design and modeling of security protocols and verify the correctness of their source codes based on the refinement technique and theorem provers. In this paper, the event-B method and verification tools Isabelle/HOL and VCC are introduced, and the typical work on the design and modeling of security protocols and verification of the correctness of their source codes is surveyed. These work include:the refinement design method of security protocols, the refinement modeling method of TPM-based protocol applications, and the refinement verification method of source code.