形式化分析

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

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机工程与应用x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
轻量级移动支付协议公平性分析被引量：4
《计算机工程与应用》2018年第19期82-87,共6页李茜 王峥 马建芬 李娜 
山西省重点研发计划国际合作项目(No.201603D421013)
为保证移动支付安全、顺利进行,必须采用安全的移动支付协议。针对计算和存储能力有限的移动设备和不可靠的移动环境,选择采用对称加密的轻量级移动支付协议PCMS,使用串空间理论对其建模,进行形式化分析。通过图的方式直观描述协议的执...
关键词：移动支付协议 形式化分析 串空间 公平性 模型检测 
一种改进的满足后向安全的RFID双向认证协议被引量：8
《计算机工程与应用》2017年第9期136-140,共5页马远佳 刘道微 
广东省云机器人(石油化工)工程技术研究中心开放基金资助课题(No.201507B05);广东省石化装备故障诊断重点实验室开放基金(No.772715);广东省科研创强重点项目(No.2012B01040);广东省科技计划项目(No.2014A020208139)
针对在物联网应用中,现有的RFID双向认证协议存在认证效率低和安全隐患等问题,提出了一种满足后向安全的RFID双向认证协议,采用随机数使标签保持信息的新鲜性,从而实现标签与阅读器之间的双向认证;通过Rabin加密算法的运算单向性,来解...
关键词：物联网 射频识别 Rabin算法 BAN形式化分析 双向认证 
基于SPIN的远程证明协议的形式化分析及改进被引量：4
《计算机工程与应用》2017年第1期34-38,72,共6页秦嫚蔓 王峥 王莉 
国家高技术研究发展计划(863)项目(No.2014AA015204)
远程证明是解决移动支付安全问题的有效手段之一。通过对可信计算远程证明协议进行分析,发现用户平台配置信息的隐私性、用户的认证性和远程验证者的认证性存在脆弱点,使用SPIN模型检测工具,应用模型检测方法对协议进行了形式化分析,检...
关键词：移动支付 远程证明协议 用户属性 形式化分析 SPIN模型检测 
认证测试中协议主体串参数一致性研究被引量：1
《计算机工程与应用》2015年第13期86-91,152,共7页余磊 魏仕民 卓泽朋 
安徽高校省级自然科学研究重点项目(No.KJ2014A231;No.KJ2014A220)
针对认证测试基础理论在协议主体串参数一致性分析方面,因形式化判定规则不足所产生的分析复杂度较高和自动化程度较低问题,通过对消息组件结构的形式化,以及认证测试结构的共性分析,基于认证测试基础理论对认证测试结构进行形式化建模...
关键词：安全协议 形式化分析 串空间模型 认证测试 串参数 
协议主体密钥在测试组件构造上的性质分析被引量：6
《计算机工程与应用》2013年第6期114-117,共4页余磊 魏仕民 
安徽高校省级自然科学研究项目(No.KJ2012B158)
针对认证测试理论在测试组件构造方面缺少具体形式化构造规则的不足,根据协议主体在认证测试中的角色特点,以及包含惟一源发消息的消息组件在认证测试中的作用和性质,对消息组件进行分类和定义并提出认证测试模型的概念,基于认证测试模...
关键词：安全协议 形式化分析方法 串空间模型 认证测试 消息组件 测试组件 
有色Petri网的扩展使用控制策略模型设计被引量：1
《计算机工程与应用》2012年第33期96-100,共5页李沛武 雷金娥 
江西省自然科学基金(No.2009GZS0082;No.2011ZBAB201005);江西省工业支撑计划(No.2011ZBBE50030)
为解决目前UCON模型和策略规范存在系统应用功能与安全策略集成性差、缺少事后义务和无并发性控制问题,通过定义行为、安全和并发规则,提出了一种扩展的使用控制策略,采用有色Petri网技术,达到形式化定义、分析的目的,为将来的研究工作...
关键词：使用控制 形式化分析 有色PETRI网 扩展使用控制策略模型 
一种适于带时间戳安全协议的形式化分析方法被引量：1
《计算机工程与应用》2012年第36期116-120,共5页范玉涛 苏桂平 
中国科学院研究生院院长基金(No.Y15102HN00)
提出了一种适用于带有时间戳的安全协议的有色Petr(iCPN)形式化分析方法,利用一个非自动时钟来描述协议中涉及的时间因素。对著名的WMF协议建模,利用CPN Tools,采用CPNML语言编写查询函数验证协议的新鲜性,从而发现协议的漏洞。应用分...
关键词：形式化分析 有色Petri网(CPN) 时间戳 安全协议 
Needham-Schroeder协议的认证测试方法形式化分析被引量：1
《计算机工程与应用》2010年第19期100-102,共3页李廷元 秦志光 刘晓东 张选芳 
民航局科研基地863项目(No.2007kf003)~~
在安全协议的形式化分析方法中,串空间模型和基于串空间模型的认证测试方法是比较常用的验证方法。针对Need-ham-Schroeder协议存在中间人攻击的缺陷,提出对协议的改进并采用认证测试方法,验证了改进的协议可以满足协议的安全目标。
关键词：安全协议 形式化分析 串空间模型 认证测试方法 Needham-Schroeder协议 
TLS协议认证测试模型与形式化分析被引量：2
《计算机工程与应用》2009年第23期100-103,共4页孔娟 曹利培 
TLS协议是一种重要的传输层安全协议,得到了广泛的应用。在结合串空间理论和方法的基础上,通过构造TLS握手协议的认证测试模型,提出了TLS协议的DH参数签名认证测试方案,分析和证明了协议的保密性和认证性等关键属性。结果表明TLS协议满...
关键词：传输层安全协议 认证测试 串空间 形式化分析 
改进的安全协议一阶逻辑模型
《计算机工程与应用》2008年第26期95-98,101,共5页张超 韩继红 王亚弟 朱玉娜 
由于Blanchet安全协议一阶逻辑模型不能够给出易于理解的攻击序列,基于该安全协议一阶逻辑模型,对逻辑推理中的规则及合一化操作进行了分类,给出了操作置换规则,明确了改进系统中的一些关键性概念和命题。最后,以化简的Needham-Schroede...
关键词：安全协议 形式化分析 一阶逻辑模型 攻击序列重构 
全选清除导出
共3页<123>
检索报告 对象比较 聚类工具 使用帮助 返回顶部