基于马尔科夫决策过程的S-ALOHA协议的形式化分析

S-ALOHA协议是物联网RFID中决定标签信息能否及时可靠的被阅读器识别的关键技术之一,也是提高物联网服务质量的关键.实验,仿真和模拟主要通过探索S-ALOHA协议的部分行为对协议性质进行估算,得出的结论不具有精确性,本文采用一种高度自动化的形式化分析技术-概率模型检测完成S-ALOHA协议的精确分析.首先依据S-ALOHA的工作原理及特性,将其动态行为抽象成能支持非确定性,离散时间以及概率选择的马尔科夫决策过程,然后使用PRISM工具验证了模型的概率可达性和期望可达性,结果表明随着最大退避数的增加,S-ALOHA的期望时间比ALOHA的小6个时间单位,同时S-ALOHA发送数据的平均速度比ALOHA快1.2倍左右.     

概率时态认知逻辑模型检测中三值抽象技术的研究

 为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题,提出了概率时态认知逻辑的三值抽象技术.具体研究内容包括:定义抽象模型及模型上概率时态认知逻辑的三值语义,依据状态空间等价划分建立初始抽象模型,并证明抽象技术对概率时态认知逻辑的满足性保持关系;提出概率时态认知逻辑模型检测算法;依据初始模型检测的结果,给出利用最小证据和最小反例引导的抽象系统的求精过程.最后通过Dining Cryptographer协议说明了抽象技术的应用,及其在约简系统状态空间方面的效果.     

概率实时时态认知逻辑模型检测中抽象技术的研究

概率实时时态认知逻辑PTACTLK模型检测面临着与传统模型检测同样的挑战,即状态空间爆炸问题.抽象是缓解状态空间爆炸问题的最为有效的方法之一.为了缓解概率实时时态认知逻辑模型检测中的状态空间爆炸问题,我们给出了一种抽象技术:对于PTACTLK中的实时部分PTACTL,采用抽象离散时钟赋值,把概率实时解释系统的无限状态空间转化成有限形式;对于PTACTLK中的认知算子K,给出了抽象状态关于智体认知等价的定义.定义了概率实时解释系统的抽象模型,给出了抽象模型上概率实时时态认知逻辑的语义,并证明了由抽象技术演绎得到的抽象模型是原始模型的上近似.最后通过一个通信协议来说明抽象技术的有效性.     

一种新的应用于WLAN中密钥协商和身份认证方案

目前,无线局域网中使用的认证和密钥协商协议结构复杂,且存在安全隐患.文中依据无线局域网的特性,对MB-IBAKA协议进行改进,并在此基础上给出了一种新的密钥协商和身份认证方案.利用模型检测技术对新方案进行形式化分析,分析结果表明,该方案满足认证性、保密性和完整性.另外,新方案在系统开销方面均低于已有方案.