Abstract:

MSISDN (Mobile Station International ISDN) numbers are used as communication identifiers and they are open to the public, causing users’ information is stolen. MSISDN virtualization can protect user data by introducing the mimic defense mechanism. However, the security of this technique cannot be analysis in the whole state space due to the lack of method. First, one can use a finite state automaton to describe the state transitions of the MSISDN virtualization. A cellular automaton is employed to describe the dynamic structure of the MSISDN virtualization. A hierarchical automaton is employed to express the different granularities of the MSISDN virtualization. Second, a mimic automaton is obtained by combining the various types of automata mentioned above in the certain logical relationship. And this mimic automaton can describe the behaviors of MSISDN virtualization. Third, a given formula in linear temporal logic (LTL) can express the security property of MSISDN virtualization. Final, the security problem of the MSISDN virtualization is reduced to the following LTL model checking problem. The MSISDN virtualization satisfies the security requirement, if the model checking result shows that the mimic automaton satisfies this given LTL formula. The MSISDN virtualization does not satisfy the security requirement, if the model checking result shows that the mimic automaton does not satisfy the given LTL formula. On the basis of it, one can automatically verify the security property of the MSISDN virtualization in the whole state space. And the simulations demonstrate the efficiency of the new method.

Key words: mimic automaton, model checking, MSISDN virtualization, mimic defense