CTL* model checking on a shared-memory architecture

In this article we present the parallelisation of an explicit-state CTL^* model checking algorithm for a virtual shared-memory high-performance parallel machine architecture. The algorithm uses a combination of private and shared data structures for implicit and dynamic load balancing with minimal synchronisation overhead. The performance of the algorithm and the impact that different design decisions have on the performance are analysed using both mathematical cost models and experimental results. The analysis shows not only the practicality and effective speedup of the algorithm, but also the main pitfalls of parallelising model checking for shared-memory architectures.

An Attack-Finding Algorithm for Security Protocols

This paper proposes an automatic attack construction algorithm in order to find potential attacks on ecurity protocols.It is based on a dynamic strand space model,which enhances the original strand space model by introducing active nodes on strands so as to characterize the dynamic procedure of protocol execution.With exact causal dependency relations between messages considered in the model,this algorithm can avoid state space explo-sion caused by asynchronous composition.In order to get a finite state space,a new method called strand-added on demand is exploited,which extends a bundle in an incremental manner without requiring explicit configuration of protocol execution parameters.A finer granularity model of term structure is also introduced, in which subterms are divided into check subterms and data subterms .Moreover,data subterms can be further classified based on the compatible data subterm relation to obtain automatically the finite set of valid acceptable terms for an honest principal.In this algorithm,terms core is designed to represent the intruder‘s knowledge compactly,and forward search technology is used to simulate attack patterns easily.Using this algorithm,a new attack on the Dolve-Yao protocol can be found,which is even more harmful beeause the secret is revealed before the session terminates.     

Improving state class constructions for CTL* model checking of time Petri nets

The state space explosion is still one of the most challenging problems in formal verification using enumerative techniques. The challenge is even greater for real time systems whose state spaces are generally infinite due to time density. To use enumerative techniques with these systems, their state spaces need to be contracted into finite structures that preserve properties of interest. We propose in this paper an efficient approach to construct a contraction of the time Petri net model state space, which preserves its CTL* properties.     

A tableau-based decision procedure for CTL*

We present a sound, complete and implementable tableau method for deciding satisfiability of formulas in the propositional version of computation tree logic CTL*. This is the first such tableau. CTL* is an exceptionally important temporal logic with applications from hardware design to agent reasoning, but there is no easily automated reasoning approach to CTL*. The tableau here is a traditional tree-shaped or top-down style tableau, and affords the possibility of reasonably quick decisions on the satisfiability of medium-sized formulas and construction of small models for them. A straightforward subroutine is given for determining when looping allows successful branch termination, but much needed further development is left as future work. In particular, a more general repetition prevention mechanism is needed to speed up the task of tableau construction.     

A specialized on-the-fly algorithm for lexicon and language model composition

This paper presents an algorithm for the composition of weighted finite-state transducers which is specially tailored to speech recognition applications: it composes the lexicon with the language model while simultaneously optimizing the resulting transducer. Furthermore, it performs these computations "on-the-fly" to allow easier management of the tradeoff between offline and online computation and memory. The algorithm is exact for local knowledge integration and optimization operations such as composition and determinization. Minimization and pushing operations are approximated. Our results have confirmed the efficiency of these approximations.     

安全协议状态空间的束动作偏序约简算法*

目前安全协议分析的偏序归约算法较为复杂、不易实现,限制了其适用范围,且以动作为基础,粒度较小,对减少状态空间的作用有限。针对该问题提出了一种束动作偏序约简算法,将同一会话中的动作序列看做一个束动作,根据攻击者截获的消息与攻击者知识集间的关系,判断迹等价的束动作迁移所到达的后继状态是否为冗余节点,以约简状态空间。该算法思想简单、易于实现;实例表明它有效地约简了安全协议的状态空间。     

可能性测度下的CTL符号化模型检测

随着系统复杂性的增加,系统中的不确定信息亟待处理,状态爆炸问题也越来越严峻,现有的模型检测技术已不能完全适用于复杂系统的验证。 对可能性测度下CTL符号化模型检测进行了研究。首先用多终端二值决策图和布尔公式分别描述系统模型和待验证性质,然后再对系统模型进行归一化和简化,最后利用不动点计算完成系统验证。该研究是对可能性测度下的模型检测技术和符号化模型检测技术的整合,不但能处理系统的不确定信息,而且保持了符号化模型检测对计算时空要求低的优点,对于复杂系统模型检测具有重要意义。     

A formal approach for checking security properties in SecSpaces

SecSpaces is a Linda-like coordination model whose aim is to provide a support for secure coordination in Open System applications. Substantially it provides a methodology to restrict the access to the objects stored in the shared dataspace. In this paper we introduce a formal language for representing systems interacting via SecSpaces primitives and its operational semantics. Moreover in this context we consider a notion of observational equivalence, namely testing equivalence. In order to evaluate the adequacy of the model for limiting the access to the shared dataspace, we present some examples of interaction protocols that can be used to obtain some security properties (e.g., authentication or privacy of a datum).     

OFMC: A symbolic model checker for security protocols

We present the on-the-fly model checker OFMC, a tool that combines two ideas for analyzing security protocols based on lazy, demand-driven search. The first is the use of lazy data types as a simple way of building efficient on-the-fly model checkers for protocols with very large, or even infinite, state spaces. The second is the integration of symbolic techniques and optimizations for modeling a lazy Dolev–Yao intruder whose actions are generated in a demand-driven way. We present both techniques, along with optimizations and proofs of correctness and completeness.Our tool is state of the art in terms of both coverage and performance. For example, it finds all known attacks and discovers a new one in a test suite of 38 protocols from the Clark/Jacob library in a few seconds of CPU time for the entire suite. We also give examples demonstrating how our tool scales to, and finds errors in, large industrial-strength protocols.     

Parameterized model checking for security policy analysis

International Journal on Software Tools for Technology Transfer - We explain how a parameterized model checking technique can be exploited to mechanize the analysis of access control policies. The...     

A quadratic-time DBM-based successor algorithm for checking timed automata

Most of the timed automaton model checking algorithms explore state spaces by enumeration of time zones. The data structure called Difference Bound Matrix (DBM) is widely adopted to represent time zones because of its efficiency and simplicity. In this paper, we first present a quadratic-time algorithm to compute the canonical form of the conjunction of a canonical DBM and a time guard or a location invariant. Based on this algorithm, we present a quadratic-time DBM-based successor algorithm for timed automaton model checking.     

基于Prolog的安全协议在线自动化分析

基于串空间理论和约束消减方法,提出安全协议可达性分析模型;采用Prolog实现模型自动推理,利用XSB的Java接口实现基于Web的自动分析工具。     

基于BSP树的启发式阴影生成算法

阴影的生成在虚拟现实领域一直是个难题,特别是针对动态光源的大规模场景,目前还没有较成熟的阴影算法。通过对现有阴影生成算法和场景组织算法的研究,该文提出了基于二维空间分割树(BSP树)的启发式阴影生成算法:首先创建场景BSP树,随着观察者视点的改变,选取视剪裁体内的节点创建以光源为视点的遮挡体BSP树,然后通过对该BSP树的遍历拣选出阴影启发区内的物体,经过处理后BSP树只留下一些生成阴影必要的多边形大大减少了计算量,最后能够快速生成阴影。     

改进的安全协议一阶逻辑模型

由于Blanchet安全协议一阶逻辑模型不能够给出易于理解的攻击序列,基于该安全协议一阶逻辑模型,对逻辑推理中的规则及合一化操作进行了分类,给出了操作置换规则,明确了改进系统中的一些关键性概念和命题。最后,以化简的Needham-Schroeder协议为例,对秘密性进行形式化验证,结果表明改进的系统能够给出易于理解的攻击序列。     

一种基于状态扩展的安全协议验证机制

基于模型检测验证协议的方法存在状态空间爆炸问题,其中基于目标绑定搜索状态空间的方法有效控制了状态空间,但不能完全给出协议的运行情况。针对这一问题,提出了一种基于状态扩展的安全协议自动化验证机制,首先对协议状态进行初始搜索,给出协议运行需要的事件,得到协议基本状态,然后进行扩展搜索,考虑基本状态与其他协议运行的关系,形成协议扩展状态。该机制能够有效反映出协议的运行情况,且能够同时对多种安全性质进行验证。