基于时间自动机的物联网网关安全系统的建模及验证

2018-04-19王国卿庄雷王瑞民宋玉张坤丽

通信学报 2018年3期

王国卿，庄雷，王瑞民，宋玉，张坤丽

王国卿，庄雷，王瑞民，宋玉，张坤丽

（郑州大学信息工程学院，河南郑州 450001）

物联网是一个多网异构融合网络，其感知层常面临各类安全威胁。物联网网关作为感知层和网络层的桥梁，应当具备安全管理功能，防止安全问题向上层扩散。针对物联网网关目前安全方面的不足，以物联网网关中间件技术为平台，设计一个通用的物联网网关安全系统。该系统可以嵌入不同的安全协议或算法，然后进行建模与分析，能够辅助安全网关的设计和具体实现。利用时间自动机对系统进行形式化建模与验证，验证结果表明物联网网关安全系统满足机密性、可用性、真实性、顽健性、完整性和新鲜性6项安全需求。

物联网网关；安全系统；中间件；时间自动机；模型检测

1 引言

随着第4次工业革命的到来，人类社会正逐步进入一个万物互联的时代，物联网（IoT, Internet of things）应运而生。物联网是继计算机、互联网和移动通信之后的又一次革新发展，是信息化时代的重要发展阶段[1]。物联网是由具有自我标识、感知和智能的物理实体基于通信技术相互连接而成的网络，这些物理实体可以自发地进行协同和互动，以实现智能的识别、定位、监控和管理，从而将人类社会、信息空间和物理系统进行有机的融合[2]。

物联网的体系结构如图1所示，共分为3层。其中，感知层负责随时获取物理实体的信息，并将应用层指令反馈给物理实体；网络层负责实时传输各类信息、数据和指令；应用层负责对海量数据和信息进行分析、处理及决策，接收用户的服务定制。3个层次并不是相互独立的，而是相互支撑、相互影响的，进而搭建起整个体系架构。

网关技术在传统互联网中的运用比较成熟，应用到物联网体系中，将成为连接感知网络与传统通信网络的纽带。作为物联网网关，可以实现感知网络与通信网络以及不同类型感知网络之间的协议转换[3]。物联网网关还可以提供管理功能和安全策略[4]。通过物联网网关设备可以管理底层的感知节点和运行设备，监测各物理实体的运行状态，实现远程控制；带有安全策略的物联网网关可以屏蔽传感器网络和移动通信网的异构性，实现从协议级到应用级的保护。

在物联网网关的体系结构方面，许多学者设计并实现了网关的基本功能[5~8]，主要包括感知接入、协议适配、协议转换、消息传输等，解决了物联网网关的关键问题，即对异构网络的不同通信协议进行转换和底层通信协议到上层通信协议的转换，并在物联网网关的管理与控制时，建立可统一识别指令及标准。但在网关安全方面没有详细设计，或默认安全策略已经完备，或只是简单说明而没有具体实现。

图1 物联网体系结构

关于物联网网关安全方面的研究，文献[9]针对IoT中机器对机器（M2M, machine to machine）通信，设计了一个安全网关应用（SGA, security gateway application），其中，包括对称密钥加密协商功能、安全密钥交换生成功能和信息安全传递功能，能够满足M2M服务层的基本安全需求；文献[10]设计了一种基于动态优先级调度算法的异构物联网网关，可支持RS485、蓝牙、ZigBee等协议，通过实现高层协议保证了物联网网关的数据安全性和可靠性；文献[11]提出了一种结合物联网智能设备与控制系统网关的实时响应模型，通过加强身份验证与授权的控制，以提高系统的安全性；文献[12]讨论了传感器网络、家庭网关和应用终端的安全问题及相应的解决方案，通过对这3个部分安全性进行有机整合，实现信息传输和用户隐私的安全保护，最大限度地保护智能家居的安全；文献[13]设计实现了基于Modbus协议的物联网汇聚安全网关，通过在应用层构建网关覆盖网，提供网关信任管理，有效解决了网关海量数据的拥塞控制问题，保证了网关虚拟网络的安全性。上述研究成果大多针对某一特殊场景，例如，文献[11,13]主要应用于工业物联网，文献[12]主要应用于智能家居。文献[9,10]虽然应用场景更宽泛一些，但在安全体系的设计上存在一些不足。文献[9]集中考虑了密钥管理体系，对其他安全技术没有涉及；文献[10]的安全网关在应用层级，没有考虑连接感知层和网络层的网关安全性。

基于对当前研究现状的分析，针对物联网网关安全方案存在的不足，利用物联网安全常用的密钥管理、身份认证、入侵检测等技术，设计了一个通用的物联网网关安全系统。通过对系统的形式化分析与验证，保证了系统的机密性、可用性、真实性、顽健性、完整性、新鲜性等相关安全特性，为网关中间件的设计和实现提供了理论框架。物联网网关安全系统可以嵌入各类安全协议或算法，然后进行建模与分析，验证系统是否正确与可靠，对网关的具体设计和实现具有指导意义。

2 物联网网关安全系统的设计

物联网是信息技术发展的趋势，物联网应用在给人们生活带来便利的同时，也带来了很多安全隐患。尤其物联网感知层作为物联网体系结构的底层，直接面向现实环境，承担着信息感知和命令执行的重任，其安全问题尤为重要。

物联网网关作为感知层和网络层的桥梁，由于硬件设备的迅猛发展，其功能不再局限于单一的协议转换，可以向服务提供、设备管理、安全检测等功能扩展[14]；中间件技术可屏蔽底层硬件细节，对外提供统一抽象接口，使用跨层设计的思想，在满足应用动态性的同时可满足应用异构性，为安全系统的实现提供了平台[15]。

2.1 物联网网关安全需求

物联网感知层的安全异常重要，作为底层感知和执行设备，所有物联网应用能否正常运行全部依赖于感知层是否安全可靠。由于感知层自身有限的存储空间和计算能力、有限的带宽和通信能量以及网络协议安全形式的多样，感知层经常面临通信信道攻击、拒绝服务攻击、节点捕获、假冒攻击、路由协议攻击等安全威胁[16]，如表1所示。

表1 物联网感知层面临的安全威胁

针对上述安全威胁，物联网网关需要弥补感知层能力的不足，避免安全缺陷从感知层通过网关传递到网络层，应满足以下6个方面的安全需求[17]。

1) 机密性：消息对非授权方是保密的。

2) 可用性：按约定向合法用户提供服务。

3) 真实性：消息认证能够核实来源的真实。

4) 顽健性：面对不确定因素具有强适应性。

5) 完整性：收到的信息与源信息完全一致。

6) 新鲜性：保证消息的时效性。

网关技术具有有效的安全隔离、灵活的业务代理、成熟的技术积累等特点。为了应对感知层安全威胁，避免感知层安全问题向上扩散，信息加密、认证与访问控制、入侵检测等信息安全技术可以综合运用到物联网网关安全系统中，能够和其他相关技术实现较好的衔接，从而满足物联网网关安全需求。基于网关中间件及安全支撑平台构建的物联网网关安全技术框架如图2所示。

2.2 网关安全系统的逻辑流程

在传感器网络中，节点通过各种方式大量部署在被感知对象内部或附近，这些节点通过自组织方式构成无线网络，以协作的方式感知、采集和处理网络覆盖区域中特定的信息，可以实现对任意地点信息在任意时间的采集、处理和分析。对于新加入或退出的节点，自组织网络可设定生存时间检测，通过多跳的方式连接至汇聚节点，节点收到数据连接安全网关，整个系统通过任务管理器来管理和控制。

图2 物联网网关安全技术框架

根据所设计的物联网网关安全技术框架，物联网网关安全系统实现在物联网网关中间件平台上，其在完成物联网网关基本功能的基础上，添加了加密传输、轮询检测、身份校验、异常处理等子模块。物联网网关安全系统的逻辑流程如图3所示。

为了便于建模与检测，仅抽取主要流程分析并进行适当假设。物联网网关安全系统的顶层主模块在网关进行消息转发等基本功能的基础上实现了网关合法性认证及入侵检测，以确保网关的安全启动和运行，然后进入中间层轮询模块。终端在轮询时一般处于工作状态，需要安全系统发出控制指令检测终端状态。对于感知终端，由于感知节点的大规模和随机性，安全系统主要连接汇聚节点进行监测，汇聚节点的处理能力、存储能力、通信能力相对较强，在实现通信协议栈转换的同时，可发布网关的监测任务。对于执行终端，如果设备正在运行，则令设备在合法时间内运行一段时间，如果在规定时间内设备状态能正确返回到安全系统，则认为轮询成功，设备处于正常状态，生成监控信息。底层主要提供了密钥算法、统一认证、入侵检测、异常处理等安全服务，应用于顶层和中间层的各个环节，以保证安全系统整体的安全可靠。

若暂不考虑底层安全服务模块所选策略，设网关安全系统所需管理的终端数为，则顶层主模块的时间复杂度为()，中间层轮询模块的时间复杂度为(2)，所以网关安全系统的时间复杂度为(2)。若进一步考虑底层安全服务模块，则时间复杂度受到底层所选策略的影响可能会提高，但由于底层所选策略通常是成熟的算法，因此，应用到网关安全系统中的总时间复杂度是可以接受的。

3 基于时间自动机的网关安全系统建模

由于物联网网关安全系统不仅需要满足运行结果的逻辑正确性，部分功能还需要满足时间的正确性，因此，选择时间自动机进行形式化分析，可有效刻画物联网网关安全系统的时间属性，并可借助模型检测工具UPPAAL进行验证。

3.1 预备知识

图3 物联网网关安全系统的逻辑流程

根据物联网网关安全系统流程的分层设计，可考虑引入层次时间自动机进行建模，它以层次方式对时间自动机进行了扩展，能有效解决建模时的复杂流程与蕴含逻辑。

3.2 形式化表示

使用层次时间自动机建模，整个系统表示为3个层次。

表2 模型中状态位置的含义

其中，Top表示顶层主模块，Middle表示中间层轮询模块，底层安全服务模块包括KMS密钥管理系统、AC认证中心、IDS入侵检测系统及Exception异常处理。模型中状态位置、同步通道、变量等符号的含义如表2~表4所示。

表3 模型中同步通道的含义

表4 模型中变量的含义

图4 顶层主模块模型（Top）

中间层及底层各模块形式化模型依据顶层主模块模型，结合图例较容易得出，限于篇幅不再详述。

3.3 层次化建模

根据层次时间自动机的定义，首先建立顶层主模块模型，如图4所示。

对于中间层轮询模块，通过通道StartMiddle开启轮询，并由通道FinishMiddle返回顶层主模块。CheckCategory状态控制轮询逻辑的终端是感知终端还是执行终端，两者有不同的流程处理。所建立的中间层轮询模块模型如图5所示。

图5 中间层轮询模块模型（Middle）

当=2时，对感知终端进行轮询；当=3时，对执行终端进行轮询。在2个轮询流程中，根据不同的需求通过同步通道调用底层安全服务，具体过程可由状态位置、同步通道、变量的含义解读，在此不再赘述。特别地，在等待计时阶段和设备保持运行状态阶段也添加了时间约束，例如，执行终端需在5个时间单位内返回运行状态，持续运行需保持25个时间单位以上，以此来保证安全需求的新鲜性。

顶层主模块模型和中间层轮询模块模型是物联网网关安全系统的通用框架，其安全性的实现最终依赖于底层的安全服务模块，因此，需要完善底层安全服务模块的模型构建。图3中给出了底层各个安全服务子模块的常用算法或协议，用户可根据实际场景和需要选择适合的算法协议，然后在此框架下进行相应的建模分析，从而指导网关安全系统在网关中间件平台的设计与实现。

为了验证所设计的物联网网关安全系统是否满足安全需求，拟选取基于时间标签的AES密码算法[20]为核心，建立密钥管理、身份认证、入侵检测及异常处理模型。需要说明的是，加、解密是密钥管理系统常用的逻辑流程，为使结构更加清晰，分别对加、解密进行了单独建模。底层安全服务模块建模如图6~图11所示。

图6 密钥管理系统模型（KMS）

图7 AES算法加密模型（AESEncryption）

图8 AES算法解密模型（AESDecryption）

图9 认证中心模型（AC）

图10 入侵检测系统模型（IDS）

图11 异常处理模型（Exception）

简要对密钥管理系统模型和基于时间标签的AES密码算法进行介绍，其他安全服务模型限于篇幅不再赘述。密钥管理系统首先检测，如果=1，则更新密钥，与终端通信获取终端密钥信息进行解密校验，判断是否需要更新，若需要更新则通过数据中心密钥池分配新的密钥，然后加密传送回终端；如果=2，则验证密钥，将终端传来的密文进行解密，然后提交数据中心比对处理，最后记录数据中心反馈的验证信息。

AES密码算法包括加密过程、解密过程和密钥扩展过程。其加密过程共10轮（或12轮、14轮），前9轮（或前11轮、前13轮）由字节代换、行移位、列混合和加轮密钥等4种变换迭代完成，最后一轮没有列混合变换；解密过程与加密过程的轮数一致，并且前若干轮变换是加密过程的逆变换，依次是逆字节代换、逆行移位、逆列混合和加轮密钥变换，最后一轮没有逆列混合变换。基于时间标签的AES密码算法是在密钥扩展阶段引入时间标签，使轮密钥可随时间的变化进行动态更新，进而实现密文的变化，可以更有效地保证机密信息的安全性。因此，在建模过程中对加、解密模型的部分状态位置和边界添加了时间约束，以体现时间标签属性。

4 网关安全系统的形式化验证

可以对建立好的物联网网关安全系统的层次时间自动机模型使用模型检测工具UPPAAL进行验证，能够有效发现模型的错误，并验证模型的安全性质是否满足。

4.1 UPPAAL工具简介

UPPAAL[21]是瑞典Uppsala大学和丹麦Aalborg大学于1995年联合发布的基于时间自动机的自动化验证工具，其名字的由来是2所学校名称的前3个字母组合。UPPAAL的操作界面包含编辑器（editor）、模拟器（simulator）、验证器（verifier）3个部分。编辑器用于对要分析的问题进行建模和编辑，是一个图形化交互界面，可进行自定义及编程；模拟器用于模拟模型的执行过程，可选择步进执行或随机执行，工具将生成时序图和消息控制序列，以帮助设计者发现错误原因和路径；验证器用于验证给定性质是否满足，在每个性质验证结束后给出验证结果、验证时间和内存消耗，性质的表示使用巴科斯范式（BNF, Backus-Naur form）描述。

4.2 安全需求性质的验证

本文通过编辑器建立物联网安全系统模型，可以在模拟器模拟各层次的交互情况。时序图详细展示了各层次对象间的交互情况及各时间自动机模型的执行情况，消息控制序列以图文形式展示了各对象的运行流程和通信状态，它们对于模型的分析和调试有极大帮助。

模拟器的模拟运行，其择路条件随机，不一定能够完全遍历模型状态，因此，需要使用验证器进行全面验证。2.1节提到，物联网网关的安全需求需要满足机密性、可用性、真实性、顽健性、完整性、新鲜性6个性质，使用BNF语法对上述性质进行公式化表示，然后利用验证器进行验证。

1) 机密性验证

A[] AC.AlertToManager imply==0

加密信息通过网关时，若密钥验证失败，则安全监控逻辑进行报警，拒绝消息继续传输。

2) 可用性验证

在顶层模型，检测网关认证状态可达，可确保网关的合法身份和轮询周期的不断进行；中间层及底层各模型入口状态可达，可确保为用户提供相应服务。待验证性质表示如下。

E<> Top.CheckGS

E<> Top.EnterMiddle imply Middle.CheckCateg-ory

E<> Middle.UpdateKey imply KMS.CheckKT

E<> Top.Authentication imply AC.CheckCate-gory

E<> Middle.IntrusionDetection imply IDS.Init

E<> Top.Verify imply Exception.CheckEL

3) 真实性验证

E<>==1 imply AC.==1

在消息认证时，需要同步验证消息来源节点的私钥以认证身份的合法性。如果认证中心的认证成功，则认为终端状态正常，说明源节点是系统内节点，而不是外部伪造的。

4) 顽健性验证

A[] not deadlock

系统不存在死锁，即面对任何情况都有处理路径可执行。

5) 完整性验证

A[] AC.ObtainMessage imply AC.==1

消息认证码（MAC, message authentication code）可同时提供基于校验和的数据完整性和基于秘密密钥的数据源完整性。如果接受的消息最终通过Hash运算处理后，2次计算的值相等，则认为数据未被篡改，解密并获取发送方的信息。

6) 新鲜性验证

整个模型中设置了多处时间约束，目的就是保证消息的时效性。待验证性质表示如下。

A[] Top.Restart imply≤300

A[] Top.Record imply≤600

A[] Middle.RetrieveData imply Middle.≥30

A[] Middle.WaitDevice imply Middle.≤5

A[] IDS.Analysis imply IDS.≤60

A[] AESEncryption.MUX imply AESEncryption.≤4

A[] AESDecryption.InShiftRows_ imply≥100

UPPAAL验证器对上述6个性质的全部语句逐条进行验证，验证结果如表5所示。

表5 模型检测结果

验证结果表明，所有性质均通过验证，所设计的物联网安全系统满足机密性、可用性、真实性、顽健性、完整性、新鲜性等安全需求。

5 结束语

物联网作为新一代信息技术的重要组成部分，安全问题应当得到足够重视。物联网感知层直面真实环境，其底层感知和执行设备常常面临各类安全威胁。物联网网关负责连接感知层与网络层，可弥补感知层能力的不足，避免安全问题的进一步扩散。目前，对物联网网关体系结构的研究主要解决了基本功能的实现，安全策略涉及不多；对物联网网关安全措施的研究一般都有实际应用背景，可借鉴性与通用性不强。

基于上述分析，结合现有的密钥管理、身份认证、入侵检测等安全技术，设计了一个通用的物联网网关安全系统，可在网关中间件平台部署。利用时间自动机对系统3个层次进行形式化建模，并使用模型验证工具UPPAAL进行性质验证，结果表明网关安全系统满足机密性、可用性、真实性、顽健性、完整性、新鲜性等安全性质。物联网网关安全系统还可以根据实际需要调整底层安全协议或算法，然后重新进行建模分析，有助于发现设计漏洞，辅助网关的设计和实现。

下一步研究工作的重点有2个方面。

1) 进一步研究其他安全协议或算法的建模方法，以便有效嵌入物联网网关安全系统，从而提升系统的普适性。

2) 结合物联网网关的硬件设备及中间件技术，在实际环境中具体实现物联网网关安全系统。

[1] 王良民, 熊书明. 物联网工程概论[M]. 北京: 清华大学出版社, 2011:45-52.

WANG L M, XIONG S M. The introduction of IoT engineering[M]. Beijing: Tsinghua University Press, 2011:45-52.

[2] 钱志鸿, 王义君. 物联网技术与应用研究[J]. 电子学报, 2012, 40(5):1023-1029.

QIAN Z H, WANG Y J. IoT technology and application[J]. Acta Electronica Sinica, 2012, 40(5):1023-1029.

[3] MORABITO R, BEIJAR N. A framework based on SDN and containers for dynamic service chains on IoT gateways[C]//The Workshop on Hot Topics in Container Networking and Networked Systems. 2017:42-47.

[4] SATHYADEVAN S, VEJESH V, DOSS R, et al. Portguard an authentication tool for securing ports in an IoT gateway[C]//IEEE International Conference on Pervasive Computing and Communications Workshops. 2017:624-629.

[5] SCHRICKTE L F, MONTEZ C B, OLIVEIRA R S D, et al. Design and implementation of a 6LoWPAN gateway for wireless sensor networks integration with the internet of things[J]. International Journal of Embedded Systems, 2016, 8(5/6):380-390.

[6] 陈琦, 韩冰, 秦伟俊, 等. 基于Zigbee/GPRS物联网网关系统的设计与实现[J]. 计算机研究与发展, 2011, 48(s2):367-372.

CHEN Q, HAN B, QIN W J, et al. Design and implementation of the IoT gateway based on Zigbee/GPRS protocol[J]. Journal of Computer Research and Development, 2011, 48(s2):367-372.

[7] ZHANG L, ALHARBE N R, ATKINS A S. A self-adaptive distributed decision support model for Internet of things applications[J]. Transactions of the Institute of Measurement and Control, 2017, 39(4): 404-419.

[8] 罗俊海, 周应宾, 邓霄博. 物联网网关系统设计[J]. 电信科学, 2011, 27(2):105-110.

LUO J H, ZHOU Y B, DENG X B. Design for gateway system in Internet of things[J]. Telecommunications Science, 2011, 27(2): 105-110.

[9] CHEN H C, YOU I, WENG C E, et al. A security gateway application for end-to-end M2M communications[J]. Computer Standards & Interfaces, 2016, 44(C):85-93.

[10] MIN D, XIAO Z, SHENG B, et al. Design and implementation of heterogeneous IoT gateway based on dynamic priority scheduling algorithm[J]. Transactions of the Institute of Measurement and Control, 2014, 36(7):924-931.

[11] CONDRY M W, NELSON C B. Using smart edge IoT devices for safer, rapid response with industry IoT control operations[J]. Proceedings of the IEEE, 2016, 104(5):938-946.

[12] LI F, WAN Z, XIONG X, et al. Research on sensor-gateway-terminal security mechanism of smart home based on IoT[C]//IoT Workshop 2012, CCIS 312. 2012: 415-422.

[13] 石希, 陈震, 汪东升, 等. 物联网汇聚安全网关关键技术研究[J]. 信息网络安全, 2012(6):85-89.

SHI X, CHEN Z, WANG D S, et al. A research of the key technology of the aggregative security gateway of Internet of things[J]. Netinfo Security, 2012(6):85-89.

[14] SERDAROGLU K C, BAYDERE S. WiSEGATE: wireless sensor network gateway framework for Internet of things[J]. Wireless Networks, 2015, 22(5):1-17.

[15] 罗娟, 顾传力, 李仁发. 基于角色的无线传感网络中间件研究[J]. 通信学报, 2011, 32(1):79-86.

LUO J, GU C L, LI R F. Researches on role-based middleware in wireless sensor networks[J]. Journal on Communications, 2011, 32(1):79-86.

[16] 杨光, 耿贵宁, 都婧, 等. 物联网安全威胁与措施[J]. 清华大学学报(自然科学版), 2011, 51(10):1335-1340.

YANG G, GENG G N, DU J, et al. Security threats and measures for the Internet of things[J]. Journal of Tsinghua University (Science and Technology), 2011, 51(10):1335-1340.

[17] 王浩, 郑武, 谢昊飞, 等. 物联网安全技术[M]. 北京: 人民邮电出版社, 2016:5-17.

WANG H, ZHENG W, XIE H F, et al. IoT security technology[M]. Beijing: Posts & Telecom Press, 2016:5-17.

[18] ALUR R, DILL D L. A theory of timed automata[J]. Theoretical Computer Science, 1994, 126(2):183-235.

[19] DAVID A, OLIVER M M. From HUPPAAL to UPPAAL: a translation from hierarchical timed automata to flat timed automata[R]. BRICS Report Series RS-01-11, Department of Computer Science, University of Aarhus, 2001.

[20] YIN A, WANG S. A novel encryption scheme based on timestamp in gigabit ethernet passive optical network using AES-128[J]. Optik, 2014, 125(3):1361-1365.

[21] BEHRMANN G, DAVID A, LARSEN K G. A tutorial on UPPAAL[M]//Formal Methods for the Design of Real-Time Systems. Springer Berlin Heidelberg, 2004:200-236.

Modeling and verifying based on timed automata of Internet of things gateway security system

WANG Guoqing, ZHUANG Lei, WANG Ruimin, SONG Yu, ZHANG Kunli

School of Information Engineering, Zhengzhou University, Zhengzhou 450001, China

The Internet of things (IoT) is a multiple heterogeneous network, and its perception layer is often faced with various security threats. As the bridge between the perception layer and the network layer, the IoT gateway should have the security management function to prevent the security issue from spreading to the upper layer. According to the current security deficiencies in IoT gateway, a universal IoT gateway security system was proposed based on the IoT gateway middleware technology. Various security protocols or algorithms can be embedded in IoT gateway security system, and the modeling and analysis can help the design and implementation of IoT gateway. The formal modeling and verification of the IoT gateway security system was performed by timed automata. The results show that the IoT gateway security system satisfies the security properties of confidentiality, availability, authenticity, robustness, integrity and freshness.

IoT gateway, security system, middleware, timed automata, model checking

TP393

10.11959/j.issn.1000-436x.2018042

2017-10-12；

2018-02-20

庄雷，ielzhuang@zzu.edn.cn

国家自然科学基金资助项目（No.61379079）；河南省科技攻关计划基金资助项目（No.172102210478）；河南省国际科技合作计划基金资助项目（No.152102410021）

The National Natural Science Foundation of China (No.61379079), The Science and Technology Key Project of Henan Province (No.172102210478), The International Cooperation Program of Henan Province (No.152102410021)

王国卿（1989-），男，山东临沂人，郑州大学博士生，主要研究方向为模型检测、形式化分析、物联网安全等。