形式化分析

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

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机工程与设计x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于PUF的Kerberos认证协议被引量：1
《计算机工程与设计》2022年第11期3045-3050,共6页冯志华 张宇轩 卢文涛 罗重 
国家重点研发计划基金项目(2018YFB220030)。
为解决Kerberos身份认证协议易遭受口令猜测攻击和重放攻击等局限和不足,提出一种基于物理不可克隆函数(physical unclonable function,PUF)的Kerberos改进协议。该协议的优势在于利用物理不可克隆函数生成的激励响应对代替原协议中的密...
关键词：KERBEROS协议 物理不可克隆函数 身份认证 口令攻击 重放攻击 密钥管理 形式化分析 
改进的轻量级移动RFID双向认证协议被引量：13
《计算机工程与设计》2018年第4期912-917,共6页汪杰 汪学明 
国家自然科学基金项目([2011]61163049);贵州省自然科学基金项目(黔科合J字[2014]7641)
为提高移动RFID认证协议的安全性和计算效率,分析现有的移动RFID双向认证协议存在的问题,提出一种改进的轻量级移动RFID双向认证协议。采用轻量级的Hash函数和动态ID机制结合共享密钥的方法实现标签、移动阅读器和后台服务器通信三方之...
关键词：移动RFID 轻量级 HASH函数 双向认证 形式化分析 
OAuth2.0协议的优化方法被引量：2
《计算机工程与设计》2016年第11期2949-2955,共7页魏成坤 刘向东 石兆军 
为保证OAuth2.0协议的安全性,防止实施过程中出现令牌泄露、钓鱼攻击及中间人攻击等威胁,对原有的协议框架进行优化。通过在Authorization Server和Resource Server之间建立信任机制,同步信任信息,在Authorization Server中引入"安全节...
关键词：开放授权2.0协议 形式化分析 安全性 访问令牌 授权码 
OAuth2.0协议的安全性形式化分析被引量：6
《计算机工程与设计》2016年第7期1746-1751,共6页魏成坤 刘向东 石兆军 
为使用户信任安全系统,保证OAuth2.0协议的有效实施,提出对OAuth2.0协议进行详细的安全性分析。通过对Scyther的研究和OAuth2.0协议的分析,形式化验证OAuth2.0协议的安全性。将OAuth2.0协议标准转化为Scyther的形式化语义,分析协议的安...
关键词：OAuth2.0 Scyther 形式化分析 云计算 安全性 
颜色Petri网的电子商务协议攻击分析方法被引量：1
《计算机工程与设计》2014年第3期814-818,840,共6页司亚利 刘文远 卢贝 
国家自然科学基金项目(61272466;61300193);河北省自然科学基金青年科学基金项目(G2011203195);秦皇岛自筹经费基金项目(2012021A058)
针对现有颜色Petri网方法较少分析电子商务协议存在重放攻击的问题,提出一种基于颜色Petri网的电子商务协议攻击分析方法,用于分析协议中可能存在的攻击。给出带有攻击者的具体建模方法和分析过程,提出从不可否认证据中提取敏感信息作...
关键词：电子商务协议 形式化分析 颜色PETRI网 重放攻击 颜色Petri网工具 
基于Z规格的LR(k)形式化分析及验证
《计算机工程与设计》2013年第7期2403-2407,共5页张杨 段富 
山西省自然科学基金项目(2008011039);山西省科技攻关基金项目(20080322008)
在编译器的构造中,常由于语义的二义性等问题导致不正确的目标程序。为解决此问题,提出了一种新型的语法及语义正确性验证方案,即建立LR(k)文法和Z规格说明的联系,以此构造LR(k)文法的形式化描述及其形式化验证。实验结果表明,该方案能...
关键词：LR(k)文法 形式化描述 形式化验证 Z规格 语法 语义 
动态远程证明协议及其形式化分析
《计算机工程与设计》2012年第8期2901-2905,共5页辛思远 赵勇 王婷 
国家973重点基础研究发展计划基金项目(2007CB311100);国家863高技术研究发展计划基金项目(2009AA01Z437);国家核高基项目(2010ZX01037-001-001);信息安全国家重点实验室(中国科学院软件研究所)开放课题
针对程序的运行时动态攻击给远程证明带来的安全威胁,设计一种动态远程证明协议DRAP,对内存中处于运行状态的程序实施实时的动态度量,并向远程验证方证明平台实时状态。针对DRAP协议所用的TPM功能对LS2逻辑进行扩展,引入重置规则、时刻...
关键词：动态度量 远程证明 时间戳 LS2逻辑 形式化分析 
移动微支付协议Payword的改进与形式化分析
《计算机工程与设计》2011年第8期2572-2574,2579,共4页周璇 汪学明 
国家自然科学基金项目(60963023);贵州大学引进人才科研基金项目(005)
针对移动微支付协议Payword不满足不可否认性的问题,提出了改进的移动微支付协议Payword。相比Payowrd,改进的Payword具有更好的安全性和公平性。为验证改进的移动微支付协议Payword能否满足不可否认性,对SVO逻辑进行扩展,并运用扩展后...
关键词：移动支付 微支付协议 SVO逻辑 协议分析 不可否认性 
公平的电子合同签署协议的博弈分析与改进
《计算机工程与设计》2010年第24期5347-5350,5362,共5页翁立晨 汪学明 
国家自然科学基金项目(60963023);贵州大学引进人才科研基金项目((2008)005号)
为了克服传统时序逻辑以封闭系统方式分析协议的缺点,根据电子合同签署协议的特点引入一种基于博弈的ATL逻辑形式化分析方法。利用该方法分析了一个公平的电子合同签署协议,发现该协议存在不满足公平性和时限性的缺陷。通过向协议中添...
关键词：电子合同签署 形式化分析 时限性 公平性 博弈 MOCHA 
UML顺序图中消息的形式化描述与相关特性分析被引量：5
《计算机工程与设计》2010年第15期3427-3431,共5页黄陇 杨宇航 李虎 
国家863高技术研究发展计划重点基金项目(2004AA119030)
为了实现基于UML顺序图的自动化测试,研究了顺序图中消息的形式化描述方法。形式化地定义了消息的发送和接收,并对二者的一致性关系进行了分析。提出了活动点的概念,讨论了其所具有的性质。建立了活动点集合上的二元关系描述方法,形式...
关键词：统一建模语言 顺序图 消息 形式化分析 活动点 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部