论文部分内容阅读
根据可信密码模块规范的非形式化描述,利用模型检测工具SPIN对可信密码模块安全性进行形式化分析,给出了可信密码模块形式化分析的基本框架,重点分析了AP授权协议和可信密码模块初始化子系统。指出了AP授权协议存在的缺陷,并给出了具体的改进措施;同时验证可信密码模块初始化子系统状态的一致性。
可信密码模块的模型检测分析
【摘 要】
：
根据可信密码模块规范的非形式化描述,利用模型检测工具SPIN对可信密码模块安全性进行形式化分析,给出了可信密码模块形式化分析的基本框架,重点分析了AP授权协议和可信密码模块初始化子系统。指出了AP授权协议存在的缺陷,并给出了具体的改进措施;同时验证可信密码模块初始化子系统状态的一致性。
【机 构】
：
中国科学院软件研究所信息安全国家重点实验室
【出 处】
：
通信学报
【发表日期】
：
2010年01期
其他文献
由于半固态金属加工技术具有短流程、低能耗和高质量的优点,近年来在全世界范围内得到广泛的应用,半固态金属加工过程的数值模拟技术也得到了快速发展。介绍了半固态金属加工
垃圾邮件的误判问题一直是反垃圾邮件领域中未能得到根本解决的难点。基于清华大学邮箱系统及反垃圾邮件网关系统进行了一整年的部署和实验(2011年9月至2012年10月),通过用户对可疑垃圾邮件点击召回的历史行为进行分析,并采用对其感兴趣的垃圾邮件进行文本相似度计算以及关键参数预测的方法来智能化预测用户对当前某一封垃圾邮件的感兴趣程度,即基于用户主观的选择和体验来帮助用户自动召回其可能感兴趣、然而却被反
提出了一种适应于可信计算平台系统设计的抽象模型,该模型借鉴信息流的基本无干扰理论,利用进程代数和逻辑推理方法,将系统抽象为进程、动作、状态和输出,形式化地定义了进程运行可信,给出进程运行可信的条件和性质,推出进程运行可信隔离定理,在进程运行可信基础上给出系统运行可信的定义,并证明了系统运行可信判定定理。该模型建立在逻辑推理基础上,不依赖于特定的安全机制和实现方法,任何一种符合这个模型的实现方法,都
从理论上定量分析了未预期模型误差影响下秩减估计器的方位估计性能。通过对秩减估计空域谱进行一阶Taylor级数展开得到方位估计偏差的表达式,基于此分别推导了秩减估计器的方位估计均方误差和测向成功概率。针对一种用于均匀阵列互耦自校正的秩减估计器给出数值实验,实验结果验证了理论推导的有效性。
提出了自适应分组调度的策略,使TD-HSUPA(high speed uplink packet access,高速上行分组接入)可以更加灵活地进行分组调度。在自适应调度算法中,系统进行调度算法的同时,在后台运用遗传算法找出更适合当前无线网络环境的权值。系统仿真表明,该算法可以灵活地处理各种网络环境。
水基压铸脱模剂是生产铝合金、锌合金中不可或缺的压铸辅料，脱模剂喷涂工艺对于压铸件质量、压铸模具寿命等具有重要的影响。在对脱模剂喷涂工艺进行描述的基础上，采用有限元分析的方法研究了不同喷涂工艺条件下的模具表层温度场及其温度梯度分布。分析结果表明，脉冲喷涂工艺条件下，模具表面温度呈“之”字形下降。且可以降低模具表面的温度梯度，从而对提高模具寿命带来积极的影响。
针对视频数据库中涉及敏感信息的视频数据分级保护问题,提出视频数据库多级访问控制模型。在该模型中,设计用户身份辨别及身份强度算法,其结果作为用户安全等级隶属函数的输入,该函数值为用户安全等级隶属度,并与视频数据安全等级隶属度一起作为授权规则中安全等级隶属度比较函数的输入,其函数值结合时间元素能够灵活地实现多级访问控制。与已有的访问控制模型相比,该模型最突出的特点是实现动态授权和视频数据分级保护。
基于闲时能量开销优化目标提出了一种适用于异构传感器网络的密度控制算法(DCA),DCA能寻找到一个闲时能量开销近似最小化的连通覆盖集合,该集合最终映射为活跃节点集合。理论分析和实验数据表明,DCA所生成的拓扑能有效降低网络闲时能量开销,延长了网络的生命周期。