Abstract: The model checking technology was used, and the method of modeling the fast handover authentication protocol FHAM by HLPSL language and analyzing it by AVISPA based on Dolev-Yao model was used. The test results show that the protocol is secure, able to resist many types of malicious attacks, and achieves the desired security goals.