LTE网间切换安全机制的形式化分析

Formal analysis of inter-RAT handover protocol in LTE

通过分析3GPP LTE网间切换安全协议,发现通过监听网络消息的方式,入侵者可以在协议的信息交互过程中获取协议的2个核心密钥,并将其用于非法活动而不会被系统发现.为了解决这一问题,在保留原协议信息交互框架的基础上,提出了一种改进的3GPP LTE网间切换安全协议.该改进协议引入了公钥体系,保证密钥不会因为第三方的截取而泄露;同时,改进的协议还为关键消息提供了消息传递双方的双向认证过程,不仅能保证消息传递双方身份,还能确保消息不会被第三方随意修改.最后,应用串空间模型理论及认证测试方法,从协议的机密性与认证的正确性2个方面形式化地检验了改进协议的安全性.结果表明,改进的协议能够有效地保证消息的机密性与认证的正确性,从而确保协议的安全.

Through analyzing the inter-RAT（radio access technology） handover security protocol of the third generation partnership project（3GPP） long term evolution（LTE）,a security flaw is pointed out.By monitoring network messages,intruders can get and use the keys without being found by network in the exchanging procedure.To solve this problem,an improved protocol which keeps the frame of the 3GPP＇s protocol is given.In this protocol,the public key system is introduced to keep the core key from stealing.Meanwhile,the mutual authentication for important messages,which can not only ensure the identity of both sender and receiver but also avoid the message modification by other people,is provided.Finally,the security of the improved protocol is formally proved with the strand space model and authentication tests from the aspects of confidentiality and the correctness of authentication.The results indicate that the improved protocol can guarantee the confidentiality and freshness of messages,which guarantees the protocol＇s security.