Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks

We consider the problem of formal automatic verification of cryptographic protocols when some data, like poorly chosen passwords, can be guessed by dictionary attacks. First, we define a theory of these attacks and propose an inference system modeling the deduction capabilities of an intruder. This system extends a set of well-studied deduction rules for symmetric and public key encryption, often called Dolev–Yao rules, with the introduction of a probabilistic encryption operator and guessing abilities for the intruder. Then, we show that the intruder deduction problem in this extended model is decidable in PTIME. The proof is based on a locality lemma for our inference system. This first result yields to an NP decision procedure for the protocol insecurity problem in the presence of a passive intruder. In the active case, the same problem is proved to be NP-complete: we give a procedure for simultaneously solving symbolic constraints with variables that represent intruder deductions. We illustrate the procedure with examples of published protocols and compare our model to other recent formal definitions of dictionary attacks.     

Modelling and analysing cognitive causes of security breaches

In this paper we are concerned with security issues that arise in the interaction between user and system. We focus on cognitive processes that affect security of information flow from the user to the computer system and the resilience of the whole system to intruder attacks. For this, we extend our framework developed for the verification of usability properties by introducing two kinds of intruder models, an observer and an active intruder, with the associated security properties. Finally, we consider small examples to illustrate the ideas and approach. These examples demonstrate how our framework can be used (a) to detect confidentiality leaks, caused by a combination of an inappropriate design and certain aspects of human cognition, and (b) to identify designs more susceptible to cognitively based intruder attacks.     

Analysing the Vulnerability of Protocols to Produce Known-pair and Chosen-text Attacks

In this paper we report on an analysis for finding known-pair and chosen-text attacks in protocols. As these attacks are at the level of blocks, we extend the attacker by special capabilities related to block chaining techniques. The analysis is automated using Blanchet's protocol verifier and illustrated on two well-known protocols, the Needham-Schroeder-Lowe public-key protocol as well as the Needham-Schroeder symmetric-key protocol. On the first protocol, we show how the special intruder capabilities related to chaining may compromise the secrecy of nonces and that chosen- ciphertext attacks are possible. We propose two modified versions of the protocol which strengthen its security. We then illustrate known-pair and chosen-plaintext attacks on the second protocol.     

Model-Based Verification of a Security Protocol for Conditional Access to Services

We use the formal language LOTOS to specify and verify the robustness of the Equicrypt protocol under design in the European OKAPI project for conditional access to multimedia services. We state some desired security properties and formalize them. We describe a generic intruder process and its modelling, and show that some properties are falsified in the presence of this intruder. The diagnostic sequences can be used almost directly to exhibit the scenarios of possible attacks on the protocol. Finally, we propose an improvement of the protocol which satisfies our properties.     

Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol by Rewriting

This paper reports on work in progress on using rewriting techniques for the specification and the verification of communication protocols. As in Genet and Klay's approach to formalizing protocols, a rewrite system describes the steps of the protocol and an intruder's ability of decomposing and decrypting messages, and a tree automaton encodes the initial set of communication requests and an intruder's initial knowledge. In a previous work we have defined a rewriting strategy that, given a term t that represents a property of the protocol to be proved, suitably expands and reduces t using the rules in and the transitions in to derive whether or not t is recognized by an intruder. In this paper we present a formalization of the Needham-Schroeder symmetric-key protocol and use the rewriting strategy for deriving two well-known authentication attacks.     

一种无线认证密钥协商协议

提出一种新的无线局域网认证密钥协商协议,可以提供双方相互认证及密钥确认。该协议在密钥设置上基于挑战响应协议和KAS方案,在密钥预分配上基于Diffie—Hellman协议,可以提供完美前向安全性,抵抗被动攻击、字典攻击、中间人攻击、假冒攻击等。并对协议的计算代价和通信代价进行分析。     

移动ad hoc网络中DOS攻击及其防御机制

移动ad hoc网络由于其动态拓扑、无线信道以及各种资源有限的特点,特别容易遭受拒绝服务(DOS)攻击．提出了移动ad hoc网络中一种新的DOS攻击模型——ad hoc flooding攻击及其防御策略．该攻击主要针对移动ad hoc网络中的按需路由协议,如AODV,DSR等．ad hoc flooding攻击是通过在网络中泛洪发送超量路由查询报文及数据报文,大量地占用网络通信及节点资源,以至于阻塞节点正常的通信．分析ad hoc flooding攻击之后,提出了两种防御策略：其一是邻居阻止,即当入侵者发送大量路由查询报文时,邻居节点降低对其报文的处理优先级,直至不再接收其报文．其二是路径删除,即目标节点将入侵者发送攻击报文的路径删除,以阻止其继续发送攻击报文．模拟实验证实,通过这两种方法的结合．能够有效地阻止网络中的ad hoc flooding攻击行为．     

命题公式真值表的生成算法

真值表是命题逻辑理论中的一个重要概念,利用它可以求命题公式的主范式、判定命题公式的类型以及进行命题逻辑的推理等。本文给出了任意命题公式真值表的生成算法,为利用计算机解决命题逻辑中的其它问题奠定了基础.     

一种基于并发命题投影时序逻辑模型检测的入侵检测方法

基于投影时序逻辑模型检测的入侵检测方法具有描述网络入侵者分段攻击的能力,然而对并发攻击仍无能为力,因为该逻辑无法直接描述并发。针对此问题,在该逻辑的基础上定义了一种新的并发算子,并给出基于并发投影时序逻辑模型检测的入侵检测方法。对复杂攻击实例的检测表明,新方法可有效提高对并发攻击的检测能力。     

Propositional semantics for disjunctive logic programs

In this paper we study the properties of the class of head-cycle-free extended disjunctive logic programs (HEDLPs), which includes, as a special case, all nondisjunctive extended logic programs. We show that any propositional HEDLP can be mapped in polynomial time into a propositional theory such that each model of the latter corresponds to an answer set, as defined by stable model semantics, of the former. Using this mapping, we show that many queries over HEDLPs can be determined by solving propositional satisfiability problems. Our mapping has several important implications: It establishes the NP-completeness of this class of disjunctive logic programs; it allows existing algorithms and tractable subsets for the satisfiability problem to be used in logic programming; it facilitates evaluation of the expressive power of disjunctive logic programs; and it leads to the discovery of useful similarities between stable model semantics and Clark's predicate completion.     

基于时序逻辑的3种网络攻击建模

与其他检测方法相比,基于时序逻辑的入侵检测方法可以有效地检测许多复杂的网络攻击。然而,由于缺少网络攻击的时序逻辑公式, 该方法不能检测 出常见的back,ProcessTable以及Saint 3种攻击。因此,使用命题区间时序逻辑(ITL)和实时攻击签名逻辑(RASL)分别对这3种攻击建立时序逻辑公式。首先,分析这3种攻击的攻击原理;然后,将攻击的关键步骤分解为原子动作,并定义了原子命题;最后,根据原子命题之间的逻辑关系分别建立针对这3种攻击的时序逻辑公式。根据模型检测原理,所建立的时序逻辑公式可以作为模型检测器(即入侵检测器)的一个输入,用自动机为日志库建模,并将其作为模型检测器的另一个输入,模型检测的结果即为入侵检测的结果,从而给出了针对这3种攻击的入侵检测方法。     

基于同态的安全协议攻击及其形式化验证

介绍2种利用加密算法同态特性的安全协议攻击,定义安全协议项代数表示和基于角色行为序列的协议模型,提出一种基于角色行为实例交互的安全协议约束序列生成方法,应用等式理论将Dolev D等人提出的Dolev-Yao模型（IEEE Transactions on Information Theory,1983,第12期）进行扩展,设计攻击者一阶逻辑演绎系统,采用约束求解方法对NSL协议进行建模和形式化验证,发现基于“完美密码系统假设”无法验证的同态攻击。     

Wired and wireless intrusion detection system: Classifications, good characteristics and state-of-the-art

In computer and network security, standard approaches to intrusion detection and response attempt to detect and prevent individual attacks. Intrusion Detection System (IDS) and intrusion prevention systems (IPS) are real-time software for risk assessment by monitoring for suspicious activity at the network and system layer. Software scanner allows network administrator to audit the network for vulnerabilities and thus securing potential holes before attackers take advantage of them.

In this paper we try to define the intruder, types of intruders, detection behaviors, detection approaches and detection techniques. This paper presents a structural approach to the IDS by introducing a classification of IDS. It presents important features, advantages and disadvantages of each detection approach and the corresponding detection techniques. Furthermore, this paper introduces the wireless intrusion protection systems.

The goal of this paper is to place some characteristics of good IDS and examine the positioning of intrusion prevention as part of an overall layered security strategy and a review of evaluation criteria for identifying and selecting IDS and IPS. With this, we hope to introduce a good characteristic in order to improve the capabilities for early detection of distributed attacks in the preliminary phases against infrastructure and take a full spectrum of manual and automatic response actions against the source of attacks.     

Security enhancement of an IC-card-based remote login mechanism

Wang et al. presented a remote password authentication scheme using IC (Integrated Circuit) cards in 2004. Unfortunately, we discovered that their scheme is unable to withstand the forgery attack. We consequently propose in this paper a novel version to resist this kind of attacks. Furthermore, our scheme can also provide mutual authentication between a remote server and login users. The security of our scheme is based on the public one-way hash function. What is more, the timestamp mechanism is applied in our scheme to protect such potential attacks in the case that an intruder may replay a previously intercepted login request to access the remote server.     

Improving the quality of alerts and predicting intruder’s next goal with Hidden Colored Petri-Net

Intrusion detection systems (IDS) often provide poor quality alerts, which are insufficient to support rapid identification of ongoing attacks or predict an intruder’s next likely goal. In this paper, we propose a novel approach to alert postprocessing and correlation, the Hidden Colored Petri-Net (HCPN). Different from most other alert correlation methods, our approach treats the alert correlation problem as an inference problem rather than a filter problem. Our approach assumes that the intruder’s actions are unknown to the IDS and can be inferred only from the alerts generated by the IDS sensors. HCPN can describe the relationship between different steps carried out by intruders, model observations (alerts) and transitions (actions) separately, and associate each token element (system state) with a probability (or confidence). The model is an extension to Colored Petri-Net (CPN). It is so called “hidden” because the transitions (actions) are not directly observable but can be inferred by looking through the observations (alerts). These features make HCPN especially suitable for discovering intruders’ actions from their partial observations (alerts) and predicting intruders’ next goal. Our experiments on DARPA evaluation datasets and the attack scenarios from the Grand Challenge Problem (GCP) show that HCPN has promise as a way to reducing false positives and negatives, predicting intruder’s next possible action, uncovering intruders’ intrusion strategies after the attack scenario has happened, and providing confidence scores.     

Counting complexity of propositional abduction

Abduction is an important method of non-monotonic reasoning with many applications in artificial intelligence and related topics. In this paper, we concentrate on propositional abduction, where the background knowledge is given by a propositional formula. Decision problems of great interest are the existence and the relevance problems. The complexity of these decision problems has been systematically studied while the counting complexity of propositional abduction has remained obscure. The goal of this work is to provide a comprehensive analysis of the counting complexity of propositional abduction in various settings.     

An Immunity-based Security Architecture for Mobile Ad Hoc Networks

Mobile ad hoc network of lets convenient infrastructure less communication over the shared wireless channel. However, the nature of ad hoc networks makes them vulnerable to security attacks. Existing security technologies such as intrusion prevention and intrusion detection are passive in response to intrusions in that their countermeasures are only to protect the networks and there is no automated, network-wide counteraction against detected intrusions. While they all play an important role in counteracting intrusion, they do not, however, effectively address the root cause of the problem - intruders. In this paper, wc propose the architecture of automated intrusion response. When an intruder is found in our architecture, the block agents will get to the neighbor nodes of the intruder and formed a firewall to isolate the intruder. In the end, we illustrate our architecture by an example.     

SAT-Solving in Practice, with a Tutorial Example from Supervisory Control

Satisfiability solving, the problem of deciding whether the variables of a propositional formula can be assigned in such a way that the formula evaluates to true, is one of the classic problems in computer science. It is of theoretical interest because it is the canonical NP-complete problem. It is of practical interest because modern SAT-solvers can be used to solve many important and practical problems. In this tutorial paper, we show briefly how such SAT-solvers are implemented, and point to some typical applications of them. Our aim is to provide sufficient information (much of it through the reference list) to kick-start researchers from new fields wishing to apply SAT-solvers to their problems. Supervisory control theory originated within the control community and is a framework for reasoning about a plant to be controlled and a specification that the closed-loop system must fulfil. This paper aims to bridge the gap between the computer science community and the control community by illustrating how SAT-based techniques can be used to solve some supervisory control related problems.     

Boosting complete techniques thanks to local search methods

In this paper, an efficient heuristic allowing one to localize inconsistent kernels in propositional knowledge‐bases is described. Then, it is shown that local search techniques can boost the performance of logically complete methods for SAT. More precisely, local search techniques can be used to guide the branching strategy of logically complete techniques like Davis and Putnam's one, giving rise to significant performance improvements, in particular when addressing locally inconsistent problems. Moreover, this approach appears very competitive in the context of consistent SAT instances, too. This revised version was published online in June 2006 with corrections to the Cover Date.