Completeness and Counter-Example Generations of a Basic Protocol Logic: (Extended Abstract)

We give an axiomatic system in first-order predicate logic with equality for proving security protocols correct. Our axioms and inference rules derive the basic inference rules, which are explicitly or implicitly used in the literature of protocol logics, hence we call our axiomatic system Basic Protocol Logic (or BPL, for short). We give a formal semantics for BPL, and show the completeness theorem such that for any given query (which represents a correctness property) the query is provable iff it is true for any model. Moreover, as a corollary of our completeness proof, the decidability of provability in BPL holds for any given query. In our formal semantics we consider a “trace” any kind of sequence of primitive actions, counter-models (which are generated from an unprovable query) cannot be immediately regarded as realizable traces (i.e., attacked processes on the protocol in question). However, with the aid of Comon-Treinen's algorithm for the intruder deduction problem, we can determine whether there exists a realizable trace among formal counter-models, if any, generated by the proof-search method (used in our completeness proof). We also demonstrate that our method is useful for both proof construction and flaw analysis by using a simple example.     

On the Relative Soundness of the Free Algebra Model for Public Key Encryption

Formal systems for cryptographic protocol analysis typically model cryptosystems in terms of free algebras. Modeling the behavior of a cryptosystem in terms of rewrite rules is more expressive, however, and there are some attacks that can only be discovered when rewrite rules are used. But free algebras are more efficient, and appear to be sound for “most” protocols. In [J. Millen, “On the freedom of decryption”, Information Processing Letters 86 (6) (June 2003) 329–333] Millen formalizes this intuition for shared key cryptography and provides conditions under which it holds; that is, conditions under which security for a free algebra version of the protocol implies security of the version using rewrite rules. Moreover, these conditions fit well with accepted best practice for protocol design. However, he left public key cryptography as an open problem. In this paper, we show how Millen's approach can be extended to public key cryptography, giving conditions under which security for the free algebra model implies security for the rewrite rule model. As in the case for shared key cryptography, our conditions correspond to standard best practice for protocol design.     

网络安全协议的自动化设计策略

文章以演化计算为工具,以BAN逻辑为基本的推理准则,在第一阶段随机搜索候选协议,然后在第二阶段通过冗余协议约简方案得出优化的协议。两阶段设计方案可以自动生成各种需求的两方或三方通信协议,并且广泛支持各种加密方法。通过两阶段的生成和过滤,我们的方法可以实现较大规模网络安全协议的自动化设计,例如三方密钥分配协议等。     

智能电子商务采购协议*

影响智能电子商务能否得以真正实施的因素很多,其中一套完善的基于智能代理的电子商务协议至关重要。设计一套包括搜索、谈判和支付三个子协议的智能采购协议不仅满足了三个原子性、公平性和可追究性原则,而且具备了商务逻辑安全。解决了电子商务的效率和智能化问题。     

Exogenous Probabilistic Computation Tree Logic

We define a logic EpCTL for reasoning about the evolution of probabilistic systems. System states correspond to probability distributions over classical states and the system evolution is modelled by probabilistic Kripke structures that capture both stochastic and non–deterministic transitions. The proposed logic is a temporal enrichment of Exogenous Probabilistic Propositional Logic (EPPL). The model-checking problem for EpCTL is analysed and the logic is compared with PCTL; the semantics of the former is defined in terms of probability distributions over sets of propositional symbols, whereas the latter is designed for reasoning about distributions over paths of possible behaviour. The intended application of the logic is as a specification formalism for properties of communication protocols, and security protocols in particular; to demonstrate this, we specify relevant security properties for a classical contract signing protocol and for the so–called quantum one–time pad.     

基于同步数的轻量级高效RFID身份认证协议

RFID技术广泛应用的同时,其安全问题面临着严峻的考验。在确保安全性能的前提下,节省系统成本、提高效率成为未来研究重点。在分析各种协议缺陷之后,借鉴滚动码技术的同步数原理,提出了一种基于同步数的轻量级高效RFID身份认证协议。协议运用同步数以及双向认证机制保障系统安全性。对各种威胁进行分析,确保了协议的安全性。通过比较其他协议的效率与成本,可以看出该协议具有轻量级与高效性。最后运用BAN逻辑对协议进行了形式化分析,从理论上证明了本协议的可行性。     

读写器可移动的RFID高效认证协议

无线射频识别(RFID)对后端数据库的搜索效率低,且读写器的移动性差。针对该问题,基于ElGamal重加密算法,提出一种读写器可离线工作的RFID安全协议,利用GNY逻辑证明该协议的安全性。理论分析结果表明,其能抵抗重传攻击、去同步化攻击、假冒攻击、针对标签的隐私攻击,减少后端数据库的搜索次数,降低Hash计算量,提高执行效率。     

一种分析Timed-Release公钥协议的扩展逻辑

在Coffey和Saidha提出的CS逻辑(CS逻辑将时间与逻辑结构相结合，可用于形式化分析Timed-release公钥协议的时间相关性秘密的安全性)的基础上，提出了CS逻辑的扩展逻辑，它更好地反映了Timed-release公钥协议的特性，并对一个协议实例进行了有效的形式化分析．     

Partitioning knowledge bases between advanced notification and clinical decision support systems

Clinical decision support system (CDSS) and their logic syntax include the coding of notifications (e.g., Arden Syntax). The following paper will describe the rationale for segregating policies, user preferences and clinical monitoring rules into “advanced notification” and” clinical” components, which together form a novel and complex CDSS. Notification rules and hospital policies are respectively abstracted from care-provider roles and alerting mechanisms. User-defined preferences determine which devices are to be used for receiving notifications. Our design differs from previous notification systems because it integrates a versatile notification platform supporting a wide range of mobile devices with a XML/HL-7 compliant communication protocol.     

A game-theoretic framework for specification and verification of cryptographic protocols

We model security protocols as games using concepts of game semantics. Using this model we ascribe semantics to protocols written in the standard simple arrow notation. According to the semantics, a protocol is interpreted as a set of strategies over a game tree that represents the type of the protocol. The model uses abstract computation functions and message frames in order to model internal computations and knowledge of agents and the intruder. Moreover, in order to specify properties of the model, a logic that deals with games and strategies is developed. A tableau-based proof system is given for the logic, which can serve as a basis for a model checking algorithm. This approach allows us to model a wide range of security protocol types and verify different properties instead of using a variety of methods as is currently the practice. Furthermore, the analyzed protocols are specified using only the simple arrow notation heavily used by protocol designers and by practitioners.