动态虚拟MSISDN的拟态自动机模型与安全性验证方法

移动通信MSISDN号码对外公开,导致用户数据信息泄露或被恶意窃取。动态虚拟MSISDN号码通过引入拟态防御机制,可实现用户信息防泄露和防窃取。然而,对于该技术在全状态空间的安全性,目前尚缺乏有效的分析方法。文章首先使用有穷状态自动机描述动态虚拟MSISDN的状态迁移;使用细胞自动机描述动态虚拟MSISDN的变化结构;使用层次自动机描述动态虚拟MSISDN的不同计算粒度。其次,将各种自动机按照一定的逻辑关系组织起来,即可获得描述动态虚拟MSISDN内在行为的拟态自动机模型。然后,使用特定的线性时序逻辑公式描述动态虚拟MSISDN安全性。最后,将动态虚拟MSISDN安全性问题按如下方式规约为拟态自动机模型检测问题:若模型检测结果指出拟态自动机满足给定的线性时序逻辑公式,则动态虚拟MSISDN满足安全性;若模型检测结果指出拟态自动机不满足给定的线性时序逻辑公式,则动态虚拟MSISDN不满足安全性。由此便可在全状态空间上自动验证动态虚拟MSISDN的安全性。仿真实验证实了文中方法的高效性。