Research on Verification Method of Mutual Authentication in GSM/UMTS Inter-System Based on Finite State Machine

GSM and UMTS radio network will coexist for a long time. Interoperation of GSM and UMTS network will be a more important issue in the future. The authentication mechanism is key problem in GSM/UMTS inter-system. The verification method based on finite state machine is an important method to describe the state changes of complex and interactive system. It is simple formally and easy to describe target system and the proving procedure of finite state machine can be deduced. In this paper we use it to verify the GSM/UMTS authentication procedure. The deduction result shows that the state changes of both mobile station and network side is safe. The procedure also shows that the verification method based finite state machine is efficient and can be used in other complex system.