基于Tamarin的5G AKA协议形式化分析及其改进方法

对于5G移动通信网络, 3GPP组织标准化了5G AKA等协议,用于身份认证和密钥协商.本文使用安全协议验证工具Tamarin对5G AKA协议进行了形式化分析.首先基于3GPP TS 33.501v17.0.0版本,完成了对5G AKA协议及期望其满足的安全性质的形式化建模.安全性质考虑了保密性质和Lowe鉴权性质,保密性质包括安全锚点密钥KSEAF和长期共享密钥K的保密性,鉴权性质包括协议参与实体之间在参数SUPI、SNID、KSEAF上的非单射一致性,以及在KSEAF上的单射一致性.然后本文在Tamarin中验证了5G AKA协议是否满足相关安全性质,发现保密性质全部得到满足,鉴权性质一共验证了36种情况,其中有23种情况没有得到满足.最后针对协议不满足的鉴权性质,本文采用了三种修改方法来对协议模型进行改进,并对改进前后的验证结果进行了分析总结.     

基于安全协议代码的形式化辅助建模研究

随着安全协议形式化分析技术的不断发展,利用工具自动验证虽已得到实现,但建模环节仍需依赖专业人员手工建模,难度大且成本高,限制了此技术的进一步推广。为了提高建模的自动化程度,提出了依据安全协议代码进行形式化模型辅助生成的方案。首先,使用污点分析获取协议的通信流程,并且记录密码学原语操作;然后,根据通信流程之间的序列关系构建协议通信状态机;最终,根据目前主流的安全协议形式化分析工具Tamarin的模型语法生成形式化模型。实验结果表明,此方案可以生成形式化模型中的关键部分,提高了形式化建模的自动化程度,为形式化分析技术的推广作出贡献。     

基于MQTT协议物联网文件传输的实现

MQTT协议作为一种即时通信协议,在未来物联网技术的建设与发展中,将会成为其最为重要的组成部分,基于搭建完成的平台连接外部和联网的设备,充当通信桥梁的作用。本文从MQTT协议角度出发,从物模型与主题模型设计、设备状态管理设计、消息路由模块设计、系统安全模块设计、系统集群模块设计等五个角度,系统分析了基于MQTT协议的物联网文件传输系统,探究物联网文件传输的实现路径。     

基于MQTT协议的综合消息推送

推送技术在移动开发中被广泛使用,然而目前推送体系过于依赖网络,在网络中断或故障的情况下,会给消息推送带来极大的困扰。对目前常用的推送方式进行分析和研究,通过补充和完善MQTT推送协议,综合网络、邮件、短信等多种通信方式,优化服务器传输机制,并加入消息过滤层过滤垃圾信息,组建更为智能、高效、安全的推送系统。     

基于NS-3的MQTT协议仿真研究

如今,制造业数字化转型中采用消息队列遥测传输（MQTT）协议已成为趋势,而工业场景中往往存在大量的传感器等设备。考虑到实际部署的复杂性,在工业场景中实际部署MQTT前,进行必要的模拟以获取网络性能等数据是不可或缺的,这将更有利于工业场景中的链路设计和网络规划。而NS-3作为当前最流行的网络仿真器之一,提供了丰富的网络模型,非常适合像工业场景这种大型复杂网络的仿真,但目前利用其模拟部署MQTT仍是一项困难的工作。针对该问题,提出了一个适用于NS-3的扩展仿真框架ns3-mqtt,该框架由多个MQTT组件构成,能够以软件包的形式集成到NS-3中,并且提供简洁易用的仿真接口,使得扩展后的NS-3可较容易地对MQTT进行模拟部署并获取相关数据,以此研究不同工业场景下MQTT协议的性能,指导MQTT的实际部署。仿真测试结果证明了提出的ns3-mqtt框架的正确性和有效性。     

Android平台基于MQTT协议的推送机制

Android平台的迅速崛起对消息推送技术提出了更严峻的挑战.传统的推送通知方式主要有Polling,SMSPush,IP Push三种,但对Android平台上的应用来说,这些推送方式都有各自的短板.针对该情况,首先对Android平台上几种推送机制进行了分析,之后着重对基于MQTT协议的推送机制进行研究,最后借助IBM提供的开源工具Mosquitto通过编码加以实现.经实验测试,证明基于MQTT协议的推送机制效率高,功耗低,可以稳定地用于Android平台上的应用.     

基于MQTT协议的智慧农场智能化管理系统

智慧农场的运用成为当代农业发展的必然趋势,利用MQTT协议的消息发布/订阅机制,通过远程移动端设备监控智慧农场各项数据并对智慧农场实施智能化管理十分有必要.在智慧农场中,MQTT协议网络接口可通过开发板中的代码移植和外接设备实现,以此达到智慧农场中数据与外部的交流和命令的接收,并使这些消息的交互相比其他方式更加简单快捷,实现对农场的智能控制并及时反馈的目的.     

基于MQTT协议的物联网消息推送系统构建

在物联网技术不断发展的背景下,消息推送系统愈发先进,通过有针对性为客户提供感兴趣的消息,可以提升软件的满意度,为客户提供更加便捷的服务。消息推送系统可以把各类消息及时推送给客户端,在客户端和服务器之间构建一个长连接,并一直保持畅通状态,可以为客户及时推送感兴趣的消息。目前,物联网消息推送系统的应用范围比较广泛,发展前景广阔,已经初步形成移动互联网软件开发的基础系统,也是全球范围内的热点话题。     

基于MQTT协议的移动网络对讲系统架构设计

本文介绍了一种基于IBM公司MQTT协议移动网络对讲系统的架构设计,完成了系统组成,系统结构和各子系统通信机制的分析,重点阐述了如何应用MQTT协议实现一对多语音对讲的系统架构,本文对于类似即时通信软件系统开发有一定的参考价值。     

基于MQTT协议的海洋观测数据推送系统

为实现海洋观测数据的及时推送,设计了一种数据推送系统,目的是将各个观测船、浮标和水下观测网等采集到的海洋观测数据推送到手机客户端,并实现异常数据的报警。提出了一种基于MQTT协议的数据推送方案,在加密与验证方面对MQTT协议进行改进。此外,设计了安全认证机制与消息管理模块,保证了消息在传输中不被篡改或者丢失。测试结果证明,该方案安全性较高,服务权限设计合理,费用方面也具有较大的优势。     

Cryptographic protocol security analysis based on bounded constructing algorithm

1 Introduction 1.1 Background Cryptographic protocols have been used to provide security services for many applications on the open communication environment. More and more cryptographic protocols will be designed to solve the increasing security requirem…     

Needham-Schroeder 协议的认证测试方法形式化分析

在安全协议的形式化分析方法中,串空间模型和基于串空间模型的认证测试方法是比较常用的验证方法。针对Needham- Schroeder协议存在中间人攻击的缺陷,提出对协议的改进并采用认证测试方法,验证了改进的协议可以满足协议的安全目标。     

智能电网中基于MQTT协议的ABAC访问控制方案

在智能电网环境中,电力运营商和消费者通过智能电表进行大量高精度的用电数据的实时监测,用户机密数据持续暴露于未经授权的访问,在这种传统通信模式下,智能电表对家庭用户能源消耗的细粒度测量造成了严重的隐私安全问题,而现有的静态访问控制方法并不满足智能电网环境基于上下文的动态访问特性。针对此问题,提出一种基于物联网通信协议（MQTT协议）的访问控制方案,通过在MQTT协议中对树型结构的主题列表设计基于ABAC访问控制模型的动态上下文授权策略,并在WSO2系统使用XACML策略语言实现了提出的访问控制方案。性能评估结果表明,该方案能在较低的通信开销内支持动态的访问控制,以解决智能电网中用户的用电信息未经授权而泄露的隐私安全问题。     

新的复合型电子商务安全协议

针对典型电子商务安全协议存在的安全目标单一,不能满足日益增加的安全需求等问题,提出了一种能够满足多种安全属性的复合型电子商务安全协议,该协议包含认证子协议和支付子协议两部分。认证子协议基于令牌概念实现了高效认证及协商会话密钥。改进匿名电子现金支付协议,提出了支付子协议,引入电子证书证明交易主体的身份,确保协议非否认性的实现;借助可信方传递付款收据,避免交易主体不诚实所导致的公平性缺失;引入FTP传输方式传送电子货币和付款收据,确保实现可追究性与公平性,进一步增强协议的鲁棒性。     

一种新的形式化模型对安全认证协议的分析*

针对形式化建模方法在进行网络协议分析时遇到建立模型过程复杂、状态空间庞大等问题,提出在Petri网的基础上,引入融合库所建立一种新的形式化模型。利用该方法对Otway-Rees协议建立模型,并从可达性和仿真两方面进行分析。实验结果表明,该方法适合应用在协议分析中,不仅使协议建立模型更加简便,而且在一定程度上缩小了其状态空间。     

对改进的无线认证协议SSM的分析

针对刘霞提出的改进的Server-specific MAKEP协议,首次利用一种新兴的形式化分析工具—串空间模型对其进行分析。先对协议的机密性进行分析,并运用“理想”和“诚实”两个概念简化分析协议的步骤,证明了rs,rc是保密的,然后对协议的认证性进行分析,分析包括响应者认证和发起者认证。最终结果表明改进的SSM协议能够达到协议的安全目标。     

改进的OpenID Connect协议及其安全性分析

OpenID Connect协议是最新的单点登录协议之一,已经广泛应用于用户身份认证领域,其安全性受到了人们的重点关注。为增强OpenID Connect协议的安全性,首先引入数字签名及非对称加密技术,对其进行改进,重点关注改进后协议的秘密性和认证性;其次基于符号模型,应用应用PI演算对改进的OpenID Connect协议进行形式化建模;然后为验证改进后协议的认证性和秘密性,分别使用非单射性和query对认证性和秘密性进行建模;最后把改进的OpenID Connect协议的应用PI演算模型转换为安全协议分析工具ProVerif的输入,应用ProVerif对其进行形式化分析。实验结果表明,改进后的OpenID Connect协议具有认证性和秘密性。