Abstract: Mobile users utilize various accessing technologies to connect next generation mobile internet，which is composed by multiple heterogeneous networks.The networks of different security levels make it difficult to manage access control and handover.A multilevel network handover model is set up in this paper to analyze the handover security problem.In order to solve the security problem in continuous handovers，security handover policies are brought forward based on Multilevel Security（MLS） policy.It proves the security policies using formal methods.

Key words: mobile environments, multilevel security, continuous handover, formal method

摘要： 将异构移动网络抽象成多级网络模型，将多级安全引入切换过程，设计了基于MLS（Multilevel Security）的安全切换策略。该策略针对用户连续切换产生的信息泄露问题，规定保证安全等级不降低的约束条件，保证切换过程中用户与网络的安全，并且与其他方案相比，能够提供更全面的安全保护。经形式化证明，该策略是安全的。

关键词: 移动环境, 多级安全, 连续切换, 形式化方法