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

摘要

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