Andrew Secure RPG协议的一种组合分析方谢

逻辑方法和模型检验方法是安全协议的两种重要分析方法。逻辑方法简单、直观，但其最大问题是不够完备，模型检验方法自动化程度高且能生成不满足所需求性质的反例。先用BAN逻辑对Andrew Secure RPC协议进行分析，并在此基础上组合模型检验方法进行分析，结果表明逻辑方法组合模型检验方法分析协议比只用逻辑方法分析得到的结果更全面且更具体。     

基于PCL的改进型Helsinki协议的形式化分析

针对改进型的Helsinki协议安全性问题,利用协议组合逻辑PCL对协议进行形式化分析.首先使用基于"Cords演算"的程序描述语言对协议本身进行形式化描述,然后通过协议逻辑描述协议的安全属性,最后给出性质和定理,并通过逻辑推理证明改进型Helsinki协议满足其安全要求,该协议是安全的.     

Kerberos协议的形式分析与NuSMV检验

NuSMV是一个基于计算树逻辑的符号化模型检验工具。对Kerberos认证协议进行分析,并对其建立有限状态机模型,利用NuSMV保密性、认证性和活性等从3个方面进行了验证,指出Kerberos协议存在不安全性。     

分析和设计安全协议的新逻辑的语义

文献[1]中提出了一种分析和设计安全协议的新逻辑.协议分析者可以用该逻辑来对安全协议进行分析,而协议设计者可以使用该逻辑用一种系统的方法来构造安全协议.文献[1]没有给出该逻辑的形式化语义,因为串空间模型具有良好的语义,现将新逻辑和串空间模型结合起来,给出新逻辑的串空间语义,并运用该语义证明了新逻辑的推理规则是正确的.     

基于方法集的国防科技工业企业创新能力评价模型研究

首先应用AHP法和德尔菲法构建了国防科技工业企业的指标集及其权重,再分别运用各种评价方法对其进行综合评价。模型对各评价结果进行事前一致性检验,在得到各方法评价结果具有一致性的前提下再运用三种组合评价模型对各方法的评价结果进行组合评价。为了衡量组合评价的结果与各评价方法的评价结果是否吻合,又应用Spearman等级相关系数进行组合评价方法的事后检验,并根据Spearman等级相关系数的大小,选出最优的组合评价方法。最后,运用此模型进行实证分析,以验证本方法的可行性。     

基于模型检测的SSL协议形式化验证

针对传统的测试方法无法对网络安全协议的逻辑本身进行验证等问题,提出了一套基于形式化分析和SPIN模型检测的验证方法.该方法首先以BAN逻辑对目标协议进行形式化分析,然后推断目标协议存在的问题缺陷,并通过Promela语言对其构建SPIN模型,最后通过SPIN软件验证推断的正确性.并以SSL协议作为具体实例予以论证,结果表明所提方法具可行性.     

基于Strand Space模型的CCITT X.509协议分析

运用前沿的安全协议形式化分析方法--Strand Space模型理论,对CCITT X.509协议进行了分析,指出了该协议在保密性和认证正确性方面的缺陷,得到了BAN逻辑分析没有得到的保密性缺陷和相同的认证正确性缺陷.同时提出了改进的X.509协议,并用Strand Space模型论证了改进协议的保密性和认证正确性.     

应用逻辑推导图方法对一个不可否认协议的分析

以之前所提出基于模态逻辑的协议推导分析方法为基础, 用Java专家系统外壳(JESS)实现了协议推导分析工具, 对一个具体的不可否认协议进行分析,以验证逻辑推导图方法的作用.分析结果清晰地显示各协议内容对协议目标实现的作用, 并以此为基础说明协议内容中的冗余.通过与传统协议分析方法进行比较, 说明了这一方法可以更清晰地说明协议内容对协议目标的贡献作用.同时,也在分析过程中指出了SVO逻辑协议分析方法对假设的过度依赖性这一缺陷.     

基于粗糙集的组合逻辑优化算法

运用粗集理论对逻辑函数进行知识表达的方法,提出了基于粗糙集的组合逻辑优化方法,并给出了相应的算法.通过对20变量以下的组合逻辑标准Benchmark-89,91和93相容逻辑矩阵例题进行了检验,结果表明此算法是正确的,并具有显著的化简效果.     

基于组合预测包容性检验的单项模型选择

组合预测模型实际上是单项预测模型的信息进行选择利用的过程。最优组合中单项预测模型的选择是十分重要的问题,将包容性检验应用于组合预测单项预测模型的选择;给出了基于组合模型包容性检验的单项模型的选择方法和步骤,该方法主要是利用增加一个单项预测方法的组合预测模型与原组合预测模型之间的包容性检验,确定单项模型是否要保留在组合预测模型中,这样可以达到提高组合预测的预测有效度。最后通过应用实例的分析,表明通过组合预测模型的包容性检验筛选出合适的单项预测模型,再建立组合预测模型就能够达到提高预测精度的效果,因此该方法是可行的和有效的。     

Belief and Knowledge Reasoning

Alternating-time Temporal Epistemic Logic (ATEL) which is an important kind of multi-agent cooperation logics only takes knowledge into account, but does not deal with belief of agents. By introducing three kinds of belief operators into ATEL, a new multi-agent cooperation logic named ATBKL (Alternating-time Temporal Belief and Knowledge Logic) was developed. A model checking algorithm was proposed. It is proved that the model checking complexity of ATBKL is the same as that of ATEL, i.e., the presented logic is better for further study of multi-agent systems.     

基于模型检测的审计方法逻辑正确性验证

利用模型检测的建模方法,对审计方法及其计算过程和期望的计算结果进行建模,并在模型检测器上对逻辑性较强的凭证断号检查审计方法进行验证,提出一个利用模型检测方法对审计方法逻辑正确性验证的框架.利用模型检测器给出的反例,对验证的审计方法进行修正.实验结果表明,模型检测方法能验证审计方法逻辑的正确性.     

Model Checking Workflow Net Based on Petri Net

The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic （CTL） allows us to verify the soundness with symbolic model checkers. Therefore the state explosion problem in verifying soundness can be overcome efficiently. When the property is not satisfied by the system, model checking can give a counter-example, which can guide us to correct the workflow. In addition, relaxed soundness is another important criterion for the workflow. We also prove that Computation Tree Logic ＊ （CTL ＊ ） can be used to character the relaxed soundness of the workflow.     

限制的语言表达形式及其与修饰的区别

限制的语言表达形式有三种:概念加限制词;不加限制词,属概念直接过渡到种概念;通过语境进行限制。概念的逻辑限制与语词的修饰从外延上看,二者是交叉关系,其中非限制性的修饰和定语性限制区别在于:非限制性的语词修饰,其修饰词不能缩小被修饰的语词所表达的概念的外延,定语性限制中的限制词即定语一定能缩小概念的外延;定语性限制的定语有区别性,非限制性修饰中的修饰词一般没有区别性,或者说修饰词的区别性不同于限制词的区别功能。     

面向半结构化数据的树逻辑及其性质研究

半结构化数据正以其灵活性而成为解决Internet环境下互操作语义层面问题的重要工具和网络数据交换格式的标准．从基础理论层面上对版结构化数据进行研究，在考察了进程代数和空间逻辑的有关结果后，从模型和逻辑系统的角度对半结构化数据特别是XML语言进行刻画．在[1]的基础上，在数据模型中加入了受限算子，并提出一种新的空间逻辑——树逻辑，在其中引入了一个新的模态算子，它们的意义在于能够对私有数据的性质进行刻画和表达．此外，通过修正数据模型中的同余关系，使得模型符合数据的有序性，从而使其更为合理．在此基础上证明了树逻辑系统公式可满足性的不可判定性，从而说明针对整个树逻辑系统的模型检测算法是不存在的．同时选择了其中一个子逻辑系统，给出了其模型检测算法，并证明了该算法的正确性．     

Agents and Lattice-valued Logic

In fuzzy set theory, instead of the underlying membership set being a two -valued set it is a multi-valued set that generally has the structure of a lattice L with a minimal element O and the maximal element I. Furthermore if ∧, ∨, → and ┐ are defined in the set L, then we can use these operations to define, as in the ordinary set theory, operations on fuzzy subsets. In this paper we give a model of the Lattice-Valued Logic with set of agents.Any agents know the logic value of a sentence p. The logic value is compatible with all of the accessible conceptual models or worlds of p inside the agent. Agent can be rational or irrational in the use of the logic operation.Every agent of n agents can have the same set of conceptual models for p and know the same logic for p in this case the agents form a consistent group of agents.When agents have different conceptual models for p,different subgroup of agents know different logic value for p. In this case the n agents are inconsistent in the expression of the logic value for p. The valuation structure of set of agents can be used as a semantic model for the Lattice-valued Logic and fuzzy logic.     

公用技术组合逻辑电路设计方法的初步探讨

通过最简逻辑函数,可以很简单的实现组合逻辑电路。但是利用最简逻辑函数实现的逻辑电路却不一定是最简的逻辑电路。本针对此问题提出公用技术组合逻辑电路设计方法这一新的逻辑电路设计方法来进行探讨。通过实例的分析证明了使用公用技术组合逻辑电路设计方法实现的逻辑电路比使用最简逻辑函数实现的逻辑电路更简单,从而提高了逻辑电路的性价比。     

可编程逻辑器件PLD及其开发

PLD是可以由用户在系统现场进行编程的逻辑器件.通过对器件编程使之实现所需要的逻辑功能,从而给数字电子系统设计带来了革命性的变化.讨论了可编程逻辑器件的发展及各类器件的特点,着重介绍了PLD器件的开发过程.     

A detection method for logic functions suitable for dual-logic synthesis

Logic functions can be implemented in either AND/OR/NOT-based traditional Boolean (TB) logic or AND/XOR-based Reed–Muller (RM) logic. To the majority of logic functions, it will be beneficial to be partially implemented in both TB logic and RM logic, called dual-logic. In this paper, a detection condition favoring dual-logic synthesis is proposed. A corresponding detection algorithm is developed and implemented in C. The algorithm is applied to test a set of MCNC91 benchmarks for verifying the algorithm. The results show that the proposed algorithm is more efficient than published ones.     

软件体系结构动态特征建模与验证

针对软件体系结构描述语言在分析、验证软件构架动态行为中的不足,采用谓词/变迁(Pr/T)网为软件体系结构动态行为建模,并提出了基于线性时序逻辑的软件体系结构动态行为模型验证方法.首先根据体系结构层次模型扩展Pr/T网建立体系结构动态行为模型(DFM)并构造DFM的可达图,然后使用基于自动机理论的方法来验证模型的时态逻辑性质,最后通过对一个电子商务系统实例的并发控制机制建模和模型检测,验证了该方法的有效性.所提方法结合了Pr/T网和线性时序逻辑的优点,为进一步开展软件体系结构动态行为的分析、验证奠定了基础.