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

摘要：

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

关键词：拟态自动机、模型检测、MSISDN虚拟化、拟态防御

分类号：TP309(计算技术、计算机技术)

资助基金：国家自然科学基金联合基金U1204608;国家重点研发计划2016YFB0800100

在线出版日期：2018-10-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：15-22