TLA is a logic which combines the temporal logic and the logic of action,describing and validating the concurrent systems with TLA. TLA can express the system and the corresponding properties by adding actions and behaviors.First,this paper introduces the grammer,semantics and simple reasoning rules, and then formally analyzes the NS protocol, and sets up the FSM model, and specifies the model with TLA+, and then checks the corresponding properties with the tool of TLC. The results of checking shows there exists middleman’s replay attack.