Security of network software such as Web applications has drawn much attention in the industry.Modeling and verifying Web applications involving intricate interactions are a challenge to software developers.In this paper, we propose a threaten-driven approach to model and verify the on-the-fly navigation model of Web applications. Security properties are extracted from the model based on the threaten-driven method. Using the model checking tool NuSMV, we have verified the model. The experimental results indicate that the proposed approach can avoid state space explosion to a certain extent.