形式化分析

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

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机应用x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
关于秘密共享方案在应用Pi演算中的实现被引量：2
《计算机应用》2013年第11期3247-3251,共5页徐军 
针对秘密共享方案的自动化验证问题,提出一种基于等值理论的秘密共享方案自动化验证方法。首先通过等值理论在应用Pi演算中对可验证的多秘密共享方案的密码学语义进行了形式化定义。在此基础上,进一步提出了一种用于将所提出等值理论转...
关键词：PI演算 秘密共享 形式化分析 协议验证 
基于Hash函数的移动射频识别互认证安全协议设计被引量：10
《计算机应用》2013年第5期1350-1352,共3页刘鹏 张昌宏 欧庆于 
为解决移动射频识别(RFID)中阅读器与后端服务器分离所产生的安全问题,设计出一种基于Hash的轻量级认证协议,在无线通信环境下利用Hash的单向性实现标签、阅读器和后端服务器之间三方的互相认证,防止重放攻击、非法读取、位置跟踪等一...
关键词：移动RFID 互认证 HASH函数 形式化分析 轻量级 GNY逻辑 
基于Petri网的列控系统形式化分析方法被引量：2
《计算机应用》2013年第4期1132-1135,1160,共5页刘建昆 宋文 周涛 
国家自然科学基金资助项目(60872089);四川省教育厅应用基础研究项目(09226030)
利用原型Petri网对列车控制系统建模难于实现,用带抑止弧的增广Petri网则可以较好地描述问题。将带抑止弧的增广Petri网作为计算模型,对列车控制系统的一些关键问题进行了建模并给出了两个控制子系统:车站调度子系统与区间运行子系统。...
关键词：PETRI网 抑止弧 列车控制系统 闭塞区间 形式化 
IEEE 802.1X的安全性分析及改进被引量：7
《计算机应用》2011年第5期1265-1270,共6页周超 周城 郭亮 
IEEE 802.1X标准存在一些设计缺陷,为消除拒绝服务攻击(DoS)、重放攻击、会话劫持、中间人攻击等安全威胁,从状态机运行角度对协议进行了分析,指出产生这些问题的根源在于协议状态机的不平等和不完备,缺乏对消息完整性和源真实性的保护...
关键词：网络访问控制 IEEE 802.1X标准 可扩展认证协议 状态机 形式化分析 BAN逻辑 
一种挂号电子邮件协议的设计及其形式化分析被引量：2
《计算机应用》2008年第8期1928-1930,1935,共4页高悦翔 彭代渊 
挂号电子邮件协议需要具备保密性、不可否认性及公平性。提出了一种基于在线第三方的挂号电子邮件协议,以满足挂号电子邮件的一般安全特性。利用扩展Kailar逻辑对该协议进行分析,说明该协议满足不可否认性及公平性,并具有抗篡改、重放...
关键词：挂号电子邮件协议 不可否认性 公平性 形式化分析 KAILAR逻辑 
普适环境中一种安全协议的设计及分析
《计算机应用》2008年第7期1802-1806,共5页杨帆 吕庆聪 曹奇英 
教育部科学技术研究重点项目(104086)
普适环境需要满足"透明""无需人干预的"性质,提出了一种普适计算环境下的安全协议——SPUE。它满足数据认证、数据新鲜性等安全特性,同时满足普适计算的"无需人干预的"性质。协议采用非对称密钥与对称密钥相结合的方法,在解决普适计算...
关键词：普适计算 安全协议 形式化分析 
IEEE 802.11i协议的形式化分析被引量：2
《计算机应用》2008年第5期1125-1127,共3页吴开贵 徐成 廖振岚 
国家自然科学基金资助项目(30400446)
在Furqan提出运用串空间理论对IEEE802.11i协议进行形式化验证的基础上,对IEEE802.11i协议的串空间模型进行了改进,并证明了Furqan没有证明的保密性以及服务器的认证性。分析结果证明,在目前的攻击者模型中,IEEE802.11i协议是安全的。
关键词：IEEE 802.11i协议 串空间 形式化分析 
基于一阶逻辑的非否认协议模型
《计算机应用》2007年第9期2189-2193,共5页范钰丹 韩继红 王亚弟 赵宇 朱玉娜 
为了将密码协议的非否认性和公平性统一在一个框架之下更好地进行分析,提出了一套适用于分析非否认性和公平性的一阶逻辑语法和语义。在此基础上建立了一个用于分析非否认性和公平性的一阶逻辑模型,并以FairZG非否认协议为例进行了分析...
关键词：非否认性 公平性 一阶逻辑 形式化分析 
支持双认证方式的单点登录方案被引量：10
《计算机应用》2007年第3期595-596,613,共3页杨智 陈性元 张斌 
国家863计划项目(2006AA01Z457);金盾工程项目(J1GAB23W013)
支持多认证方式的单点登录是目前的一个新需求,通常这又使认证协议的实现和跨域的认证更加复杂。为此提出一种灵活的支持证书、口令及其组合认证的单点登录方案。方案通过认证协议模板和临时证书票据设计,避免了单点登录的认证协议重复...
关键词：单点登录 认证协议 形式化分析 跨域认证 
非否认协议形式化分析技术被引量：1
《计算机应用》2006年第11期2610-2614,共5页范钰丹 韩继红 王亚弟 赵宇 
对目前现有的非否认协议的几种形式化分析方法进行了分析和比较,指出了它们的优缺点,最后提出了进一步的研究方向。
关键词：非否认协议 形式化分析 公平性 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部