共查询到20条相似文献，搜索用时 203 毫秒
1.
一种混合的安全协议形式化分析技术 总被引：1，自引：0，他引：1
分析了模型检测技术和逻辑推证技术的优点与不足,并在此基础上提出了一种混合的形式化分析技术的说明,该技术可提供更为完全的安全协议形式化分析. 相似文献
2.
安全协议是网络安全的重要因素，但是它并不完善．我们需要用形式化的方法去分析它是否具有相应的安全属性.本文主要分析了三类典型的安全协议形式化分析方法，研究这些方法的基本思想和优缺点．并提出了形式化分析方法中存在的问题及可行的解决办法. 相似文献
3.
安全协议形式化分析理论与方法研究综述 总被引：12，自引：0，他引：12
综述目前安全协议形式化分析的理论与方法 ,包括安全协议的分类与模型 ,安全协议形式化分析的 3种典型方法 (基于推理的结构性方法 ,基于攻击的结构性方法 ,基于证明的结构性方法 ) ,安全协议分析的形式化语言 ,安全协议设计的形式化方法 ,以及安全协议形式化分析面临的挑战 相似文献
4.
采用针对Web服务组合协议的扩充π-演算,形式化地描述了Wab服务流程的行为,在抽象的形式化层次上描述了由不同Web服务组合协议构成的流程之间互操作的中间适配规范,适配器生成规范和由规范制导的适配器生成方法.通过适配器生成过程的形式化描述可以自动生成该适配器.通过实例具体实现了BPEL4WS和WSCI互操作的适配器形式化描述,以此说明可以在抽象层次上实现不同Web服务组合协议描述的服务流程之间的互操作. 相似文献
5.
BAN类逻辑是一款非常优秀的形式化分析工具。它能够帮助设计和分析各种安全协议。介绍了BAN逻辑的产生、构建、分析步骤,指出BAN逻辑现存在的缺陷。同时用BAN逻辑形式化分析了Yahalom协议。 相似文献
6.
本文介绍了循环不变式的理论和特点,在详细分析循环结构的基础上,结合实例介绍了在教学中引导学生通过循环不变式设计循环程序的过程,给出了通过循环不变式设计循环程序的具体步骤。 相似文献
7.
分析和研究了谓词逻辑在ATM上的应用。分别介绍了谓词演算的含义、ATM系统原理和怎样利用谓词逻辑将ATM系统形式化。通过谓词演算、加锁协议等方法,对ATM取款流程进行了形式化描述,建立ATM的四备规则,保证了ATM的安全性和有效性。 相似文献
8.
给出用PVS对密码协议进行形式化规范的一种方法.该方法以高阶逻辑为规范语言,利用trace模型来描述协议的行为,并假设系统中存在强攻击者和理想加密系统.重要的结构如消息、事件、协议规则等都通过语义编码方式定义. 相似文献
9.
介绍了抽象状态机（ASM）,建立了基于这种形式化方法的协议描述于验证的环境,并建立了一般意义上的入侵者模型.作为应用实例,给出了 Helsinki协议的 ASM规约,说明利用这个规约可以直观的演绎 Horng-Hsu攻击. 相似文献
10.
为π演算建立具有安全级别的简单类型系统,并证明该类型系统在规约语义下的类型可靠性.此类型系统使得π演算成为安全系统、安全协议分析与规范的普适形式化工具. 相似文献
11.
采用Gröbner基方法,可以把一个在有限群作用下不变的多项式写成不变环的生成元的多项式.核心问题是如何有效地计算这个正维不变理想的Gröbner基.本文引入一个有效提升算法来计算这组Gröbner基.当用straight line program模型对整个计算过程进行复杂度分析时,可以把计算开销控制在多项式时间内. 相似文献
12.
采用Gr(o)bner基方法,可以把一个在有限群作用下不变的多项式写成不变环的生成元的多项式.核心问题是如何有效地计算这个正维不变理想的Gr(o)bner基.本文引入一个有效提升算法来计算这组Gr(o)bner基.当用straight line program模型对整个计算过程进行复杂度分析时,可以把计算开销控制在多项式时间内. 相似文献
13.
《Journal of The Franklin Institute》2023,360(8):5481-5503
Neural decoders were introduced as a generalization of the classic Belief Propagation (BP) decoding algorithms. In this work, we propose several neural decoders with different permutation invariant structures for BCH codes and punctured RM codes. Firstly, we propose the cyclically equivariant neural decoder which makes use of the cyclically invariant structure of these two codes. Next, we propose an affine equivariant neural decoder utilizing the affine invariant structure of those two codes. Both these two decoders outperform previous neural decoders when decoding cyclic codes. The affine decoder achieves a smaller decoding error probability than the cyclic decoder, but it usually requires a longer running time. Similar to using the property of the affine invariant property of extended BCH codes and RM codes, we propose the list decoding version of the cyclic decoder that can significantly reduce the frame error rate(FER) for these two codes. For certain high-rate codes, the gap between the list decoder and the Maximum Likelihood decoder is less than 0.1 dB when measured by FER. 相似文献
14.
The existence and uniqueness of stationary distribution and ergodic properties of a stochastic system are obtained. Especially, different from the existing methods, a new method is introduced to analyze almost sure permanence and uniform boundedness of the stochastic predator–prey model. This new idea is based on geometric structure of invariant set for a stochastic system. More specifically, we obtain our main conclusions by showing the invariant set for the stochastic population system lies in the interior of the first quadrant. It is interesting and surprising that the stochastic population model can guarantee a uniform boundedness almost surely. Some numerical simulations are carried out to support our results. 相似文献
15.
《Journal of The Franklin Institute》2019,356(8):4622-4647
The Region of Attraction of an equilibrium point is the set of initial conditions whose trajectories converge to it asymptotically. This article, building on a recent work on positively invariant sets, deals with inner estimates of the ROA of polynomial nonlinear dynamics. The problem is solved numerically by means of Sum Of Squares relaxations, which allow set containment conditions to be enforced. Numerical issues related to the ensuing optimization are discussed and strategies to tackle them are proposed. These range from the adoption of different iterative methods to the reduction of the polynomial variables involved in the optimization. The main contribution of the work is an algorithm to perform the ROA calculation for systems subject to modeling uncertainties, and its applicability is showcased with two case studies of increasing complexity. Results, for both nominal and uncertain systems, are compared with a standard algorithm from the literature based on Lyapunov function level sets. They confirm the advantages in adopting the invariant sets approach, and show that as the size of the system and the number of uncertainty increase, the proposed heuristics ameliorate the commented numerical issues. 相似文献
16.
The usual use of fractals involves self-similar geometrical objects to fill a space, where the self-similar iterations may continue ad infinitum. This is the first paper to propose the use of self-similar mechanical objects that fill an alloted space, while achieving an invariance property as the self-similar iterations continue (e.g. invariant strength). Moreover, for compressive loads, this paper shows how to achieve minimal mass and invariant strength from self-similar structures. The topology optimization procedure uses self-similar iteration until minimal mass is achieved, and this problem is completely solved, with global optimal solutions given in closed form. The optimal topology remains independent of the magnitude of the load. Mass is minimized subject to yield and/or buckling constraints. Formulas are also given to optimize the complexity of the structure, and the optimal complexity turns out to be finite. That is, a continuum is never the optimal structural for a compressive load under any constraints on the physical dimension (diameter). After each additional self-similar iteration, the number of bars and strings increase, but, for a certain choice of unit topology shown, the total mass of bars and strings decreases. For certain structures, the string mass monotonically increases with iteration, while the bar mass monotonically reduces, leading to minimal total mass in a finite number of iterations, and hence a finite optimal complexity for the structure. The number of iterations required to achieve minimal mass is given explicitly in closed form by a formula relating the chosen unit geometry and the material properties. It runs out that the optimal structures produced by our theory fall in the category of structures we call tensegrity. Hence our self-similar algorithms can generate tensegrity fractals. 相似文献
17.
Bond graph formulation of an optimal control problem for linear time invariant systems 总被引：1，自引：0，他引：1
A recent communication has proposed a conjectural procedure for representing a category of optimal control problems in bond graph language [W. Marquis-Favre, B. Chereji, D. Thomasset, S. Scavarda, Bond graph representation of an optimal control problem: the dc motor example, in: ICBGM’05 International Conference of Bond Graph Modelling and Simulation, New Orleans, USA, January 23-27, 2005, pp. 239-244]. This paper aims at providing a fundamental theory for proving the effectiveness of this procedure. The class of problem that the procedure can deal with has been extended. Its application was formerly restricted to linear time invariant siso system. The systems considered now are linear time invariant mimo systems. The optimization objective is the minimization of dissipation and input. The developments concerning the optimal control problem are based on the Pontryagin maximum principle and the proof of the effectiveness of the procedure makes a broad use of the port-Hamiltonian concept. As a result, the bond graph representation of the given optimization problem enables the analytical system, which provides the optimal solution, to be derived. The work presented in this paper is the first step in research with perspectives towards formulating dynamic optimization problems in bond graph and, towards coupling this formulation with a sizing methodology using bond graph language and a state-space inverse model approach. This sizing methodology, however, is not the topic of this paper and thus is not presented here. 相似文献
18.
《Journal of The Franklin Institute》2021,358(18):9483-9509
This paper mainly studies the design of iterative learning constrained model predictive fault–tolerant control for batch processes accompanied by multi–delays, interference and actuator failures. Firstly, an equivalent 2D–Roesser model with multi–delays is established. The definition of invariant set is proposed. The sufficient conditions with invariant set characteristics are established. After that the predictive fault-tolerant controller is designed with terminal constraints against external disturbances. In this paper, Lyapunov–Razumikhin Function (LRF) is used to form Lyapunov–Krasovskii Function (LKF) to construct the sufficient condition for the predictive control system that satisfies the terminal constraint condition. Moreover, the system state still remains invariant set characteristics. This method has certain advantages in controller design and calculation. In addition, it has the characteristics of simple design and small computation, and is especially suitable for small delay systems. Finally, a simulation experiment in the nonlinear batch reactor is carried out. Compared with the traditional one-dimensional (1D) method, the presented strategy has better performance through simulation experiment. 相似文献
19.
A pulse compressor is utilized in many aspects of signal processing. Compression is usually accomplished by using special matched-filter-signal pairs. An alternative method takes advantage of the fact that any linear dynamic system can be excited to produce a time-limited output. Accordingly for a given dynamic system a synthesis procedure is provided for stepwise-constant input pulses evoking a time-limited response. Pairing the signal and system carefully leads to pulse compression. The Doppler invariant pulse compression is an important special case. Many examples are given. 相似文献
20.
Roberto R. Kampfner 《Information processing & management》1985,21(5):401-414
An organizational information system can be viewed, in a broad sense, as a computational model of organizational activity and function. Logical requirements of information systems are defined, according to this view, as constraints imposed by the logical structure of such a computational model on the design, implementation and operation of information systems. In this study a formal model for the specification of logical requirements is presented in detail and its role as a tool for systems development is discussed. Three main advantages of the specification of logical requirements that can be capitalized through the use of this formalism are: (1) logical requirements are invariant with respect to specific means in which information processing is actually accomplished; (2) they can be easily related to relevant aspects of organizational activity and function; and (3) they can be related to basic components of the corresponding software systems, either existing or being developed. 相似文献