通信学报 ›› 2018, Vol. 39 ›› Issue (3): 63-75.doi: 10.11959/j.issn.1000-436x.2018042

• 论文Ⅰ:物联网与安全 • 上一篇    下一篇

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

王国卿,庄雷(),王瑞民,宋玉,张坤丽   

  1. 郑州大学信息工程学院,河南 郑州 450001
  • 修回日期:2018-02-20 出版日期:2018-03-01 发布日期:2018-04-02
  • 作者简介:王国卿(1989-),男,山东临沂人,郑州大学博士生,主要研究方向为模型检测、形式化分析、物联网安全等。|庄雷(1963-),女,山东日照人,博士,郑州大学教授、博士生导师,主要研究方向为模型检测、未来网络架构、网络虚拟化等。|王瑞民(1974-),男,河南安阳人,博士,郑州大学副教授,主要研究方向为密码学、信息安全、物联网安全等。|宋玉(1969-),男,河南邓州人,郑州大学副教授,主要研究方向为数据挖掘、物联网体系结构、人工智能等。|张坤丽(1977-),女,河南巩义人,郑州大学讲师,主要研究方向为人工智能、自然语言处理等。
  • 基金资助:
    国家自然科学基金资助项目(61379079);河南省科技攻关计划基金资助项目(172102210478);河南省国际科技合作计划基金资助项目(152102410021)

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

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

  1. School of Information Engineering,Zhengzhou University,Zhengzhou 450001,China
  • Revised:2018-02-20 Online:2018-03-01 Published:2018-04-02
  • Supported by:
    The National Natural Science Foundation of China(61379079);The Science and Technology Key Project of Henan Province(172102210478);The International Cooperation Program of Henan Province(152102410021)

摘要:

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

关键词: 物联网网关, 安全系统, 中间件, 时间自动机, 模型检测

Abstract:

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.

Key words: IoT gateway, security system, middleware, timed automata, model checking

中图分类号: 

[1] 李 颖,魏急波. 裁减自动球形译码算法与性能分析[J]. 通信学报, 2007, 28(5): 8 -54 .
[2] 包先雨,蒋建国,袁 炜,李 援. H.264/AVC标准中基于CABAC的数字视频加密研究[J]. 通信学报, 2007, 28(6): 5 -29 .
[3] 战金龙,卢建军,卢光跃. 新的GLSFBC-CDMA-OFDMA发射方案[J]. 通信学报, 2012, 33(4): 14 -106 .
[4] 李方伟,李 晗,卢 晓. TD-SCDMA系统中多速率业务的接纳控制算法研究[J]. 通信学报, 2012, 33(4): 24 -182 .
[5] 胡玉鹏,罗昊,林亚平,秦拯,尹波. 社会网络中时空周期行为模式挖掘算法[J]. 通信学报, 2013, 34(1): 8 -18 .
[6] 陈晓华,李春芝,陈良育,曾振柄. 虚拟网络映射最小费用流模型及算法[J]. 电信科学, 2014, 30(6): 90 -94 .
[7] “基于大数据的互联网化存量经营”项目组,“基于用户感知的运维转型”项目组. 运营商存量经营大数据平台及其关键技术研究[J]. 电信科学, 2014, 30(6): 118 -125 .
[8] 沈成彬,王成巍,蒋铭,王波. 下一代PON技术的进展与应用[J]. 电信科学, 2010, 26(8): 1 -7 .
[9] 王晓鹏,王纯. 基于OSGi和RCP的融合通信客户端的设计与实现[J]. 电信科学, 2010, 26(8): 35 -41 .
[10] 刘军1,孙茜1,王英梅2,叶宁1,沙明博3. 支持网络编码的认知无线自组网拓扑控制算法[J]. 通信学报, 2013, 34(5): 16 -142 .