形式化分析

作品数：446被引量：1033H指数：13
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：王亚弟文静华韩继红冯登国张玉清更多>>
相关机构：解放军信息工程大学西安电子科技大学贵州大学中国科学院研究生院更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划国家科技重大专项更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机学报x
共 条 记 录，以下是1-8
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
可信平台模块的形式化分析和测试被引量：25
《计算机学报》2009年第4期646-653,共8页陈小峰 
国家自然科学基金(60673083;60603017);国家"九七三"重点基础研究发展规划项目基金(2007CB311202)资助~~
可信平台模块(Trusted Platform Module,TPM)是可信计算平台的核心和基础,可信平台模块的功能测试和验证是保证可信平台模块的实现正确性以及规范一致性的重要手段,但是目前尚不存在一种有效严格的可信平台模块测试和功能验证方法,同时...
关键词：可信计算平台 可信平台模块 一致性测试 形式化分析 
分析安全协议猜测攻击的模态逻辑方法
《计算机学报》2007年第6期924-933,共10页毛晨晓 罗文坚 王煦法 
以CKT5逻辑为基础,对其进行了多方面重要的扩展;在原有对称密钥机制的基础上,增加了公开密钥机制和Vernam加密机制以增强其描述协议的能力;打破完善加密假设,给出了一组定义和规则使主体具备猜测和验证口令的能力;给出了与在线猜测攻击...
关键词：安全协议 猜测攻击 CKT5逻辑 模态逻辑 形式化分析 
对一类多级安全模型安全性的形式化分析被引量：10
《计算机学报》2006年第8期1468-1479,共12页何建波 卿斯汉 王超 
北京市自然科学基金(4052016);国家自然科学基金(60573042);国家"九七三"重点基础研究发展规划项目基金(G1999035802)资助.
深入分析了MLS的核心思想,给出了MLS在包含多级客体的系统中的表述形式,分析了安全不变式(in-variant)在系统安全定义中的作用.为了保证模型的安全,必须验证模型的不变式满足MLS策略.为了说明不变式验证的重要性,借助Z语言和形式验证工...
关键词：BLP模型 MLS策略 安全不变式 Z语言 Z/EVES定理证明器 
安全协议的形式化分析技术与方法被引量：61
《计算机学报》2006年第1期1-20,共20页薛锐 冯登国 
国家自然科学基金(60373048)资助~~
对于安全协议的形式化分析方法从技术特点上做了分类和分析.对于安全协议分析技术的发展历史、目前的状况以及将来的趋势作了总体的介绍和总结.根据作者的体会,从纵向和横向两个角度进行了总结.纵向方面主要是从用于分析安全协议的形式...
关键词：安全协议 形式化分析 安全目标 Dolev-Yao模型 密码学可靠性 
SPA:新的高效安全协议分析系统被引量：6
《计算机学报》2005年第3期309-318,共10页李建欣 李先贤 卓继亮 怀进鹏 
国家自然科学基金(90412011);国家"八六三"高技术研究发展计划项目基金(2003AA144150)资助~~
研制高效的自动分析系统是密码协议安全性分析的一项关键任务,然而由于密码协议的分析非常复杂,存在大量未解决的问题,使得很多现有分析系统在可靠性和效率方面仍存在许多局限性.该文基于一种新提出的密码协议代数模型和安全性分析技术...
关键词：信息安全 密码协议 形式化分析 搜索算法 攻击序列 
一种分析电子商务协议的新方法被引量：10
《计算机学报》2004年第4期507-515,共9页王彩芬 葛建华 
西北师范大学重点研究方向基金资助 .
通过将Kailar逻辑和LPC形式方法相结合 ,提出一种新的用于分析电子商务协议的形式化方法 .新方法中的推导规则既简单便捷同时又具有分析签名和分析密文的能力 .该方法既能描述协议中参加者的行为又能够分析参加者拥有的知识和推导协议...
关键词：电子商务 协议 可追究性 公平性 形式化分析 KAILAR逻辑 
UML实时活动图的形式化分析被引量：22
《计算机学报》2004年第3期339-346,共8页崔萌 李宣东 郑国梁 
国家自然科学基金 ( 6 0 2 0 70 3 6 ;6 0 2 3 3 0 2 0 );国家"八六三"高技术研究发展计划基金 ( 2 0 0 1AA1 1 3 2 0 3 ;2 0 0 2AA1 1 6 0 90 );江苏省自然科学基金 (BK2 0 0 1 0 3 3 )资助
统一建模语言 (UML)自从成为OMG规范后 ,应用越来越广泛 .但UML没有精确的、形式化的语义阻碍了它的进一步发展 .该文基于Petri网 ,给出带时间约束的UML活动图的形式化描述 .与Petri网不同的是 ,Petri网的时间约束是在跃迁 (transition)...
关键词：UML 统一建模语言 OMG规范 面向对象 活动图 形式化分析 
一种分析Timed-Release公钥协议的扩展逻辑被引量：5
《计算机学报》2003年第7期831-836,共6页范红 冯登国 
国家重点基础研究规划项目 (G19990 3 5 80 2 );国家杰出青年科学基金( 60 0 2 5 2 0 5 )
在Coffey和Saidha提出的CS逻辑 (CS逻辑将时间与逻辑结构相结合 ,可用于形式化分析Timed release公钥协议的时间相关性秘密的安全性 )的基础上 ,提出了CS逻辑的扩展逻辑 ,它更好地反映了Timed release公钥协议的特性 ,并对一个协议实例...
关键词：Timed-Release公钥协议 扩展逻辑 密钥 密码协议 形式化分析 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部