面向无线传感器网络的认证密钥协商机制

无线传感器网络(Wireless Sensor Networks,WSN)是物联网的重要组成部分,因为WSN能通过因特网将采集到的数据发送到云服务器.认证和密钥协商机制是一个重要的密码学概念,可以确保数据传输的安全和完整性.传感器节点是资源受限的设备,因此目前多数认证和密钥协商机制在计算效率上并不适用于WSN.针对该问题,本文提出了一种新的认证和密钥协商机制,该方案是一种基于椭圆曲线的轻量级认证和密钥协商方案.在eCK安全模型下,将方案的安全性规约到CDH数学困难假设之上,形式化的证明了方案的安全性.最后通过方案对比,表明文章所提出的方案实现了计算效率和安全属性之间的平衡.

安全协议形式化分析方法研究综述

介绍了安全协议的基本概念和分类,然后对安全协议形式化分析方法进行了详细介绍,包括基于模态逻辑的方法、基于模型检测的方法、基于定理证明的方法和基于可证明安全性理论的方法。其中,基于模型检测的方法是目前应用最广泛的一种方法,因此详细介绍了一些常用的基于模型检测方法的工具。最后,总结了当前安全协议形式化分析方法的研究热点和未来的发展方向。

基于Isabelle/HOL的文件系统形式化设计与验证

对于构建可信操作系统而言,文件系统设计和实现的正确性至关重要,即使是已经得到广泛运用的文件系统仍然有漏洞被检测出来。采用形式化方法对文件系统的设计和实现的正确性进行严格的验证是公认的可行方法。当前文件系统的形式化验证工作大多基于宏内核操作系统,而忽视了微内核操作系统架构下文件系统的验证。为此,提出一种微内核架构下采用内联数据机制的文件系统的形式化设计和验证方法。以高阶逻辑(HOL)和自动机模型为基础,将文件系统中的工作对象和系统资源抽象为系统对象来构建文件系统的工作状态,形式化地描述文件系统的相关系统调用的功能语义,将系统调用提供服务的过程抽象为系统工作状态发生跃迁的过程,并给出文件系统功能正确性和安全属性的断言。以实现的安全可信微内核操作系统(VSOS)中的安全可信文件系统(VSFS)为例,在设计阶段构建VSFS的有限状态机模型,并在Isabelle/HOL中抽象描述VSFS的可移植操作系统接口(POSIX)系统调用,分析和归纳出VSFS文件系统正确性断言,使用定理证明的方式来验证VSFS的正确性。实验结果表明,该方法在Isabella/HOL中完成VSFS有限状态机模型细粒度的形式化验证,满足预期的安全需求规范。

Formal Verification of Robertson-Type Uncertainty Relation

Formal verification using interactive theorem provers have been noticed as a method of verification of proofs that are too big for humans to check the validity of them. The purpose of this work is to verify the validity of Robertson-type uncertainty relation toward verifying unconditional security of quantum key distributions. We verify the validity of the relation by using proof assistant Coq and it is turned out that the theorem regarding the relation formally holds. The source code for Coq which represents the validity of the theorem is printed in Appendix.

格值命题逻辑系统L(X)(Ⅱ)

本文讨论以格蕴涵代数为真值域的格值命题逻辑系统Ｌ（Ｘ）的语法问题，给出了系统的公理和推演规则，并证明了系统的可靠性定理、演绎定理＊及协调性定理。

混合偏好模型下的分布式理性秘密共享方案

理性秘密共享方案通过扩展参与者的类型后具有更好的适应性,而现有方案中的共享秘密往往依赖于秘密分发者,但在某些特定环境中秘密分发者并不一定存在.通过对传统分布式秘密共享方案的分析,给出了分布式理性秘密共享方案的一般形式化描述;同时,考虑理性参与者的眼前利益和长远利益,提出一种新的理性参与者混合偏好模型;进一步结合机制设计理论的策略一致机制,设计了一个激励相容的信誉讨价还价机制,以此有效约束理性参与者的行为,从而实现了公平的(t,n)(t,n≥2)分布式理性秘密共享方案的构造;通过从信道类型、秘密分发者的在线/离线需求、方案的通用性和偏好模型等方面与目前相关理性秘密共享方案进行对比分析,进一步分析了所提出方案的优势.

新物联网下的RFID双向认证协议

针对物联网发展的新形势提出一个新型的双向认证协议.有别于传统的RFID认证协议,通过基于零知识证明的认证方法来认证成员身份,并将参与主体的身份安全规约到其自身身份密钥的安全性上.解决了传统的基于加密算法的认证协议中主体的身份安全依赖于所有参与实体信息安全的问题.新协议能够满足一个标签在多个互联的RFID系统中应用时的认证安全.本文给出新协议的详细描述,并且用基于串空间模型的形式化证明方法证明了协议至少满足认证性、秘密性和标签不可追踪性的要求.

协议抗拒绝服务攻击性自动化证明

首先从攻击者上下文与进程表达式2个方面对标准应用PI演算进行扩展,然后从协议状态的角度,应用扩展后的应用PI演算对协议抗拒绝服务攻击性进行建模,提出一个基于定理证明支持一阶定理证明器ProVerif的抗拒绝服务攻击性自动化证明方法,最后应用ProVerif分析与验证了JFK协议与IEEE 802.11四步握手协议抗拒绝服务攻击性,发现IEEE 802.11四步握手协议存在一个新的拒绝服务攻击,并且针对IEEE 802.11四步握手协议存在的拒绝服务攻击提出了改进方法。

eCK模型下的密钥协商

如何构造安全的密钥协商协议是信息安全领域富有挑战性的问题之一。目前安全协议只能达到"启发式"安全,协议的安全假设也不够理想。针对这一问题,提出了基于计算性假设(CDH)的三方认证密钥协商协议,并运用陷门测试定理形式化地证明该协议在eCK模型下是安全的,更好地支持了敌手的询问。

实时系统软件开发过程中形式方法的作用

针对实时系统软件开发的特殊性要求,本文强调形式方法是保证实时系统软件开发正确的一种重要方法。文章首先对形式方法的含义进行了系统的介绍,然后分析了形式方法的三个分支在实时系统软件开发过程中的作用,即形式规约、定理证明、形式验证,并指出了形式方法当前主要应用的能力以及应用的局限性,最后提出了形式方法的一些主要研究方向。

基于Strand空间的认证协议证明方法研究

Strand空间是一种新的安全协议分析模型.系统研究了使用Strand空间模型证明认证协议存在缺陷的方法.在证明过程中,使用目标细化方法证明了认证属性.通过在该模型中引入消息类型检查机制,简化了证明过程.并将该方法应用到包含三方主体的认证协议.最后得出与相关文献相同的结论.

一种改进的RFID双向认证安全强化协议

针对物联网中标签上数据信息容易泄露的问题,提出了一个新型的双向认证安全强化协议。不同于传统的RFID认证协议,提出的协议通过基于零知识证明的认证方法来认证成员身份,利用证明者与验证者实时的信息交互完成零知识证明,并将参与主体的身份安全规约到其自身身份密钥的安全性上。文中最后对本协议的形式化证明,包括秘密性证明、认证性证明、标签不可追踪性三个方面,表明本协议均满足RFID双向认证要求。

基于物理不可克隆函数的RFID双向认证

在物联网应用中,基于传统加密手段的无线射频识别(RFID)认证协议计算量较大,在资源有限的设备中不具有可操作性。为解决该问题,提出一种基于物理不可克隆函数的RFID双向认证协议。分析RFID系统协议的安全需求,根据物理不可克隆函数设计轻量级的双向安全认证协议,利用形式化分析语言证明协议的安全性。分析结果表明,与随机化Hash-Lock、轻量级认证协议等相比,该协议不仅能够有效防止假冒、重放、追踪攻击,也能抵抗物理克隆攻击。

一种形式化的互联网地址机制通用框架

地址机制作为互联网体系结构中的核心组成部分,其演进性决定了对上层网络创新应用的承载能力.传统IP地址的缺陷导致当前互联网陷入僵化,大量新型地址机制的异构性使研究者很难以统一方法论解释和把握未来互联网地址体系的演进发展.针对上述问题,通过对互联网地址机制的演化进行深入研究,抽象最小化核心特征,提出一种能够容纳异构地址策略构建乃至并存的通用框架,包括:1)完备的形式化概念模型,赋予地址常量的精确定义,并形成相关设计原则及约束规范的一致性理论基础;2)抽象多维度、可扩展的接口原语以构建3种核心交互模式,并结合通信公理化性质以及语义,构造一个地址交互过程的正确性证明框架;3)推导出通用地址引擎原型,允许灵活构建地址策略,支持异构地址机制的评估、演进以及共存,以更好地支撑互联网顶层生态的不断演化.

一种新的安全协议形式化分析方法--证据逻辑

形式化分析技术对于安全协议的正确设计至关重要,考虑到现有信仰逻辑分析方法的不足,文章提出了一种新的安全协议形式化分析方法——证据逻辑,即通过对协议主体证据的推理来实现安全协议的形式化分析。与现有的方法相比,该方法不仅能够用于认证协议、密钥协商(交换)协议的分析,也能用于电子商务协议的不可否认性和公平性的分析,因此具有更好的通用性和更强的协议分析能力。

命题逻辑中形式推演证明题的自动评阅系统

自动阅卷评分是大规模计算机考试的必然选择,而数学类主观题涉及运算符号、运算步骤、解题方法多样等问题,其自动评分一直制约着考试系统的发展。数理逻辑是数学的一个分支,命题逻辑是数理逻辑的一部分。命题逻辑的同一个形式可推演性模式可以有不同的形式证明,即存在一题多解的情况,但其证明有严格的程式,针对其特点用C#开发一个适用于其自身的自动评分系统。应用表明,系统操作界面友好,可大大提高教师阅卷的工作效率。

基于模型的开发方法在多应用智能卡中的应用

安全性、可靠性是嵌入式软件的重要性质。为了更好地保证开发的嵌入式软件是可靠和安全的,提出了一种基于模型的开发方法学,包括提炼需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面提取需求,同时明确层次化的精化策略;然后利用形式化方法建立抽象模型并对该模型进行形式化验证,在正确的抽象模型上逐层精化,并对每层模型进行验证;最后,基于满足需求的模型,进一步利用工具完成代码自动生成。该方法从抽象到具体,以逐层递增的方式明确被开发系统的需求及性质,进行形式化建模,通过反馈机制确保模型的正确性及可用性。为了证明该方法学的可行性,文章以多应用智能卡为开发实例,基于Event-B方法及Rodin平台给出了实际建模及证明的过程和结果。

论数学哲学中的直觉主义思想

数学哲学中的直觉主义学派高度重视直觉和个人的创造性思维在科学实践中的作用,这具有积极的意义;它对排中律和间接证明方法有效性的质疑,揭示了经典逻辑只具有相对的真理性;它所倡导的构造性和能行性的研究方法,促进了人工智能和计算机科学的发展。但是,对直觉功能的过分夸大则并不足取。

安全协议形式化分析方法

安全协议的形式化分析是检验协议安全性的必要手段。为了实现协议的规范描述和合理完备的安全性验证,各种数学理论和人工智能方法被引进安全协议形式化分析与自动化验证领域。主要从逻辑方法、模型检测方法和证明方法3个方面对符号化的安全协议形式化分析方法进行了综述,并指出了今后该领域的研究方向。

有穷时间投影时序逻辑的完备公理系统

为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称NF)和正则图(normal form graph,简称NFG).基于NF给出了NFG的构造算法,并利用NFG可描述公式模型的性质证明PTL公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了PTL及其公理系统在系统验证中的应用.结果表明,基于PTL的定理证明方法可方便用于并发系统的建模与验证.