期刊文献+
任意字段
题名或关键词
题名
关键词
摘要
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到688篇文章
< 1 2 … 35 >
每页显示 20 50 100
已选0条
引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
A Formal Method for Developing Algebraic and Numerical Algorithms 认领 引用 被引量：1
1
作者 ZUO Zhengkang SU Wei +3 位作者 LIANG Zanyang HUANG Qing WANG Yuan WANG Changjing 《Wuhan University Journal of Natural Sciences》 CAS CSCD 2021年第2期191-199,共9页
The development of algebraic and numerical algorithms is a kind of complicated creative work and it is difficult to guarantee the correctness of the algorithms. This paper introduces a systematic and unified formal de... The development of algebraic and numerical algorithms is a kind of complicated creative work and it is difficult to guarantee the correctness of the algorithms. This paper introduces a systematic and unified formal development method of algebraic and numerical algorithms. The method implements the complete refinement process from abstract specifications to a concrete executable program. It uses the core idea of partition and recursion for formal derivation and combines the mathematical induction based on strict mathematical logic with Hoare axiom for correctness verification. This development method converts creative work into non-creative work as much as possible while ensuring the correctness of the algorithm, which can not only verify the correctness of the existing algebraic and numerical algorithms but also guide the development of efficient unknown algorithms for such problems. This paper takes the non-recursive implementation of the Extended Euclidean Algorithm and Horner's method as examples. Therefore, the effectiveness and feasibility of this method are further verified. 展开更多
关键词 algebraic and numerical algorithms formal method partition and recursion mathematical induction
暂未订购 下载PDF
Integrating object-oriented methods and formal methods for requirement engineering 认领 引用 被引量：2
2
作者 陈怡海 缪淮扣 《Journal of Harbin Institute of Technology(New Series)》 EI CAS 2004年第3期295-299,共5页
High quality software requirement specification is crucial for a software development. Although much efforts and research works have been done to address the problem, the errors in user requirement are still prevent u... High quality software requirement specification is crucial for a software development. Although much efforts and research works have been done to address the problem, the errors in user requirement are still prevent us from developing high quality software. To address the problem, this paper proposes integrating graphical specification technique UML with formal specification technique to construct user requirement specification. We also present a prototype tool to perform the automatic translation from UML specification into Object-Z specification. 展开更多
关键词 formal methods UML Object-Z methods integration
暂未订购 下载PDF
On the use of formal methods to model and verify neuronal archetypes 认领 引用
3
作者 Elisabetta DE MARIA Abdorrahim BAHRAMI +4 位作者 Thibaud L'YVONNET Amy FELTY Daniel GAFFÉ Annie RESSOUCHE Franck GRAMMONT 《Frontiers of Computer Science》 SCIE EI CSCD 2022年第3期101-122,共22页
Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and medicine.In this paper,we adopt a formal model to... Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and medicine.In this paper,we adopt a formal model to represent neurons,some neuronal graphs,and their composition.Some specific neuronal graphs are known for having biologically relevant structures and behaviors and we call them archetypes.These archetypes are supposed to be the basis of typical instances of neuronal information processing.In this paper we study six fundamental archetypes(simple series,series with multiple outputs,parallel composition,negative loop,inhibition of a behavior,and contralateral inhibition),and we consider two ways to couple two archetypes:(i)connecting the output(s)of the first archetype to the input(s)of the second archetype and(ii)nesting the first archetype within the second one.We report and compare two key approaches to the formal modeling and verification of the proposed neuronal archetypes and some selected couplings.The first approach exploits the synchronous programming language Lustre to encode archetypes and their couplings,and to express properties concerning their dynamic behavior.These properties are verified thanks to the use of model checkers.The second approach relies on a theorem prover,the Coq Proof Assistant,to prove dynamic properties of neurons and archetypes. 展开更多
关键词 neuronal networks leaky integrate and fire modeling synchronous languages model checking theorem proving Lustre Coq formal methods
暂未订购 下载PDF
Formal methods, statistical debugging and exploratory analysis in support of system development: Towards a verification and validation calculator tool 认领 引用
4
作者 Saikou Y.Diallo Ross Gore +1 位作者 Christopher J.Lynch Jose J.Padilla 《International Journal of Modeling, Simulation, and Scientific Computing》 EI 2016年第1期120-141,共22页
In this paper,we propose an approach to formally verify and rigorously validate a simulation system against the specification of the real system.We implement the approach in a verification and validation calculator to... In this paper,we propose an approach to formally verify and rigorously validate a simulation system against the specification of the real system.We implement the approach in a verification and validation calculator tool that takes as input a set of statements that capture the requirements,internal conditions of the system and expected outputs of the real system and produces as output whether the simulation satisfies the requirements,faithfully represents the internal conditions of the system and produces the expected outputs.We provide a use case to show how subject matter experts can apply the tool. 展开更多
关键词 Verification and validation formal methods modeling and simulation
A Hybrid Formal Description Method Based on FSM,CSP and ADT for Communication Protocol 认领 引用
5
作者 Li Layman 《Journal of Systems Engineering and Electronics》 EI 1998年第3期29-38,共10页
Since communication protocol deals with complex issues related to distribution such as communication, concurrency and synchronization, their development needs to be traced by using sophisticated formal description met... Since communication protocol deals with complex issues related to distribution such as communication, concurrency and synchronization, their development needs to be traced by using sophisticated formal description methods. This paper presents a new hybrid formal method for communication protocol specification. In this method, finite state machine (FSM), communication sequential process (CSP) and abstract data type (ADT) are mixed and the best features of these approaches are offered. In this paper, the main formal description techniques (FDT) for protocol engineering are brieny introduced and a hybrid formal description method based on the FSM, CSP and ADT for communication protocol is described. Finally, this paper presents the formal specification of an example protocol for LAN by using the proposed hybrid formal method. The results of studies show that the hybrid formal description method for communication protocol is an available and effective approach. 展开更多
关键词 Communication protocol Formal description techniques,Protocol engineering Hybrid formal method
暂未订购 下载PDF
A Privilege Separation Method for Security Commercial Transactions 认领 引用 被引量：1
6
作者 Chen Yasha Hu Jun +1 位作者 Sun Yu Gai Xinmao 《China Communications》 SCIE 2010年第6期94-99,共6页
Privilege user is needed to manage the commercial transactions, but a super-administrator may have monopolize power and cause serious security problem. Relied on trusted computing technology, a privilege separation me... Privilege user is needed to manage the commercial transactions, but a super-administrator may have monopolize power and cause serious security problem. Relied on trusted computing technology, a privilege separation method is proposed to satisfy the security management requirement for information systems. It authorizes the system privilege to three different managers, and none of it can be interfered by others. Process algebra Communication Sequential Processes is used to model the three powers mechanism, and safety effect is analyzed and compared. 展开更多
关键词 privilege separation fraud management security commercial transactions formal method
暂未订购 下载PDF
A Formal Reputation System for Trusting Wireless Sensor Network 认领 引用 被引量：1
7
作者 XIAO Deqin FENG Jianzhao ZHANG Huanguo 《Wuhan University Journal of Natural Sciences》 CAS 2008年第2期173-179,共7页
In this paper,a formal system is proposed based on beta reputation for the development of trustworthy wireless sensor networks(FRS-TWSN).Following this approach,key concepts related to reputation are formal described ... In this paper,a formal system is proposed based on beta reputation for the development of trustworthy wireless sensor networks(FRS-TWSN).Following this approach,key concepts related to reputation are formal described step by step for wireless sensor networks where sensor nodes maintain reputation for other sensors and use it to evaluate their trustworthiness.By proving some properties of beta reputation system,the beta distribution is founded to fit well to describe reputation system.Also,a case system is developed within this framework for reputation representation,updates and integration.Simulation results show this scheme not only can keep stable reputation but also can prevent the system from some attacks as bad mouthing and reputation cheating. 展开更多
关键词 wireless sensor networks formal method reputation Beta distribution
暂未订购 下载PDF
基于STPA的联锁系统层级安全需求建模及确认方法 认领 引用
8
作者 陈祖希 周林 +3 位作者 梅萌 王龙生 张宏扬 徐中伟 《中国铁道科学》 EI CAS CSCD 北大核心 2026年第1期185-196,共12页
针对铁路联锁系统安全需求验证中存在的动态行为建模不足和层级约束可追溯性弱等问题,提出1种基于系统理论过程分析(STPA)与形式化开发协同的安全需求建模及确认方法。首先,通过扩展STPA框架,建立多层次的安全需求模型,将顶层抽象的系... 针对铁路联锁系统安全需求验证中存在的动态行为建模不足和层级约束可追溯性弱等问题,提出1种基于系统理论过程分析(STPA)与形式化开发协同的安全需求建模及确认方法。首先,通过扩展STPA框架,建立多层次的安全需求模型,将顶层抽象的系统级安全约束逐步精化为具体的安全需求;其次,设计面向铁路联锁领域的分层精化策略,实现安全需求向形式化模型不变式与事件守卫条件的系统性转化;最后,引入形式化验证工具链,构建集定理证明、模型检测和行为仿真于一体的混合验证机制,通过数学证明完成各精化层级的验证,利用模型检验的状态空间探索与反例生成功能,全面验证由安全需求转化而来的模型不变式及线性时序逻辑(LTL)的正确性,并通过仿真复现典型运行场景,确认系统无死锁且满足预期的安全需求。结果表明:经过3次分层精化,将132条证明义务分解到4层模型中,并通过形式化验证工具进一步完成安全需求的确认,有效降低了铁路联锁系统安全需求建模的复杂性,也为铁路联锁系统的安全运行奠定了基础。 展开更多
关键词 铁路联锁系统 形式化方法 安全需求 线性时序逻辑 STPA
暂未订购 下载PDF
基于事件逻辑的改进型Helsinki协议的形式化分析 认领 引用
9
作者 肖美华 罗运先 钟小妹 《计算机应用与软件》 北大核心 2026年第1期325-332,共8页
安全协议是现代网络通信的基础,证明协议的安全性问题是当今研究热点之一。事件逻辑是一种基于事件系统证明协议安全属性的形式化方法,结合事件类以及事件序语言,利用原子类型表示随机数、密钥等不可猜测的数据,能有效刻画协议系统。针... 安全协议是现代网络通信的基础,证明协议的安全性问题是当今研究热点之一。事件逻辑是一种基于事件系统证明协议安全属性的形式化方法,结合事件类以及事件序语言,利用原子类型表示随机数、密钥等不可猜测的数据,能有效刻画协议系统。针对改进型Helsinki协议的安全性问题,对事件逻辑扩充谓词Fresh和FirstSend及其推理规则,利用扩充后的事件逻辑对协议进行形式化分析,首先对协议构建基本序列,然后通过事件逻辑对协议的认证性以及秘密性进行形式化规约,最后利用公理系统和推理规则证明改进型Helsinki协议满足认证性和秘密性。结果表明事件逻辑理论能有效证明安全协议的认证性和秘密性。 展开更多
关键词 安全协议 事件逻辑 形式化方法 Helsinki协议
暂未订购 下载PDF
基于时间-事件逻辑的ID-AOFE协议形式化分析 认领 引用
10
作者 肖美华 乔珊珊 杨科 《郑州大学学报（理学版）》 CAS 北大核心 2026年第2期48-54,共7页
公平交换协议旨在为数字信息交换提供安全、公平的机制,分析该类协议的公平性是信息安全领域中一个重要的研究内容。时间-事件逻辑具有描述协议主体知识和状态随时间变化的机制,是一种分析协议安全属性的有效方法。基于时间-事件逻辑针... 公平交换协议旨在为数字信息交换提供安全、公平的机制,分析该类协议的公平性是信息安全领域中一个重要的研究内容。时间-事件逻辑具有描述协议主体知识和状态随时间变化的机制,是一种分析协议安全属性的有效方法。基于时间-事件逻辑针对公平交换协议中主体互不信任、存在欺骗行为的特点,通过分析当协议结束运行时,是否存在使不诚实主体获得额外优势的策略来分析协议的公平性。以一个基于身份的混淆乐观公平交换(identity based-ambiguous optimistic fair exchange,ID-AOFE)协议为例进行分析,定义了一种规范的消息交互过程,对ID-AOFE协议消息交互过程中的时间进行了细粒度分析,发现协议中存在两个公平性漏洞,结合图形描述方式给出了攻击发生的全过程,说明了时间-事件逻辑理论的有效性。 展开更多
关键词 形式化方法 时间事件逻辑 ID-AOFE协议 公平性分析
暂未订购 下载PDF
韧性系统工程:概念、方法与挑战 认领 引用 被引量：1
11
作者 杨林 王强 +4 位作者 匡洪宇 操礼春 马小山 李峰 任保全 《中国工程科学》 EI CSCD 北大核心 2026年第3期233-248,共16页
智能时代的复杂系统具有多域互联、“人-机-物”高度融合等特征,在开放、动态甚至对抗环境下受到多维扰动威胁,生存性、可用性面临挑战。针对经典系统工程理论方法在应对不确定性、突发扰动方面的不足,本文提出了韧性系统工程概念并构... 智能时代的复杂系统具有多域互联、“人-机-物”高度融合等特征,在开放、动态甚至对抗环境下受到多维扰动威胁,生存性、可用性面临挑战。针对经典系统工程理论方法在应对不确定性、突发扰动方面的不足,本文提出了韧性系统工程概念并构建了方法框架,探索了系统设计阶段的“韧性设计内置”,以提升复杂系统持续运行与适应演进能力。梳理了韧性概念的多学科定义与内涵,明确了扰动因素分类、韧性能力阶段划分,对比了韧性与容错性、生存性、安全性、鲁棒性等的差异性。在经典系统工程理论方法的基础上引入了韧性理论要素,提出了韧性系统工程的概念与方法流程,将预防、抵御、适应、恢复、演进等韧性能力融入系统全生命周期设计中。构建了涵盖通用指标、领域特定指标,由定量评估、定性评估构成的韧性度量框架,并以自主巡航机器人系统为例阐述了韧性系统工程方法的应用过程。以电力能源系统、信息通信网络、无人智能系统、供应链网络为典型领域,探讨了韧性理论方法的工程化探索情况,进而辨析了落地应用面临的挑战。通过持续的理论创新、方法完善、工程实践,将韧性系统工程发展成为系统工程的新范式,为关键基础设施、智能无人装备、复杂系统的安全可靠与持续运行提供坚实的理论方法支撑。 展开更多
关键词 韧性 系统工程 韧性系统工程 韧性评估 基于模型的系统设计 形式化方法
暂未订购 下载PDF
大模型驱动的形式化定理证明:综述与展望 认领 引用
12
作者 胡俊杰 陈宇杰 +7 位作者 胡义坤 文成 曹嘉伦 马智 苏杰 孙纬地 田聪 秦胜潮 《计算机科学》 CSCD 北大核心 2026年第4期1-23,共23页
定理证明作为逻辑与计算机科学的交汇点,不仅奠定了现代数学推理的形式化基础,也是衡量人工智能逻辑推理能力的试金石,更支撑着软件工程对高可靠性的根本需求。然而,传统定理证明依赖严谨的逻辑推理与繁琐的人机交互,长期面临自动化程... 定理证明作为逻辑与计算机科学的交汇点,不仅奠定了现代数学推理的形式化基础,也是衡量人工智能逻辑推理能力的试金石,更支撑着软件工程对高可靠性的根本需求。然而,传统定理证明依赖严谨的逻辑推理与繁琐的人机交互,长期面临自动化程度有限、推理效率不足以及对专家经验高度依赖等难题。随着大语言模型(LLM)的快速发展,其在自然语言理解、代码生成和逻辑推理等方面展现出突破性能力,为提升自动定理证明的自动化与智能化水平提供了新的契机。为此,系统梳理了大模型驱动的形式化定理证明的研究现状与趋势,重点聚焦于两个主要应用场景。1)在交互式定理证明方面,分析了现有工作是如何缓解其手动开销巨大的难题,并以Lean语言中的Prover系列工作为例,系统总结了其技术演化路径。2)在自动定理证明方面,探讨了大模型如何结合静态分析、验证器反馈等技术,自动生成函数合约、循环不变式等形式化规约,从而显著降低验证门槛。最后,归纳了该领域中面临的共性挑战,包括规约完备性、推理可靠性、数据稀缺性以及工具链集成等,并展望了未来的发展方向。 展开更多
关键词 定理证明 形式化方法 大语言模型 形式化验证 形式化规约
暂未订购 下载PDF
高铁复合无线通信信道形式化建模与验证 认领 引用
13
作者 买宁 关永 +3 位作者 陈善言 王国辉 李希萌 施智平 《软件学报》 EI CSCD 北大核心 2026年第7期2953-2967,共15页
随着高铁无线通信质量需求日益增长,高速移动场景下的通信可靠性已成为高铁无线通信中亟需关注和解决的核心问题.构建可靠的信道模型是解决这一问题的关键.高铁复合无线通信信道建模应充分考虑实际运行环境与信道传播特性,以构建通用性... 随着高铁无线通信质量需求日益增长,高速移动场景下的通信可靠性已成为高铁无线通信中亟需关注和解决的核心问题.构建可靠的信道模型是解决这一问题的关键.高铁复合无线通信信道建模应充分考虑实际运行环境与信道传播特性,以构建通用性强且可靠性高的无线通信信道模型.在复杂无线信道建模方面,形式化方法凭借其严谨的数学建模与严格的逻辑推理能力展现出显著优势.在高架桥这一典型的高铁通信场景中,结合形式化验证方法,提出一种基于小尺度衰落模型的复合无线通信信道的高阶逻辑模型.针对复合信道的长尾分布特性,运用定理证明技术验证了复合无线通信信道的概率密度函数符合第2类修正Bessel函数的分布. 展开更多
关键词 形式化方法 高铁无线通信 复合信道建模 定理证明
暂未订购 下载PDF
操作系统形式规约与验证综述 认领 引用
14
作者 王梓 王洪强 +1 位作者 杨晓艺 兰雨晴 《计算机工程》 CAS CSCD 北大核心 2026年第2期24-45,共22页
操作系统(OS)作为信息时代关键基础设施,广泛应用于军事、工业、医疗等核心领域。其可靠性与安全性直接决定关键领域运行稳定,漏洞易致系统崩溃、数据泄露等严重后果,因此构建系统化安全保障体系具有重要理论与工程价值。以“形式规约-... 操作系统(OS)作为信息时代关键基础设施,广泛应用于军事、工业、医疗等核心领域。其可靠性与安全性直接决定关键领域运行稳定,漏洞易致系统崩溃、数据泄露等严重后果,因此构建系统化安全保障体系具有重要理论与工程价值。以“形式规约-形式验证-工程落地”为框架,梳理近十年该领域研究成果,剖析技术路径与实践应用。在形式规约层面,明确基于迁移系统等数学结构描述系统功能的模型规约与基于线性时序逻辑(LTL)定义安全、活性需求的性质规约的差异,从功能正确性和安全属性两个方面进行阐述,其中,功能正确性涵盖任务管理调度、内存分配回收、异常中断处理、任务间通信与文件系统读写一致性,安全属性聚焦访问控制的BLP模型与BIBA模型、分离内核多域隔离、信息流无干扰与无泄漏理论。在形式验证层面,阐述依托霍尔逻辑验证程序一致性的推理证明、基于LTL与计算树逻辑(CTL)验证时序属性的模型检测、属性验证标准化流程3类核心方法,并以首个通过机器证明实现功能正确与信息流无干扰的seL4微内核为案例,揭示理论到工程的转化路径。在工程应用上,总结汽车领域控制器局域网(CAN)总线通信验证、智能手机Android系统组件间通信鲁棒性检测的成果。本文的系统性梳理旨在为相关领域的研究奠定基础,为大语言模型提供数据集支持,并为最终的技术工程落地提供参考。 展开更多
关键词 操作系统 形式化方法 形式规约 形式验证 系统安全
暂未订购 下载PDF
带递归定义的SMT公式求解技术综述 认领 引用
15
作者 冯维直 刘嘉祥 +1 位作者 张立军 吴志林 《软件学报》 EI CSCD 北大核心 2026年第2期508-542,共35页
带有递归数据结构,如列表(list)和二叉树(tree)等数据类型的程序,在计算机领域被广泛使用.程序验证问题通常将程序转换为可满足性模理论(satisfiability modulo theories,SMT)公式进行求解.递归数据结构通常会转换为代数数据类型(algebr... 带有递归数据结构,如列表(list)和二叉树(tree)等数据类型的程序,在计算机领域被广泛使用.程序验证问题通常将程序转换为可满足性模理论(satisfiability modulo theories,SMT)公式进行求解.递归数据结构通常会转换为代数数据类型(algebraic data type,ADT)和整数等混合理论的一阶逻辑公式.另外,为表示递归数据结构的性质,程序中通常需要包含递归函数,递归函数在SMT中则需要通过包含量词和未解释函数的断言来表示.关注带有ADT和递归函数这两类递归定义SMT公式的求解方法.从SMT求解器、自动定理证明器和约束霍恩子句(constrained Horn clause,CHC)求解器这3方面对现有技术进行梳理和介绍.同时,对主流的求解工具进行统一实验对比,探究现有求解工具和技术在各类问题上的优势和缺陷,尝试寻找潜在的优化方向,为研究者提供有价值的分析和参考. 展开更多
关键词 形式化方法 递归函数 可满足性模理论 归纳推理 引理合成 约束霍恩子句
暂未订购 下载PDF
基于模型检测的核电厂DCS网络功能可靠性验证研究 认领 引用
16
作者 张乘源 杜德君 +3 位作者 陈浠毓 姚姜源 李亚慧 陈日罡 《自动化仪表》 CAS 2026年第6期63-68,74,共6页
传统的核电厂数字化控制系统(DCS)网络可靠性研究采用的检测方法,无法彻底证明系统可靠性。因此,引入网络验证中常用的形式化模型检测技术进行核电厂DCS网络验证。以核电厂DCS网络的功能可靠性为主要研究对象,采用基于数学描述和基于形... 传统的核电厂数字化控制系统(DCS)网络可靠性研究采用的检测方法,无法彻底证明系统可靠性。因此,引入网络验证中常用的形式化模型检测技术进行核电厂DCS网络验证。以核电厂DCS网络的功能可靠性为主要研究对象,采用基于数学描述和基于形式化语言描述的形式化模型的综合建模方法。首先,建立系统的非确定有限自动机数学模型。然后,以该数学模型为基础,使用Promela语言建立该系统的网络功能可靠性验证组件。最后,结合具体系统连接组件,建立某核电厂DCS网络功能可靠性验证模型。使用该模型进行网络验证。验证结果表明,该系统能在一定数量的故障下保持可靠性。通过将该模型验证结果与样机测试结果对比,验证了该模型检测的可靠性验证方法的合理性。该模型能应用于核电厂DCS的网络可靠性评价。 展开更多
关键词 核电厂 功能可靠性 形式化方法 模型检测 Promela 交换机 网络验证
暂未订购 下载PDF
“两条道路”的阐释边界及其方法论意义——基于《1857-1858年经济学手稿》的考察 认领 引用
17
作者 方瑞 《武汉大学学报（哲学社会科学版）》 CSSCI 北大核心 2026年第4期93-101,共9页
“两条道路”方法的科学阐释,是在与古典政治经济学方法论的内在争议中形成的。虽然马克思对这一方法的辩证重构彻底超越了纯粹经验归纳或形式抽象的旧有路径,但在后续学界的阐释中仍存在着混淆“两条道路”的层级关系与功能定位的倾向... “两条道路”方法的科学阐释,是在与古典政治经济学方法论的内在争议中形成的。虽然马克思对这一方法的辩证重构彻底超越了纯粹经验归纳或形式抽象的旧有路径,但在后续学界的阐释中仍存在着混淆“两条道路”的层级关系与功能定位的倾向。为此,有必要回到《1857-1858年经济学手稿》的原始语境,重新厘定“从具体到抽象”与“从抽象上升到具体”的阐释边界。马克思以自然科学的精确性为基础,通过对国民经济事实的系统考察,确立了第一条道路作为经验整理环节的唯物主义前提,从而克服了古典政治经济学在具体与抽象关系问题上的图式化倾向。然而,仅停留于一般的抽象规定,无法把握作为“具体总体”的资本主义社会结构,这就必须通过第二条道路即在思维中系统再现现实的具体,从而在逻辑与历史的统一中为“两条道路”的阐释功能划定严格的理论边界。这一方法论层面的自觉划界,不仅构成了政治经济学批判科学化的核心环节,也为当代中国自主知识体系的建构提供了重要的方法论依据。 展开更多
关键词 《1857-1858年经济学手稿》 两条道路 经验抽象 形式抽象 政治经济学批判
暂未订购 下载PDF
OpenID Connect协议的形式化分析与优化 认领 引用
18
作者 陈琼 缪祥华 袁梅宇 《计算机技术与发展》 2026年第2期195-200,214,共6页
OpenID Connect协议作为实现身份认证与授权的重要机制,其安全性备受关注。利用Scyther模型检测工具,在CK强安全模型约束下对该协议进行形式化分析。分析结果表明,OpenID Connect协议存在明显的安全漏洞,其中包括跨站请求伪造攻击、重... OpenID Connect协议作为实现身份认证与授权的重要机制,其安全性备受关注。利用Scyther模型检测工具,在CK强安全模型约束下对该协议进行形式化分析。分析结果表明,OpenID Connect协议存在明显的安全漏洞,其中包括跨站请求伪造攻击、重放攻击以及中间人攻击等问题。这些安全漏洞严重威胁着协议运行的安全性和用户信息的保密性。针对跨站请求伪造攻击,对state参数实施加盐哈希处理;针对重放攻击,引入时间戳校验机制,客户端请求时服务端生成精确时间戳,通过网络时间协议确保时间同步,仅处理处于预设时间窗口期内的请求;针对中间人攻击,采用SM2数字签名算法,客户端用私钥签名请求,服务器用公钥验证,服务器转发时附加自身签名,确保请求来源可信。改进后的协议在抵御上述安全攻击方面表现出色,经检验具备良好的安全性,能够为用户提供更为可靠的身份验证和授权服务,对于提升OpenID Connect协议在实际应用中的安全性具有重要意义。 展开更多
关键词 OpenID Connect协议 形式化分析 CK安全模型 Scyther 协议分析 改进
暂未订购 下载PDF
基于秩函数合成的程序终止性验证综述 认领 引用
19
作者 蔡裕星 陈长波 李轶 《计算机应用研究》 CSCD 北大核心 2026年第3期641-650,共10页
秩函数合成是程序终止性验证的主流方法之一,其基本思想是通过构造程序变量状态变换的良序映射来证明程序的终止性。近年来,深度学习技术在秩函数合成中的应用取得了初步进展,在一定程度上缓解了形式化方法对程序分析与逻辑推理等专业... 秩函数合成是程序终止性验证的主流方法之一,其基本思想是通过构造程序变量状态变换的良序映射来证明程序的终止性。近年来,深度学习技术在秩函数合成中的应用取得了初步进展,在一定程度上缓解了形式化方法对程序分析与逻辑推理等专业知识的依赖,同时为该领域的进一步研究提供了新的思路。为给后续研究提供理论背景和技术参考,首先介绍了秩函数的基本概念,从基于形式化方法和基于学习方法两个方面出发,系统梳理了单一秩函数、字典序秩函数、多阶段秩函数以及神经秩函数合成的代表性工作;在此基础上,收集了相关研究中的程序样例,构建并公开了一个大规模的线性简单循环人工合成数据集,为基于学习方法的研究提供数据支持。最后,针对现有研究在数据集构造、网络结构与训练策略、验证成本等方面的不足,对未来的研究方向进行了展望。 展开更多
关键词 程序终止性 秩函数合成 形式化方法 机器学习 深度学习 神经秩函数
暂未订购 下载PDF
Formal analysis of robust email protocol based on authentication tests 认领 引用 被引量：1
20
作者 蒋睿 胡爱群 《Journal of Southeast University(English Edition)》 EI CAS 2009年第2期147-151,共5页
Based on the authentication tests and the strand space model, the robust email protocol with perfect forward secrecy is formally analyzed, and the security shortcomings of the protocol is pointed out. Meanwhile, the m... Based on the authentication tests and the strand space model, the robust email protocol with perfect forward secrecy is formally analyzed, and the security shortcomings of the protocol is pointed out. Meanwhile, the man-in-the-middle attack to the protocol is given, where the attacker forges the messages in the receiving phase to cheat the two communication parties and makes them share the wrong session keys with him. Therefore, the protocol is not ensured to provide perfect forward secrecy. In order to overcome the above security shortcomings, an advanced email protocol is proposed, where the corresponding signatures in the receiving phase of the protocol are added to overcome the man-in-the-middle attack and ensure to provide perfect forward secrecy. Finally, the proposed advanced email protocol is formally analyzed with the authentication tests and the strand space model, and it is proved to be secure in authentication of the email sender, the recipient and the server. Therefore, the proposed advanced email protocol can really provide perfect forward secrecy. 展开更多
关键词 email protocol authentication tests formal method perfect forward secrecy strand space model
暂未订购 下载PDF
已选0条
引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 2 … 35 下一页 到第 页
在线咨询 使用帮助 返回顶部 意见反馈