安全协议验证

作品数：15被引量：42H指数：3
导出分析报告
相关领域：自动化与计算机技术电子电信更多>>
相关作者：李梦君李舟军陈火旺苏开乐周倜更多>>
相关机构：中山大学国防科学技术大学南京大学解放军理工大学更多>>
相关期刊：《通信与信息技术》《计算机学报》《广西质量监督导报》《计算机应用与软件》更多>>
相关基金：国家自然科学基金国家高技术研究发展计划中国博士后科学基金国家重点基础研究发展计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
协议组合逻辑在实例化空间模型中的语义解释
《广东技术师范学院学报》2016年第2期8-19,共12页肖茵茵 苏开乐 
国家自然科学基金(60903054;61379019);国家"973"重点基础研究发展计划资助项目(2010CB328103);中国博士后科学基金面上项目(2013M540704);广东高校优秀青年创新人才培育项目(LYM11085;LYM11084)资助
安全协议的验证是个不可判问题.为了对实例化空间逻辑ISL的语义表达能力给出理论上的衡量与评价,选择另一种实用的协议组合逻辑PCL,分析了ISL和PCL之间的关系.在此基础上,将PCL的索状空间语义模型转换为ISL的实例化空间语义模型,在实例...
关键词：安全协议验证 实例化空间 协议组合逻辑 索状空间 语义解释 
基于约束求解的安全协议验证
《通信与信息技术》2016年第1期64-68,共5页曹龙 王思 李强 方娟 
研究了基于约束系统求解的安全协议形式化验证方法,该方法将安全协议的执行迹抽象为约束系统,将安全属性表示为基于协议迹的一阶公式,并通过求解约束系统来判定安全属性公式是否得到满足;提出了基于约简规则的一般化约束求解算法,可以...
关键词：协议验证 约束系统 约束求解 推理系统 
安全协议验证中DY模型的构建框架被引量：1
《福建工程学院学报》2015年第3期239-243,共5页唐郑熠 杨芳 薛醒思 
福建省中青年教师教育科研项目(JB14069);福建工程学院科研启动基金项目(GY-Z13112)
攻击者建模是安全协议验证工作的一个重要部分,直接影响到验证的效率与质量,但目前却还没有一个可遵循的形式化框架,影响了建模工作的准确性与客观性。针对这一问题,通过对在安全协议验证中具有广泛影响的DY模型进行形式化,建立了一个D...
关键词：安全协议 形式化 DY模型 攻击者 OTWAY-REES协议 
基于Spi演算的安全协议验证被引量：3
《计算机应用与软件》2011年第3期262-264,292,共4页郑清雄 
在安全协议的各种验证方法中,进程代数方法依托完善的进程演算理论得到了很好的应用。Spi演算在PI演算的基础上扩充了密码操作原语来刻画安全协议,并使用测试等价验证安全属性。讨论了利用Spi演算进行验证的过程,并对经典NSSK协议进行...
关键词：安全协议 SPI演算 测试等价 NSSK协议 
一种基于攻击序列求解的安全协议验证新算法
《计算机科学》2010年第9期32-35,53,共5页韩进 谢俊元 
国家自然科学基金(60503021;60721002;60875038);江苏省高新技术计划(BG2007038)资助
基于完美加密机制前提及D-Y攻击者模型,指出注入攻击是协议攻击者实现攻击目标的必要手段。分析了注入攻击及其形成的攻击序列的性质,并基于此提出了搜索攻击序列的算法,基于该算法实现了对安全协议的验证。提出和证明了该方法对于规则...
关键词：安全协议验证 攻击序列求解 自动化 
有界模型检测和串空间模型相结合的安全协议验证
《小型微型计算机系统》2010年第8期1484-1488,共5页杨晋吉 苏开乐 肖茵茵 李超明 
国家杰出青年基金项目(60725207)资助;国家“九七三”重点基础研究发展计划项目(2010CB328103)资助;广东省自然科学基金项目(06023195)资助;广东省科技计划攻关项目(2007B010400068)资助
提出用BMC和串空间结合的方法对安全协议进行验证.首先是通过串空间的出测试理论先构造不安全协议的部分丛结构,通过该丛结构来约束协议运行的的规模和角色行为;然后用BMC对该丛结构进行建模,建立起对应的有限状态自动机和LTL验证规范,...
关键词：有界模型检测 串空间 协议 验证 NUSMV 
一种基于π^t演算的安全协议建模方法
《计算机研究与发展》2010年第4期613-620,共8页韩进 蔡圣闻 王崇峻 赖海光 谢俊元 
国家自然科学基金项目(60503021;60721002;60875038);江苏省高新技术计划基金项目(BG2007038)
安全协议模型是安全协议分析与验证的基础,现有的建模方法中存在着一些缺点,如:建模复杂、重用性差等.为此提出了一种类型化的π演算:πt演算,并给出了相应类型推理规则和求值规则,πt演算的安全性也得到了证明.πt演算可以对安全协议...
关键词：安全协议模型 πt演算 安全协议验证 类型化系统 形式化方法 
利用类型推理验证Ad Hoc安全路由协议被引量：7
《软件学报》2009年第10期2822-2833,共12页李沁 曾庆凯 
国家自然科学基金Nos.60773170;60721002;90818022;国家高技术研究发展计划(863)No.2006AA01Z432;高等学校博士学科点专项科研基金No.200802840002~~
提出一种基于类型推理的移动Ad-Hoc网络安全路由协议的形式化验证方法.定义了一种邻域限制通信演算NCCC(neighborhood-constrained communication calculus),包括演算的语法和基于规约的操作语义,在类型系统中描述了移动Ad-Hoc网络路由...
关键词：安全协议验证 ad-hoc网络协议 安全路由协议 类型推理 
安全协议验证的归纳方法与串空间形式化比较被引量：1
《计算机研究与发展》2008年第z1期137-142,共6页乔海燕 
国家自然科学基金项目(60673050)
使用归纳方法和串空间分别将NSL(Needham-Schroeder-Lowe)协议及其正确性在辅助证明系统Agda中形式化,并比较了这两种安全协议验证法,证明两种方法形式化的正确性和攻击者能力是相同的.
关键词：安全协议验证 归纳方法 串空间 类型论 
一种基于状态空间演化的网络安全协议执行验证技术
《广西质量监督导报》2007年第5期92-93,共2页陈双飞 
文章提出一种基于状态空间演化的网络安全协议执行验证技术,实现对全局安全协议执行的验证。经分析表明,该技术可以做到及时发现入侵者的攻击,阻止入侵者欺骗参与者或盗取秘密信息。
关键词：进程状态空间 演化 安全协议验证 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部