基于事件逻辑的WMN客户端与LTCA认证协议安全性分析

无线Mesh网络是一种新型的宽带无线网络结构,融合无线局域网与点对点模式两者的优势,是无线网络研究的热点之一.基于事件逻辑理论,结合事件结构、事件类、公理簇以及随机数引理,提出置换规则保证用户交互信息在性质置换过程中的等价转换.通过事件逻辑构建客户端与LTCA认证协议的基本序列,对协议交互动作进行形式化描述并证明协议强认证性质.在合理假设下,无线Mesh网络客户端与LTCA间认证协议的安全性得证,研究表明事件逻辑理论不仅可以论证无线网络协议的安全属性,还能对安全协议不同身份主体间的认证性进行证明.通过流程图简化协议形式化证明步骤,阐述事件逻辑理论证明协议安全属性过程,比较分析事件逻辑理论与其他逻辑推理方法,表明事件逻辑理论具有通用性.

基于事件逻辑的无线Mesh网络认证协议安全性证明

无线Mesh网络是一种结合无线局域网和移动自组织网络的新型多跳网络,无线网络的开放性和资源受限性使得无线网络容易遭受重放、伪装等攻击。事件逻辑是一种描述并发与分布式系统中状态迁移和算法的形式化方法,可用于证明网络协议的安全性。以事件逻辑为基础提出一系列性质,其中包含多组合信息交互、不叠加、事件匹配、去重复、去未来,以降低协议分析过程中的冗余度以及复杂度,提高协议分析效率。对无线Mesh网络客户端双向认证协议进行分析,证明该协议能够抵抗中间人发起的重放攻击,无线Mesh客户端双向认证协议是安全的。此理论适用于类似复杂无线网络协议形式化分析。

基于时间区间的并行行为与并发事件逻辑

在基于时间区间的时态逻辑基础上,提出了一种处理主体并行行为与并发事件的逻辑理论框架。文章提出的逻辑系统将事件与动作置于同一个逻辑体系下,以时间区间为基础,深入分析了二者之间的关系,充分发挥了事件的作用,动作的描述得到简化。文章给出了逻辑系统的语法和语义描述,还提出了基于领域描述结构的并发事件冲突消解方法。

基于事件逻辑的CPS组件协同模型

针对CPS系统的异构性、实时性、物理世界与信息世界的高度融合等特征,提出了基于事件逻辑关系的组件协同代数模型。首先,定义了基于时空事件接口的组件形式化表示方法,建立了基于事件驱动的组件协同体系架构。然后,根据组件协同方式分析了事件间的逻辑关系,建立了组件协同代数系统。最后,以智能家居的非法入侵行为为例,使用协同代数式描述事件驱动组件行为的过程。分析表明,基于事件逻辑的组件协同代数模型能够清晰地反应组件间的交互关系,屏蔽了组件的异构性,实现了物理进程与计算进程的融合,为CPS系统的形式化建模提供了新的方法。

基于事件逻辑的炼油企业动态调度系统

针对炼油生产动态调度问题,开发了基于事件逻辑的调度优化系统.在分析大量实际生产事件和调度专家处理经验的基础上定义动态事件,生成事件逻辑.将事件逻辑与广义析取规划相结合,建立了基于事件逻辑的动态调度模型.基于事件逻辑的动态调度建模方法增加了动态调度模型生成的快速性和灵活性,在保证调度优化性的同时获得较好的调度实时性.最后,以某炼油厂"原油供应不足"事件为例进行仿真实验.结果表明,基于事件逻辑的动态调度系统是可行、有效的.

基于事件逻辑的改进Needham-Schroeder协议安全性证明

安全协议是现代网络安全的基础,密码协议的安全性证明是一个挑战性的问题。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于刻画安全协议的形式化描述,是定理证明的基础。用事件序语言、事件类和一个表示随机数、密钥、签名和密文的原子类,给出身份认证协议可以被形式化定义和强认证性证明理论。利用该理论对增加时间戳的Needham-Schroeder协议安全性进行证明,证明改进的Needham-Schroeder协议是安全的。此理论适用于类似复杂协议形式化分析与验证。

基于事件逻辑的PUFs认证协议形式化分析

提出两个事件时序概念与相关规则,用于分析事件关联消息类型为挑战数的时态性质,形式化抽象物理不可克隆函数(PUFs)随机会话秘钥生成功能,扩展事件逻辑(LoET)用于形式化分析PUFs安全协议的理论.以一个基于SRAM PUFs(基于静态随机存取存储器的PUF类型)的安全双向认证协议分析为例,形式化规约了协议基于PUFs随机秘钥生成和双向认证过程,基于扩展的事件逻辑,采用定理证明方法推理证明了该协议在合理假设下满足双向强认证性质.研究表明扩展的事件逻辑理论可用于设计和分析基于PUFs安全协议.

嵌入偏序约简的状态事件线性时序逻辑验证

模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状态事件线性时序逻辑(State/Event Linear Temporal Logic,SE-LTL)给出了一种简洁和直接的方式表达包含状态和事件的系统属性.在SE-LTL中,状态和事件都可以作为原子命题.基于自动机理论的线性时序逻辑(Linear Temporal Logic,LTL)模型检验可以被用来对SE-LTL属性进行验证.然而SE-LTL属性在经典的stutter等价(stutter-equivalent)下无法保持,所以最有效的并发程序状态约简技术:偏序约简技术(Partial Order Reduction,POR)不能直接应用于SE-LTL的验证.该文提出一种新的方法利用已有的偏序约简技术对SE-LTL验证过程的状态空间进行约简.该方法分为两个部分:第一个部分是针对SE-LTL不带NEXT算子的约简方法;第二部分则是带NEXT算子的约简方法.第一部分的主要思想是从一个Büchi自动机(Automata,BA)中抽取出“状态部分”.“状态部分”的含义是该部分只与系统的状态相关.基于“状态部分”,给出关于BA和标签Kripke结构(Labeled Kripke Structure)的同步乘,并在同步乘的构造过程中嵌入偏序约简技术,从而约简同步乘的状态空间,即该文的约简技术是on-the-fly的.嵌入的偏序约简在已有的偏序约简基础上,面向SE-LTL公式中的事件引入新的可见操作的识别方法.为了能够将偏序约简技术应用到所有的SE-LTL公式,该文同时给出验证SE-LTL带NEXT算子的偏序约简算法.NEXT算子是偏序约简的另一个主要障碍.该部分是文中的第二部分工作.该部分的技术依然是on-the-fly的,并且需要与状态部分的识别相结合.通过将该文技术实现到SPIN模型检验器中对已有的模型进行验证.Spin是针对LTL的并发程序模型检验器.实现部分包括SE-LTL到BA的转化,以及on-the-fly的模型验证过程.实验的过程主要针对三个模型集:生产消费者模型,哲学家就餐问题以及公共对象请求代理体系结构中的GIOP协议.验证结果表明,对比完全基于状态的模型检验和不带偏序约简的状态事件模型检验,该文的方法具有更好的效率,并且能够被应用于状态事件系统,特别是安全有关嵌入式系统的验证.

群体性事件的情感逻辑以DH事件为核心案例及其延伸分析

关注情感的机制是理解当下中国群体性事件的重要视角。通过对DH事件的分析及延伸性讨论,本文指出,因表达不畅所致的弥漫性民怨及民众对不满的道义建构,使情感成为主导群体性事件发生与演进的最重要机制。而情感之于群体性事件的逻辑性支撑主要表现为情感宣泄和情感管理,前者是针对权力外围和边缘地带的发泄,后者更为常态地支配群体性事件的过程,而情感表演则成为其中的核心要素,形构出与既有社会运动之情感管理不同的特色。形塑这一特色的是宏观非对称性的国家与社会关系格局,它决定了当下的群体性事件不太可能转变为常态化的社会运动,只能是沿着传统与现代错综交织的轨道间歇性发作,以作为弱势群体对中国转型期社会矛盾的一种特殊回应。

面向事件图和事件时态逻辑的模型检验方法

针对目前没有适合直接对事件图模型进行性质规约的时态逻辑语言,提出一种基于事件的时态逻辑(event temporal logic,简称ETL).ETL以事件作为原子命题,根据事件图的特点增加了对事件取消操作、模型实例化、时间约束和同时事件优先级的表达能力,便于仿真领域的用户在模型检验过程中简洁地对基于事件图的模型应满足的性质进行描述.然后,在ETL公式和自动机理论的基础上,给出了面向事件图和ETL的模型检验方法来判断事件图模型是否满足ETL描述的性质规约.实例验证了ETL对事件图模型具有足够的表达能力以及该方法的有效性.

事件的逻辑:开发中国教育史研究思想潜能的工具

中国教育史学科之所以会陷入理论上非常重要但事实上极其次要的窘境,主要原因是当前的中国教育史研究的“历史学意义”得到充分彰显,而“教育学意义”却被遮蔽了。教育史研究的“教育学意义”之所以会被遮蔽,其根本原因是教育史研究从业者是用“史家的逻辑”来支配其研究。因此,这就需要教育史研究者从“史家的逻辑”的运思方式转向“事件的逻辑”的运思方式。而要想使“事件的逻辑”的运思方式真正落到实处,变为研究者的学术实践,需要教育史研究者确立历史上的行动者必须依赖大量非理性因素采取行动、古今行动者之间的文化差异非常显著等认识前提,切实掌握无立场思维、运用古人的概念思考问题、返回主流与边缘开始分叉的原点观察历史等思维技术。

基于事理图谱的红色档案资源开发利用研究

孙大东、张怡涵在《档案学研究》2023年第5期撰文指出,事理图谱对事件类红色档案资源的开发利用具有良好的助力作用。事理图谱是一个事件逻辑知识库,描述了事件之间的演化规律和模式,在事件表达、事件逻辑组织、事件可视化呈现等方面具有独特优势。红色档案资源事理图谱建构流程包括红色档案资源全方位采集整合和网络化红色档案事理图谱构建。档案部门采集整合红色档案资源,在采集层应注重多渠道、全方位红色档案资源收录与征集,拓展红色档案资源采集主体与范围,为红色档案事理图谱构建提供资源支撑;在整合层应注重对多元异构红色档案资源的解构清洗与重组聚合,为网络化红色档案事理图谱的构建奠定基础。

基于事件知识图谱的变电站监控事件处理方法研究

提出了一种基于事件知识图谱技术的变电站监控事件处理方法,采用知识图谱的方法,建立了变电站监控各事件共指关系、因果关系和时序关系等逻辑关系,叙述了事件间的规律和模式,形成变电站监控事件处理方法。通过实际变电站监控事件处理系统的实操验证,使基于事件知识图谱的变电站监控事件处理方法能较好推广应用。

数字电路的教学中应注重逻辑思维的训练

分析数字电路逻辑设计环节,剖析数字电路教学中存在的问题,基于逻辑电路学习目标,强调逻辑思维的独特性和逻辑思维训练对数字设计的重要性。

基于IEC61850的智能电能质量监测设备模型

随着IEC 61850在电能质量监测方面的扩展,将IEC61850作为电能质量监测设备的通信协议成为建立开放式电能质量监测系统的关键。对电能质量监测IED与变电站自动化系统各功能层的接口进行了设计。遵循IEC 61850及其电能质量附录,建立了采用此接口方式的较为完整的电能质量监测IED对象模型。该模型对基于IEC 61850的电能质量监测设备的研制有较好的指导意义。

基于强认证理论的三方网络协议安全性证明

形式化方法是分析网络安全协议的一种重要方法,网络协议安全性也是信息安全领域的研究热点。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于证明网络安全协议的安全性。以事件逻辑为基础,定义强匹配及匹配会话,结合事件逻辑公理和推理规则,提出了强认证理论。利用该理论对有3个主体的Neuman-Stubblebine协议进行了研究,分析得出发送者是安全的而接收者是不安全的,从而证明了该协议是不安全的,说明了强认证理论适用于三方的网络安全协议。该理论适用于类似多方网络安全协议的安全性证明。

海战场C^4ISR系统的服务自动组合方法

针对C4ISR系统中服务人工智能(artificial intelligence,AI)规划组合存在的服务数量大、不能处理服务执行过程中动态产生的新个体、业务流程和服务质量不确定等问题,提出了一种基于离散事件演算和马尔可夫逻辑网(discrete event calculus-Markov logic network,DEC-MLN)的服务自动组合方法。首先给出了面向服务的海战场C4ISR系统的流程图,用对事件演算进行拓展形成的DEC-MLN对服务的输入、输出、前提条件和执行效果及基本服务流程进行建模,用MLN的权重刻画组合过程中业务流程和服务质量的不确定性。接着提出了一种基于模板的服务自动组合框架,并给出了溯因DEC规划方法。所提方法克服了基于传统AI规划组合方法限于顺序组合的问题;且DEC-MLN的谓词规模较小,提高了服务组合效率;DEC-MLN在处理不确定性的基础上又能解除封闭世界假说的限制,可以处理组合执行过程中新增个体,增加了组合的动态性。最后用实例验证了所提方法的可行性与有效性。

动态调度优化系统在炼油过程中的应用分析

研究与分析动态调度优化系统在炼油过程中的应用的原因以及功能。在事件逻辑当中的实时动态优化调度这一建模方法基础之上对模型进行搭建,将炼油过程当中的动态调度模型建立起来,同时研究出比较实用的一种炼油动态调度优化系统。这种建立在事件逻辑基础之上的建模方法增加了炼油过程中动态调度模型在生成时的灵活性以及快速性,对动态调度优化系统的实用性进行了提高,在相当程度之上使石油炼制行业当中的动态调度模型建立这一难题得到了解决,同时在对调度实时性进行保证的同时得到了理想的动态调度优化性。结论:在炼油厂当中动态调度优化系统模拟应用取得了成功,在一定程度上证明了在事件逻辑基础之上建立模型的方法是行之有效的,在炼油过程中建立起来的动态调度模型也是良好的。

IEEE 802.11w无线网络协议的形式化分析与验证

IEEE802.11是在无线局域网中提供安全通信的标准,主要用于无线工作站访问由访问点管理的受保护无线网络,IEEE802.11w无线认证协议增强了原先基础上所选管理帧的安全性。事件逻辑理论是一种描述并发与分布式系统下协议和算法的逻辑,使用严格的数学规则和逻辑方法对协议的性质进行证明分析。协议认证性的证明是一个安全协议设计中必不可少的一部分,文章基于事件逻辑理论,定义协议运行过程中的基本序列和匹配会话,结合事件逻辑基本公理和推理规则并提出随机数引理对IEEE 802.11w标准交互过程中认证性进行验证,证明得出IEEE 802.11w无线认证协议能够抵抗重放攻击但存在中间人攻击。研究表明,事件逻辑适用于无线认证协议的分析。

基于GTST-DMLD-ESD的装备RMS建模仿真

装备的RMS是装备的重要设计参数,是影响战备完好和保障能力的关键因素。引入GTST-DMLD作为主要建模工具,建立起装备系统的RMS描述模型,以ESD为补充和扩展,对维修过程进行建模。并以GTST-DMLD-ESD模型作为装备RMS仿真的核心,对装备RMS仿真模型的总体框架进行了研究,并对各模块进行了较为详细的探讨。