GVim的TLA+语言插件设计与实现

GVim是一款著名的编辑器,它允许用户为方便使用而自定义插件.TLA+语言是由Les-lie Lamport设计的基于行为时序逻辑的一门系统描述语言.本文描述了为GVim编写TLA+语言插件的详细步骤.这些插件提供了关键字高亮,插入模板,缩进,以及在图形界面下调用TLA模型检测的相关命令等功能,通过使用这些插件,在用TLA+语言描述系统时可明显提高编辑效率.     

网络通信协议形式化描述与验证技术的研究

首先概述当今常用的协议模型技术；然后重点剖析基于ＦＳＭ、Ｐｅｔｒｉ网和ＴＬ模型的协议形式化描述与验证技术的研究现状；最后介绍了一种最新协议描述技术－Ｚ协议技术。此外，本文还对这四种协议形式化技术各自的特点发表了作者的观点。     

协议描述和验证的基本方法

简要说明了协议描述和验证的基本概念，示例地介绍构造实现描述和协议验证的基本思想，最后以Ｐｅｔｒｉ网形式给出了ＡＢ协议一例。     

基于TLA的Kerberos协议符号化与检测

Leslie Lamport提出的一种新逻辑:行为时序逻辑TLA(Temporal Logic of Actions),它能在一种语言中同时表达模型程序与逻辑规则。AVISPA是基于行为时序逻辑的用HLPSL语言编程的协议安全检测工具。文中提出对Kerberos协议角色化,然后用AVISPA工具对HLPSL编码进行检测,结果表明用基于TLA的检测工具是宜于使用且有效的。     

基于π-演算的安全协议描述与验证

π-演算是以进程间移动通信为研究重点的并发理论，本文扼要叙述π-演算的基本概念，论述了如何用π-演算描述和验证安全协议，具体以Station-to-Station协议的一个不完全版本为例进行了分析，发现并在π-演算的工具MWB中证实了协议中存在的一个攻击，分析受到攻击的原因并给出了协议的改进版本．     

基于模型检测的SSL协议形式化验证

针对传统的测试方法无法对网络安全协议的逻辑本身进行验证等问题,提出了一套基于形式化分析和SPIN模型检测的验证方法.该方法首先以BAN逻辑对目标协议进行形式化分析,然后推断目标协议存在的问题缺陷,并通过Promela语言对其构建SPIN模型,最后通过SPIN软件验证推断的正确性.并以SSL协议作为具体实例予以论证,结果表明所提方法具可行性.     

一种身份认证协议的形式化描述与验证

身份认证作为实现网络安全的第一步，是网上商务信息安全交换的关键。而认证协议一旦存在漏洞。必然会导致秘密信息的泄漏，这就需要采用一种形式化的方法去描述和验证认证协议。本文采用着色Petri网描述身份认证协议，同时提出了一种用1-可达性分析方法和向回分析方法相结合的策略，验证了该身份认证协议的安全性。     

基于SPIN的SAS协议和NS公钥协议分析

给出SPIN模型检测协议的验证步骤,使用其分析验证SAS协议的安全属性和数据流行为属性,以及NS公钥协议的机密性和认证性.结果成功发现SAS协议数据流的缺陷和NS公钥协议的攻击路径.     

TLA改性沥青配合比设计及路用研究

特立尼达湖(TLA)改性沥青是一种混合了TLA沥青的改性沥青制成品,拥有多项出色的路用性能,沥青混合料均匀,改善沥青和沥青混合料的温度敏感性,增强在高温环境下的稳定性和抗变形能力,以及抗水损害能力等。在高速公路施工中采用并取得了良好效果,介绍了TLA改性沥青混合料配合比设计,施工工艺及质量控制。     

高速公路TLA改性沥青路面的施工关键技术控制探讨

特立尼达湖沥青（TLA）作为一种沥青改性剂掺加到石油沥青中，具有良好的高温稳定性和低温抗裂性。目前日益广泛应用于高速公路的建设。本文从摊铺与碾压两个环节，针对高速公路TLA改性沥青路面的施工关键技术进行分析，以期为高速公路建设水平的提高提供参考和借鉴。     

基于SMV的安全协议建模及类型缺陷攻击发现

在分析安全协议模型的基础上,探讨了基于SMV工具的安全协议的建模及发现类型缺陷攻击的方法,对Otway-Rees协议的建模和分析表明,该方法对于发现类型缺陷攻击是有效的.     

油蚀对TLA改性沥青混合料水稳定性的影响

通过制定室内油蚀试验方案,采用浸水马歇尔和冻融劈裂试验,分析了油蚀对TLA改性沥青混合料AC-13C的水稳定性的影响规律.研究结果表明,油蚀对水稳定性的影响与TLA掺量和油蚀时间密切相关,其中,油蚀浸水残留稳定度和油蚀冻融残留强度比随着TLA掺量增加呈现先增后减的单峰变化关系,且峰值出现在TLA掺量为30%左右; 同时,初期60 min内油蚀浸水残留稳定度的降幅占总降幅的80%以上.因此,适宜的TLA掺量与及时的除油污处理可有效提高TLA改性沥青路面的抗油蚀水损坏能力.     

基于行为时序逻辑TLA的安全协议形式化分析与检测

随着近年来网络协议的不安全性,对安全协议进行形式化分析与检测则显的非常重要。而基于行为时序逻辑TLA的模型检测是形式化分析检测方法中重要的一种。本文主要采用基于TLA的HLPSL语言形式化分析与检测H.530协议。     

概率模型检验的CBTC系统通信协议的形式化验证

通信协议是CBTC系统重要的组成部分,它的正确性、稳定性和安全性对整个CBTC系统有重要影响.鉴于通信协议中某些参数具有随机特征,本文采用概率模型检验对其进行形式化验证.分析了概率模型检验的语义及语法,建立了通信协议的概率模型,用概率模型检验工具PRISM验证了典型的概率规范.结果证明,当信道正常概率为99%,系统无延时概率为99%时,通信协议失效率小于1.5×1010.说明了用概率模型检验验证具有随机特征参数的通信协议,方法简单快捷,结论清晰明了.     

一种基于协议组合的协议动态实现模型

在协议组合理论的基础上提出了一种可以动态扩展协议句法的基本协议实现模型,依据现有协议特征中的句法结构,将协议句法结构划分为4个不同的种类,针对这4种不同类型的协议句法结构具体提出了4种不同的可动态扩展的协议句法实现模型.基于该模型实现的协议软件在句法结构上具有灵活可扩展的特性.当该协议扩展句法结构时候,即使相应协议软件处于执行状态,也可以不中止协议软件的运行而完成句法结构的扩展.最后以SIP协议为例,使用VOCAL源码详细说明了如何在该模型的基础上实现协议句法动态扩展.     

特立尼达湖沥青（TLA）路用性能研究

对特立尼达湖沥青的特点和使用情况进行了概述,通过室内试验,对特立尼达湖沥青的高低温性能、水稳定性和抗疲劳性能进行了分析研究．结果表明,湖沥青相对基质沥青的性能大幅提高,主要表现在软化点和耐老化性的提高上,与沥青相容性好,同时湖沥青混合料的路用性能也优于普通沥青混合料．     

快速密钥交换协议JFK的SPIN模型检测

快速密钥交换协议JFK是一种新型的密钥交换协议,它的安全性引起了人们的重视.论文对密钥交换协议交换过程进行分析的基础上,使用Promela语言描述了协议模型,并用LTL刻画了需要满足的性质,最后对协议验证结果分析,表明该协议满足其设计目标.