期刊文献+
共找到4篇文章
< 1 >
每页显示 20 50 100
基于迹语义的网络安全协议形式化分析
1
作者 冯珺珺 李光耀 江耘 《计算机与现代化》 2007年第2期107-109,共3页
形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段。本文提出了一种新的简单的迹语义,用于刻画协议部分安全性质,即只针对协议规约的单个主体,此技术支持协议设计者对安全性质进行形式化规约。运用此技... 形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段。本文提出了一种新的简单的迹语义,用于刻画协议部分安全性质,即只针对协议规约的单个主体,此技术支持协议设计者对安全性质进行形式化规约。运用此技术和模型检测器SPIN找到了两种针对TMN协议的攻击,证明了此方法的实用性,可方便地用于其它网络安全协议验证。 展开更多
关键词 安全协议 形式化方法 语义 模型检测 SPIN/Promela
下载PDF
事件结构的近似迹与单元失败等价(英文)
2
作者 李绍荣 王超 《电子科技大学学报》 EI CAS CSCD 北大核心 2016年第4期674-683,共10页
迹等价和测试等价等事件结构上的系统等价关系都立足于观测集上的精确相等,然而精确相等需要的精确度量在现实物理世界里是无法实现的,因此精确等价的应用是非常有限的,并且精确等价关系不具有鲁棒性。为了克服以上缺陷,该文通过使用Ba... 迹等价和测试等价等事件结构上的系统等价关系都立足于观测集上的精确相等,然而精确相等需要的精确度量在现实物理世界里是无法实现的,因此精确等价的应用是非常有限的,并且精确等价关系不具有鲁棒性。为了克服以上缺陷,该文通过使用Baire度量,提出了包含近似交织迹等价、近似交织单元失败等价、近似步骤迹等价和近似步骤单元失败等价的事件系统近似等价框架。这些近似等价具有以下几种良好性质:1)近似等价涵盖了精确等价,即传统精确等价是近似等价的特例。2)近似等价关系具有传递性,可以连续使用。 展开更多
关键词 近似等价 事件结构 单元失败语义 步进语义 语义
下载PDF
基于安全进程代数的非演绎安全模型的分析与验证 被引量:1
3
作者 王精明 虞慧群 《计算机科学》 CSCD 北大核心 2012年第2期56-58,共3页
就刻画安全的性质而言,基于非演绎信息流的安全模型较基于访问控制的安全模型更为确切和本质。在基于迹语义对非演绎信息流安全模型进行分析的基础上,基于安全进程代数给出非演绎模型的形式化描述,然后基于系统的安全进程代数表达式给... 就刻画安全的性质而言,基于非演绎信息流的安全模型较基于访问控制的安全模型更为确切和本质。在基于迹语义对非演绎信息流安全模型进行分析的基础上,基于安全进程代数给出非演绎模型的形式化描述,然后基于系统的安全进程代数表达式给出非演绎模型的验证算法且开发了相应的验证工具,最后通过实例说明该算法的正确性和验证工具的方便适用性。 展开更多
关键词 语义 安全进程代数 信息流安全模型 非演绎模型
下载PDF
基于Petri网的非演绎安全模型的分析与验证
4
作者 王精明 江怡顺 《滁州学院学报》 2012年第2期21-23,49,共4页
就刻画安全的本质而言,基于非演绎信息流安全模型较之与基于访问控制的安全模型更为确切。文章在基于迹语义对非演绎信息流安全模型进行分析的基础上,给出了基于扩展Petri网的非演绎模型的形式化描述,进一步基于Petri网的形式化描述给... 就刻画安全的本质而言,基于非演绎信息流安全模型较之与基于访问控制的安全模型更为确切。文章在基于迹语义对非演绎信息流安全模型进行分析的基础上,给出了基于扩展Petri网的非演绎模型的形式化描述,进一步基于Petri网的形式化描述给出非演绎模型的验证算法且开发相应的验证工具,最后通过实例说明该算法的正确性和验证工具的方便适用性。 展开更多
关键词 语义 PETRI网 信息流安全模型 非演绎模型
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部