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

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

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

您当前的位置：

首页 >

文章列表页 >

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

论文Ⅰ：物联网与安全 | 更新时间：2024-06-05

- 基于时间自动机的物联网网关安全系统的建模及验证
- Modeling and verifying based on timed automata of Internet of things gateway security system
- 通信学报 2018年39卷第3期页码：63-75
- 作者机构：
  
  郑州大学信息工程学院，河南郑州 450001
- 作者简介：
  
  [ "王国卿（1989-），男，山东临沂人，郑州大学博士生，主要研究方向为模型检测、形式化分析、物联网安全等。" ]
  [ "庄雷（1963-），女，山东日照人，博士，郑州大学教授、博士生导师，主要研究方向为模型检测、未来网络架构、网络虚拟化等。" ]
  [ "王瑞民（1974-），男，河南安阳人，博士，郑州大学副教授，主要研究方向为密码学、信息安全、物联网安全等。" ]
  [ "宋玉（1969-），男，河南邓州人，郑州大学副教授，主要研究方向为数据挖掘、物联网体系结构、人工智能等。" ]
  [ "张坤丽（1977-），女，河南巩义人，郑州大学讲师，主要研究方向为人工智能、自然语言处理等。" ]
- 基金信息：
  
  国家自然科学基金资助项目(61379079);河南省科技攻关计划基金资助项目(172102210478);河南省国际合作基金资助项目(152102410021)
- DOI：10.11959/j.issn.1000-436x.2018042
  中图分类号： TP393
- 网络首发：2018-03，
  
  纸质出版：2018-03-25
- 稿件说明：
移动端阅览
王国卿, 庄雷, 王瑞民, 等. 基于时间自动机的物联网网关安全系统的建模及验证[J]. 通信学报, 2018,39(3):63-75.

Guoqing WANG, Lei ZHUANG, Ruimin WANG, et al. Modeling and verifying based on timed automata of Internet of things gateway security system[J]. Journal on Communications, 2018, 39(3): 63-75.
王国卿, 庄雷, 王瑞民, 等. 基于时间自动机的物联网网关安全系统的建模及验证[J]. 通信学报, 2018,39(3):63-75. DOI： 10.11959/j.issn.1000-436x.2018042.

Guoqing WANG, Lei ZHUANG, Ruimin WANG, et al. Modeling and verifying based on timed automata of Internet of things gateway security system[J]. Journal on Communications, 2018, 39(3): 63-75. DOI： 10.11959/j.issn.1000-436x.2018042.

摘要

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

关键词

Keywords

references

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

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

钱志鸿 , 王义君 . 物联网技术与应用研究 [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 .

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 .

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 .

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 .

陈琦 , 韩冰 , 秦伟俊 , 等 . 基于 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 .

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 .

罗俊海 , 周应宾 , 邓霄博 . 物联网网关系统设计 [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 .

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 .

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 .

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 .

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 .

石希 , 陈震 , 汪东升 , 等 . 物联网汇聚安全网关关键技术研究 [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 .

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

罗娟 , 顾传力 , 李仁发 . 基于角色的无线传感网络中间件研究 [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 .

杨光 , 耿贵宁 , 都婧 , 等 . 物联网安全威胁与措施 [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 .

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

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

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

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 .

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 .

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 .

浏览量

1663

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于时间自动机的数据流通控制建模及验证

基于程序局部性引导的有界模型检测优化方法

基于模型检测的服务链信息流安全可组合验证方法

可信密码模块的模型检测分析

容忍入侵的应用服务器结构设计与实现