Formal Specifications and Verification of a Secure Communication Protocol Model

This paper presents a secure communication protocol model-EABM, by which network security communication can be realized easily and efficiently. First, the paper gives a thorough analysis of the protocol system, systematic construction and state transition of EABM. Then , it describes the channels and the process of state transition of EABM in terms of ESTELLE. At last, it offers a verification of the accuracy of the EABM model.

Designing and Verifying Communication Protocols Using Model Driven Architecture and Spin Model Checker

The need of communication protocols in today’s environment increases as much as the network explores. Many new kinds of protocols, e.g. for information sharing, security, etc., are being developed day-to-day which often leads to rapid, premature developments. Many protocols have not scaled to satisfy important properties like deadlock and livelock freedom, since MDA focuses on the rapid development rather than on the quality of the developed models. In order to fix the above, we introduce a 2-Phase strategy based on the UML state machine and sequence diagram. The state machine is converted into PROMELA code as a protocol model and its properties are derived from the sequence diagram as Linear Temporal Logic (LTL) through automation. The PROMELA code is interpreted through the SPIN model checker, which helps to simulate the behavior of protocol. Later the automated LTL properties are supplemented to the SPIN for the verification of protocol properties. The results are compared with the developed UML model and SPIN simulated model. Our test results impress the designer to verify the expected results with the system design and to identify the errors which are unnoticed during the design phase.

Analysis of reactive routing protocols for mobile ad hoc networks in Markov models

Mobile ad hoc networks （MANETs） have become a hot issue in the area of wireless networks for their non-infrastructure and mobile features. In this paper, a MANET is modeled so that the length of each link in the network is considered as a birthdeath process and the space is reused for n times in the flooding process, which is named as an n-spatiai reuse birth-death model （n-SRBDM）. We analyze the performance of the network under the dynamic source routing protocol （DSR） which is a famous reactive routing protocol. Some performance parameters of the route discovery are studied such as the probability distribution and the expectation of the flooding distance, the probability that a route is discovered by a query packet with a hop limit, the probability that a request packet finds a τ-time-valid route or a symmetric-valid route, and the average time needed to discover a valid route. For the route maintenance, some parameters are introduced and studied such as the average frequency of route recovery and the average time of a route to be valid. We compare the two models with spatial reuse and without spatial reuse by evaluating these parameters. It is shown that the spatial reuse model is much more effective in routing.

Symbolic Model Checking and Analysis for E-Commerce Protocol

A new approach is proposed for analyzing non-repudiation and fairness of e-commerce protocols. The authentication e-mail protocol CMP1 is modeled as finite state machine and analyzed in two vital aspects- non-repudiation and fairness using SME. As a result, the CMP1 protocol is not fair and we have improved it. This result shows that it is effective to analyze and check the new features of e-commerce protocols using SMV model checker.

A Novel Formal Theory for Security Protocol Analysis of Denial of Service Based on Extended Strand Space Model

Denial of Service (DoS) attack,especially Distributed Denial of Service (DDoS) attack,is one of the greatest threats to Internet.Much research has been done for it by now,however,it is always concentrated in the behaviors of the network and can not deal with the problem exactly.In this paper,we start from the security of the protocol,then we propose a novel theory for security protocol analysis of Denial of Service in order to deal with the DoS attack.We first introduce the conception of weighted graph to extend the strand space model,then we extend the penetrator model and define the goal of anti-DoS attack through the conception of the DoS-stop protocol,finally we propose two kinds of DoS test model and erect the novel formal theory for security protocol analysis of Denial of Service.Our new formal theory is applied in two example protocols.It is proved that the Internet key exchange (IKE) easily suffers from the DoS attacks,and the efficient DoS-resistant secure key exchange protocol (JFK) is resistant against DoS attack for the server,respectively.

APN Model for Specification of the Communication Protocols in Multi-Agent System

This paper deals with the proposal of a new model based on Agent Petri Nets (APN) to specify interactions among agents in Multi Agents System (MAS). Indeed, an agent approach requires a powerful and expressive formalism that allows him to model the behavior of a set of agents that interact. We are modeling some variants of FIPA standard protocols. Our Models are found based on communicating cognitive agents. Each Agent is capable of perceiving their environment partly and building, sending and receiving messages.

Secure planar convex hull protocol for large-scaled point sets in semi-honest model

Efficiency and scalability are still the bottleneck for secure multi-party computation geometry(SMCG).In this work a secure planar convex hull(SPCH) protocol for large-scaled point sets in semi-honest model has been proposed efficiendy to solve the above problems.Firstly,a novel privacy-preserving point-inclusion(PPPI) protocol is designed based on the classic homomorphic encryption and secure cross product protocol,and it is demonstrated that the complexity of PPPI protocol is independent of the vertex size of the input convex hull.And then on the basis of the novel PPPI protocol,an effective SPCH protocol is presented.Analysis shows that this SPCH protocol has a good performance for large-scaled point sets compared with previous solutions.Moreover,analysis finds that the complexity of our SPCH protocol relies on the size of the points on the outermost layer of the input point sets only.

安全协议形式化分析方法研究综述

介绍了安全协议的基本概念和分类,然后对安全协议形式化分析方法进行了详细介绍,包括基于模态逻辑的方法、基于模型检测的方法、基于定理证明的方法和基于可证明安全性理论的方法。其中,基于模型检测的方法是目前应用最广泛的一种方法,因此详细介绍了一些常用的基于模型检测方法的工具。最后,总结了当前安全协议形式化分析方法的研究热点和未来的发展方向。

基于Tamarin的门罗币支付协议分析方法

门罗币作为一款基于区块链技术的高度匿名加密货币协议,旨在为用户提供强大的隐私保护功能。与其他加密货币不同,门罗币通过独特的支付协议对用户的交易隐私加强保护。然而,支付协议中存在的安全漏洞可能导致攻击者对交易信息进行分析或拦截,从而威胁用户的隐私安全。目前,对门罗币支付协议的研究主要集中在对匿名性漏洞的攻击,大部分攻击从外部特征出发,缺少对门罗币机制进行探索,不能充分保障支付过程的安全性和不可追踪性。因此需要进行更系统化的分析,以全面评估门罗币支付协议的安全性和不可追踪性。文章从模型规则、属性定义等角度对门罗币支付协议进行细粒度建模,并运用已有的Tamarin工具对相关属性进行验证,研究结果揭示了多个门罗币支付协议漏洞,并给出优化建议。

区块链增强的低空智联网可信协作架构及集群构建策略

低空生态的繁荣不断推动智能网络服务由平面向低空三维立体方向转变,低空业务呈现出规模化、协同化和智能化等演进态势,对低空智联网跨域设备协作能力、任务处理效率、数据安全性及操作可信性等提出了较严苛要求。集群式多设备联合计算协作可提升低空智联网中复杂化大规模任务的处理效率,然而现有模式仍存在跨域设备协作困难、安全可信性缺乏保障以及资源调度灵活性不足等问题。区块链具有数据及操作不可篡改、公开透明和集体维护等特性,尤为适合在多方参与的低空智联环境中建立高效协作信任。本文提出区块链增强的低空智联网可信协作架构,为低空多源异构智联设备提供链上跨域协作计算与状态同步渠道,并设计深度融合集群任务处理流程的多级共识协议,保障低空智联网协作集群式计算服务的安全性与可信性。针对低空智联网中协作集群链上同步状态的时效性开展分析,并据此提出一种基于排队模型的低空智联协作节点链上状态修正算法与高效集群构建策略,保障链上协作任务处理效率。仿真结果表明所提架构及方案可有效提升低空智联网中协作任务处理效率和资源利用率等性能。

基于通用服务协议的主子站免对点数据传输方案研究

变电站接入调度主站时,通过人工对点的方式确保数据的正确性。针于集控站需要采集变电站大量数据的现场需求,基于通用服务协议的数据集服务及61850模型,提出了数据集数据编号规则和主子站数据传输数据映射方案,实现了变电站免对点快速接入集控站,并能保证数据的正确性。

一种比特币支付协议的形式化建模验证方法

作为主流的数字加密货币,比特币的安全性受到广泛关注,并且围绕其展开大量的研究工作.然而目前针对比特币支付过程的分析还比较欠缺,缺乏相关的安全标准和精细的建模分析,难以确保相关协议的安全.针对这一问题,基于比特币社区规范与比特币的数字货币功能属性,为比特币支付协议建立了形式化的符号模型与对应的安全属性,并使用自动验证工具Tamarin对相关模型及属性进行了形式化验证,完成了对比特币支付协议的验证工作,并且发现一种未被讨论过的比特币支付协议中的安全威胁,对该问题可能产生的影响进行了分析。

基于SM2数字签名的区块链匿名密钥交换协议

区块链技术因其去中心化、匿名性、不可篡改、不可伪造等优点,已经成为我国的一项前沿技术,在各领域得到广泛的应用。虽然用户可利用区块链发布匿名交易,有效隐藏交易双方的身份信息,但双方交易完成后传输交易相关数据可能破坏匿名性。这是因为在数据传输过程中,为了保证双方通信安全,往往使用认证密钥交换协议认证双方身份,计算会话密钥建立安全信道。由于传统的认证密钥交换协议涉及双方的长期公私钥对信息,所以将泄露交易双方的身份信息。虽然区块链匿名密钥交换可基于交易双方的历史链上交易完成密钥交换,有效保障交易双方的匿名性,但现有区块链匿名密钥交换协议主要基于国外密码算法设计,难以适用于国产区块链平台,不符合我国密码核心技术自主可控的要求。为丰富国产商用密码算法在区块链匿名密钥交换方面的研究,满足区块链交易后双方匿名安全通信的需求,本文以SM2数字签名算法和区块链为基础,构造非交互式和交互式两种区块链匿名密钥交换协议。并在CK安全模型中证明非交互式的协议满足会话密钥安全,交互式的协议满足有前向安全性的会话密钥安全。最后通过理论分析和编程实现结果表明,本文协议在没有比现有协议消耗更多的计算开销与通信代价的前提下,可适用于国产化区块链平台。

基于系统交互模型的二元应对方案对口腔癌患者术后生存质量干预的应用研究

目的:探索基于系统交互模型的二元应对方案对口腔癌患者术后生存质量的干预效果。方法:选择某三甲医院口腔颌面外科2021年6月至2022年6月收治的99例口腔癌患者,使用随机数字表法分为对照组50例和观察组49例。对照组给予口腔癌常规护理,观察组在常规护理基础上实施基于系统交互模型的二元应对方案。比较分析2组口腔癌患者术前、术后第3周和术后第9周的UW-QOL生存质量量表、二元应对量表的得分。结果:2组患者术后第3周、第9周UW-QOL得分均低于入院时,且对照组UW-QOL得分低于观察组(P<0.05);在术后第3周,观察组患者与伴侣共同应对维度的得分优于对照组(P<0.05);在术后第9周,观察组在二元应对总分、消极应对、压力沟通、共同应对、支持应对维度优于对照组(P<0.05)。重复测量方差分析结果显示时间和组别对二元应对量表总分存在交互作用(P<0.05),时间和组别对二元应对量表总分主效应显著(P<0.05)。结论:口腔癌患者生存质量状况欠佳,基于系统交互模型的二元应对方案可提高患者的生存质量,提高患者与伴侣的亲密关系,有利于口腔癌患者疾病康复。

基于NTRU密钥协商协议设计

NTRU是最早将密码系统困难性规约到格上困难问题的公钥密码体制.NTRU的特征简洁,密钥生成不复杂,运算速度快并且需要的存储空间小,所以目前基于格上困难问题建立密码体制的算法中,NTRU更加简便高效.然而基于NTRU的密钥协商协议相关研究较少,现存的基于NTRU的密钥协商协议消息传递过程中密钥的保护不充分,易为敌手攻击留下后门,且协议的安全性论证不充分不完备.鉴于此,提出了2个基于NTRU格上的密钥协商协议,增加临时秘密信息,使方案具有强前向安全性,并且提出了详细的安全证明,在不泄露响应方密钥和要伪造的会话密钥的情况下,该证明是基于格上最短向量计算困难性SVP假设下会话密钥的不可伪造性.该安全证明在eCK模型下可证明安全的.相较于DH,ECDH等传统的密钥协商方案,NTRU方案是基于多项式环上的,运算效率更高,其安全性可以归约到求解格上的困难问题,可以抵御量子攻击.

智能电网环境下电力系统通信协议的性能分析

文章旨在分析智能电网环境下电力系统通信协议的性能,以评估电力系统通信协议在实际应用中的可靠性和效率。文章阐述智能电网的通信需求和电力系统通信协议的分类与特点,提出基于模拟仿真和实际测试的性能分析方法,并选择了适合的性能评估指标。通过建立仿真模型和搭建测试环境,分析多种电力系统通信协议性能。结果表明,在不同的环境下,各种通信协议的性能表现存在差异。根据分析结果,提出了优化建议和改进方向,以提升智能电网系统的通信效率和稳定性,为智能电网的可靠运行提供理论和实践指导。

引入包分析的E-Model语音质量评价模型改进

为了能够更加准确地评价语音包丢失对基于IP的语音传输(voice over internet protocol,Vo IP)的语音质量的损伤,对ITU-T G.107建议书提出的语音质量预测模型E-Model中计算丢包与编码造成的损伤Ie-eff的方法作出改进,在综合考虑语音包的内部特性和存在突发连续丢包情况后,提出利用在固定语音长度下,语音实际损失时间Tloss来衡量语音包丢失造成的语音损伤。仿真结果表明,相比原有模型,改进后的模型得到的语音质量评分同主观语音质量评估方法(perceptual evaluation of speech quality,PESQ)评分相比,皮尔森相关系数平均提高了0.045 8,均方根误差平均降低了0.053 4,改进后的E-Model模型在评价语音质量时与PESQ更具有一致性,可以更为准确地预测Vo IP通信的语音质量。

智能变电站中的通信网络技术分析

阐述智能变电站通信网络的可靠性问题及原因,提出一种并行冗余协议与高可用性无缝环网协议相结合的系统模型,同时借助可靠性框图予以可靠性评估,并分析智能变电站的高级应用。

基于模型驱动双向主动测量协议的IP网络遥测系统研究与实现

IP层的OAM技术中,双向主动测量协议(TWAMP)通过主动向网络注入测量报文,并根据对测量报文进行采集分析来实现任意2个具备IP可达性网络节点之间的网络层性能监测。文章首先分析了TWAMP测量方案在实际运营部署时存在的主要问题和挑战,然后针对网络的运维管理日益智能化的网络发展趋势下,需要对网络运行状况进行连续实时主动监测的新需求进行了相关分析。基于此,文章提出了一种面向互联网遥测架构的硬探针TWAMP网络监控系统,以此实现IP传送网的性能监测改进,为实现更实时可靠的智能运营提供有力支撑。