首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到20条相似文献,搜索用时 93 毫秒
1.
MQTT是物联网中被广泛应用的消息传输协议,其安全性问题备受关注。当前MQTT协议安全性分析主要面向协议实现平台,缺少面向协议标准的安全性测试,导致协议标准本身存在的安全缺陷难以发现。针对该问题,采用协议形式化分析技术,提出了一种基于Tamarin的MQTT协议安全性分析方法。该方法首先面向MQTT协议3.1.1标准,构建了协议状态机,并依据Tamarin语法规则,完成了形式化描述;然后针对保密属性和认证属性,给出了MQTT协议需要满足的安全属性引理描述;最后,基于Dolev-Yao威胁模型在Tamarin中完成了对47种协议安全属性的验证。结果显示有9种保密属性违反和29种认证属性违反,对结果进行攻击测试,验证了该方法对MQTT协议安全性分析的有效性,并提出了一种基于身份重认证的优化改进方案。  相似文献   

2.
针对程序的运行时动态攻击给远程证明带来的安全威胁,设计一种动态远程证明协议DRAP,对内存中处于运行状态的程序实施实时的动态度量,并向远程验证方证明平台实时状态。针对DRAP协议所用的TPM功能对LS2逻辑进行扩展,引入重置规则、时刻规则等新的推理规则,利用扩展的LS2逻辑对DRAP协议进行分析,分析表明DRAP中可重置配置寄存器中的扩展序列能够反映平台中程序的实时运行状态,并且在TPM可信和证明代理可信的前提下,远程验证者能够有效验证平台的实时可信状态。  相似文献   

3.
胡声洲  余敏  彭文灵 《计算机工程》2007,33(21):147-148
关联性是安全协议的基本特征,该文提出了协议相关性的分析方法,从主体认证关联、消息间关联、消息内部关联 3个角度分析了协议的相关特征,阐述了相关性的概念和关联规则构建方法,构建了基于关联性的协议描述模型,为安全协议的形式化分析提供了新的思路。  相似文献   

4.
SPVT:一个有效的安全协议验证工具   总被引:12,自引:0,他引:12  
描述了基于Objective Caml开发的一个安全协议验证工具SPVT(security protocol verifying tool).在SPVT中,以扩展附加项的类(演算作为安全协议描述语言,以扩展附加项的Horn逻辑规则描述协议攻击者的Dolev-Yao模型,通过一组抽象规则将安全协议的类(演算模型转换为逻辑程序模型,基于安全协议逻辑程序的不动点计算验证安全性质,从安全协议逻辑程序的不动点计算和安全性质的验证过程中构造不满足安全性质的安全协议反例.以简化的Needham-Schroeder公钥认证协议为例,描述了使用SPVT自动验证安全协议的过程,表明了SPVT用于安全协议验证的有效性.  相似文献   

5.
形式化方法是验证加密协议的重要手段,提出了一种新的验证方法,该方法基于Debbabi的推理规则,将参与者ID|参与者密钥等数据结构从协议中抽象出来,建立起抽象的逻辑推理结构。以Woo-Lam协议为例,通过逆向递推的方式得到了协议的所有攻击路径,并以图的形式表示其关系,详尽分析了协议的漏洞,最后,提出了如何使协议更为安全的建议。  相似文献   

6.
基于串空间的可信计算协议分析   总被引:1,自引:0,他引:1  
可信计算技术能为终端、网络以及云计算平台等环境提供安全支撑,其本身的安全机制或者协议应该得到严格的形式化证明.该文基于串空间模型对其远程证明协议进行了分析.首先,扩展了串空间的消息代数和攻击者串,使其能表达可信计算相关的密码学操作,并对衍生的定理进行了证明;并且提出了4个新的认证测试准则,能对协议中的加密、签名、身份生成和哈希等组件进行推理.其次,基于扩展的串空间模型对远程证明协议的安全属性(隐私性、机密性和认证性)进行了抽象和分析.最后,给出了对发现攻击的消息流程,并基于ARM开发板对其中的布谷鸟攻击进行了实现,验证了串空间的分析结果.  相似文献   

7.
安全协议模型是安全协议分析与验证的基础,现有的建模方法中存在着一些缺点,如:建模复杂、重用性差等.为此提出了一种类型化的π演算:πt演算,并给出了相应类型推理规则和求值规则,πt演算的安全性也得到了证明.πt演算可以对安全协议、协议攻击者进行形式化建模.基于πt演算的安全协议模型及其建模过程使用NRL协议为例做出了说明.同时给出了攻击者模型,并证明了基于πt演算的安全协议攻击者模型与D-Y攻击者模型在行动能力上是一致的.这保证了基于πt演算的安全协议模型的验证结果的正确性.基于πt演算的建模方法能在协议数据语义、协议参与者知识方面实现细致的描述.与同类方法相比,该方法可提供多种分析支持,具有更好的易用性、重用性.分析表明,该方法可以在建模中发现一定的安全协议漏洞.  相似文献   

8.
串空间模型是分析安全协议的一种实用、直观和严格的形式化方法。概述基于该模型结合使用定理证明和模型检测技术开发的安全协议验证工具AVSP的体系结构,提出一些剪枝规则对状态搜索空间进行剪枝。通过Needham-Schroeder安全协议的弱一致性认证属性验证过程来表明这些状态搜索空间剪枝规则可有效缩小状态搜索空间,防止状态空间爆炸。  相似文献   

9.
赵华伟  秦静 《计算机工程》2007,33(20):30-33
提出了一种新的基于信念的模态逻辑——MBL逻辑,来分析由单向函数构造的对称钥认证交换协议的安全性。该逻辑有严格的证明体系,可证明推理规则在其语义模型下的正确性,说明该逻辑具有合理性。其推理规则不仅能对单向函数保护的消息进行有关认证性的推理,克服了以往逻辑系统使用不当的安全服务来分析协议认证性的缺陷,而且可分析消息的保密性,避免了其他逻辑分析协议时对可信中心的过分依赖,可发现敌手通过欺骗可信中心而造成的攻击。  相似文献   

10.
安全协议的形式化验证与分析已成为国际研究的热点.本文应用BAN逻辑研究Needham-Schroeder对称密钥认证协议,指出该协议存在的安全缺陷,利用消息新鲜性对其进行相应改进,并在BAN逻辑下形式化证明改进的协议可以满足安全目标.  相似文献   

11.
用于专家系统规则库的冗余校验方法研究   总被引:1,自引:0,他引:1  
产生式规则是目前应用较多的一种知识表示方法。在用于确定发酵过程生物量软测量混合模型结构的专家系统中,当向产生式规则知识库添加新的规则时,冗余的存在会影响推理的效率以及推理的准确性。提出了一种用于该专家系统规则库的冗余校验方法,给出了冗余规则的判别、冗余规则的处理以及冗余校验的实现方法。实验结果表明,该冗余校验方法可以根据输入条件和已有规则,判断出新添加的规则是否冗余,并在消除冗余对推理效率影响的同时,降低模型复杂度,有利于优化混合模型的结构。  相似文献   

12.
模糊推理中,输入和推理规则发生摄动时,内部连接算子的选择是影响推理输出的主要因素。给出了模糊Lipschitz聚合算子的定义,论证了满足Lipschitz条件的三角模算子和蕴涵算子,研究了一类稳定的Lipschitz聚合算子对模糊推理的鲁棒性影响,指出了当系统发生输入摄动和规则摄动时,内部连接算子为1-Lipschitz算子,能有效地抑制模糊推理的输出摄动,特别是当内部连接算子既是1-k∞-Lipschitz又是quasi-copulas时,模糊推理输出更稳定安全可行,模糊推理的鲁棒性得到更好调控;另外,从实验结果看,规则摄动对推理输出影响较大。实验部分既是对文中所提理论的很好验证,同时也是该理论在图像处理和人脸联想方面的具体应用。  相似文献   

13.
Model checking is a successful approach for verifying hardware and software systems. Despite its success, the technique suffers from the state explosion problem which arises due to the large state space of real-life systems. One solution to the state explosion problem is compositional verification, that aims to decompose the verification of a large system into the more manageable verification of its components. To account for dependencies between components, assume-guarantee reasoning defines rules that break-up the global verification of a system into local verification of individual components, using assumptions about the rest of the system. In recent years, compositional techniques have gained significant successes following a breakthrough in the ability to automate assume-guarantee reasoning. However, automation has been restricted to simple acyclic assume-guarantee rules. In this work, we focus on automating circular assume-guarantee reasoning in which the verification of individual components mutually depends on each other. We use a sound and complete circular assume-guarantee rule and we describe how to automatically build the assumptions needed for using the rule. Our algorithm accumulates joint constraints on the assumptions based on (spurious) counterexamples obtained from checking the premises of the rule, and uses a SAT solver to synthesize minimal assumptions that satisfy these constraints. To the best of our knowledge, our work is the first to fully automate circular assume-guarantee reasoning. We implemented our approach and compared it with established non-circular compositional methods that use learning or SAT-based techniques. The experiments show that the assumptions generated for the circular rule are generally smaller, and on the larger examples, we obtain a significant speedup.  相似文献   

14.
在应急响应系统(ERS)中,规则及规则推理用于确定应急事件的响应级别。当系统的规则库增加规则时,会出现冗余的规则,冗余规则的存在导致响应级别的判断不准确,影响推理的效率和准确性。针对该问题,提出一种规则的冗余检测方法,使规则库中的规则始终保持无冗余状态;同时,给出了冗余规则的处理方法。最后给出该算法的一个应用实例,结果表明该算法能快速检测出冗余规则,有效降低规则数目。  相似文献   

15.
A fuzzy reasoning and verification Petri nets (FRVPNs) model is established for an error detection and diagnosis mechanism applied to a complex fault-tolerant PC-controlled system. The inference accuracy can be improved through the hierarchical design of a two-level fuzzy rule decision tree and a Petri nets technique to transform the fuzzy rule into the FRVPNs model. Several simulation examples of the assumed failure events were carried out by using the FRVPNs and the Mamdani fuzzy method with MATLAB tools. The reasoning performance of the developed FRVPNs was verified by comparing the inference outcome to that of the Mamdani method. Both methods result in the same conclusions. Thus, the present study demonstrates that the proposed FRVPNs model is able to achieve the purpose of reasoning, and furthermore, determining of the failure event of the monitored application program.  相似文献   

16.
在智能决策系统(IDSS)获取知识的推理体系中,案例推理和规则推理有着各自的优点,而混合两者的集成推理可以克服两者的缺点,提高系统的效率和综合推理能力。但是集成推理系统缺乏通用性,延长了开发周期,且不利于规则库和案例库的重用。一种可扩充的集成推理框架为了解决上面的问题而被提出,该框架利用智能决策支持语言Knonit的组件性,对不同的集成方式可方便地扩充相应的集成推理方案,从而快速地搭建IDSS应用;同时规则和案例是作为Knonit广义知识元存在,可以在集成推理框架中复用,另一方面,Knonit的动态特性和可扩充性也对案例库和知识库动态的调整和扩充提供了支持。  相似文献   

17.
云模型实现了定性概念与其定量表示之间的不确定转换,在云模型基础上构建的规则发生器能有效描述用自然语言表示的定性规则.在单条件单规则发生器基础上,进一步提出双条件单规则发生器的实现算法,给出了云推理系统的体系结构.将基于云模型的不确定性推理方法用于设计电机转速控制系统,并且与模糊推理方法进行了比较,验证了云推理方法的有效性和实用性.  相似文献   

18.
陈翔  刘军丽 《计算机工程》2007,33(13):65-67
针对工作流管理系统的实现复杂性及模型可靠性的验证问题,提出了一种结合工作流网和ECA规则来创建工作流管理系统的方法。这种基于ECA规则的工作流描述和执行机制较好地实现了工作流网模型的语义描述和控制的统一。通过建立基于ECA规则的工作流描述表,将ECA 规则引入到工作流路由机制中,灵活地控制了工作流的流程。通过事件触发和消息处理机制,工作流描述表处理可以被实际系统加以执行和控制。  相似文献   

19.
Many real-life critical systems are described with large models and exhibit both probabilistic and non-deterministic behaviour. Verification of such systems requires techniques to avoid the state space explosion problem. Symbolic model checking and compositional verification such as assume-guarantee reasoning are two promising techniques to overcome this barrier. In this paper, we propose a probabilistic symbolic compositional verification approach (PSCV) to verify probabilistic systems where each component is a Markov decision process (MDP). PSCV starts by encoding implicitly the system components using compact data structures. To establish the symbolic compositional verification process, we propose a sound and complete symbolic assume-guarantee reasoning rule. To attain completeness of the symbolic assume-guarantee reasoning rule, we propose to model assumptions using interval MDP. In addition, we give a symbolic MTBDD-learning algorithm to generate automatically the symbolic assumptions. Moreover, we propose to use causality to generate small counterexamples in order to refine the conjecture assumptions. Experimental results suggest promising outlooks for our probabilistic symbolic compositional approach.  相似文献   

20.
Fuzzy rule base systems verification using high-level Petri nets   总被引:3,自引:0,他引:3  
In this paper, we propose a Petri nets formalism for the verification of rule-based systems. Typical structural errors in a rule-based system are redundancy, inconsistency, incompleteness, and circularity. Since our verification is based on Petri nets and their incidence matrix, we need to transform rules into a Petri nets first, then derive an incidence matrix from the net. In order to let fuzzy rule-based systems detect above the structural errors, we are presenting a Petri-nets-based mechanism. This mechanism consists of three phases: rule normalization, rules transformation, and rule verification. Rules will be first normalized into Horn clauses, then transform the normalized rules into a high-level Petri net, and finally we verify these normalized rules. In addition, we are presenting our approach to simulate the truth conditions which still hold after a transition firing and negation in Petri nets for rule base modeling. In this paper, we refer to fuzzy rules as the rules with certainty factors, the degree of truth is computed in an algebraic form based on state equation which can be implemented in matrix computation in Petri nets. Therefore, the fuzzy reasoning problems can be transformed as the liner equation problems that can be solved in parallel. We have implemented a Petri nets tool to realize the mechanism presented fuzzy rules in this paper.  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号