【摘 要】
：
如何自动化验证时间敏感安全协议的安全性一直是形式化研究领域的热点和难点,如何在验证过程中简单而有效地考察由时间戳而引入的约束条件信息成为验证时间敏感协议的难点问
【机 构】
：
北京航空航天大学,计算机学院,北京,100191
【出 处】
：
第三届信息安全漏洞分析与风险评估大会
论文部分内容阅读
如何自动化验证时间敏感安全协议的安全性一直是形式化研究领域的热点和难点,如何在验证过程中简单而有效地考察由时间戳而引入的约束条件信息成为验证时间敏感协议的难点问题.TSPVT是基于Objective Caml语言,在安全协议验证工具SPVT的基础上开发的时间敏感安全协议验证工具.TSPVT在SPVT基础上,首先以扩展了时间事件的类π演算作为时间敏感安全协议描述语言,然后TSPVT将协议的类π演算模型自动转换为带时间约束系统的霍恩逻辑程序P,P由刻画安全协议诚实角色的一组逻辑规则和一组基于扩展的Dolev-Yao模型的攻击者规则组成;最后在对协议霍恩逻辑模型的验证阶段,考察带时间约束系统的规则消解,基于安全协议逻辑程序P解形式不动点的计算,验证安全协议的认证性.以Denning-Sacco协议为例,描述了使用TSPVT自动验证安全协议的过程,表明了TSPVT用于验证时间敏感安全协议的有效性.
其他文献
为有效地进行云计算安全风险评估,本文定义了云计算宏观安全风险评估模型,提出了一种云计算宏观安全风险评估分析方法.通过一个典型的云计算场景用例,对云计算宏观安全风险评
纳米科学技术是20世纪80年代末诞生并迅速崛起的高新技术.它的基本含义是在纳米尺寸(即0.1~100纳米)范围内认识和改造自然,通过直接操作和安排原子、分子运动规律和特性.而创
因为网络安全态势具有较大的随机性,网络安全态势预测是一件很困难的事情.但从大的网络系统上看,安全态势具有一定的内在规律.灰色系统研究信息缺乏时的系统的运行规律,利用
当前漏洞检测存在测试数据有效性低的问题.本文提出一种基于程序内部危险函数覆盖的漏洞测试技术,依据漏洞污点传播模型,主要研究危险函数识别,包含危险函数的执行路径搜索,
二进制软件逆向分析和漏洞挖掘一直是软件安全领域研究的热点.当前的研究和已有工具主要针对某一特定平台;分析方法需要大量手工操作,且依赖安全人员的特定于具体平台环境的
按照现代国际管理认可标准和系列,包括ISO9001品质管理体系、ISO1400l环境管理体系及OHSAS18001职业安全健康管理体系的综合管理体系(Integrated Management System,IMS)概念
樱桃萝卜是一种根茎较小的萝卜,其可供食用部分的大小象乒乓球重十几克到几十克里白外红的根茎。由于其品质细嫩,生长迅速、色泽美观,可以生食、炒食、淹渍和做配菜,是一种
在诸多的包装印刷品生产工艺过程中,烫金作业是经常遇到的,尤其是随着防伪要求的日益增多,烫印镭射标识物变得更为普遍.五颜六色的包装产品易于引起人们视觉上的注意,同时也
PS版耐印率是影响印刷质量的一个关键因素,该文通过分析PS版的特点,找到影响PS版耐印率的几个重要环节,并得出相应的解决办法.
本文针对企业塑料废弃物的逆向物流系统进行剖析，选取某企业作为实证案例，找出其中存在的问题，从回收模式这一根本问题出发，提出在政府协同的基础上，小贩和第三方物流公司共存、第