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.     

一个安全、原子的电子商务协议及其形式化验证

电子商务的普及与接受主要取决于下述属性的解决：安全、原子、隐私与匿名,形式化描述和分析是描述电子商务协议并验证它各性的有效方法,面向物理商品交易的电子商务协议需要具备３个属性：安全、原子和隐私,介绍了一个安全、可靠的电子商务协议ＢＥＡＲＣＡＴ及其形式化描述,并龙有人侵者的情况下,通过用ＢＡＮ类型的逻辑证明所期望的属性的方式对协议的强度和正确性作形式化分析。     

Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures

Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication, abstract encryption/decryption. In this report we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions.     

电子商务的安全和原子：模型、协议和验证

电子商务的流行与接受主要取决于下述属性：安全、原子、隐私与匿名．对于需要安全、原子和隐私等3个属性的物理商品的电子交易还没有合适的电子商务协议．基于此,提出了一个称为ELC的电子商务模型,ELC模型模拟了国际贸易中的电子信用证．然后提出了一个安全、原子的电子商务协议．最后,在有一个入侵者的情况下,通过使用BAN风格的逻辑证明所期望的属性分析了协议的强度和正确性     

Attacking Group Multicast Key Management Protocols Using Coral

This paper describes the modelling of a two multicast group key management protocols in a firstorder inductive model, and the discovery of previously unknown attacks on them by the automated inductive counterexample finder Coral. These kinds of protocols had not been analysed in a scenario with an active intruder before. Coral proved to be a suitable tool for a job because, unlike most automated tools for discovering attacks, it deals directly with an open-ended model where the number of agents and the roles they play are unbounded. Additionally, Coral's model allows us to reason explicitly about lists of terms in a message, which proved to be essential for modelling the second protocol. In the course of the case studies, we also discuss other issues surrounding multicast protocol analysis, including identifying the goals of the protocol with respect to the intended trust model, modelling of the control conditions, which are considerably more complex than for standard two and three party protocols, and effective searching of the state space generated by the model, which has a much larger branching rate than for standard protocols.     

Reducing Protocol Analysis with XOR to the XOR-Free Case in the Horn Theory Based Approach

In the Horn theory based approach for cryptographic protocol analysis, cryptographic protocols and (Dolev?CYao) intruders are modeled by Horn theories and security analysis boils down to solving the derivation problem for Horn theories. This approach and the tools based on this approach, including ProVerif, have been very successful in the automatic analysis of cryptographic protocols. However, dealing with the algebraic properties of operators, such as the exclusive OR (XOR), which are frequently used in cryptographic protocols has been problematic. In particular, ProVerif cannot deal with XOR. In this paper, we show how to reduce the derivation problem for Horn theories with XOR to the XOR-free case. Our reduction works for an expressive class of Horn theories. A large class of intruder capabilities and protocols that employ the XOR operator can be modeled by these theories. Our reduction allows us to carry out protocol analysis using tools, such as ProVerif, that cannot deal with XOR, but are very efficient in the XOR-free case. We implemented our reduction and, in combination with ProVerif, used it for the fully automatic analysis of several protocols that employ the XOR operator. Among others, our analysis revealed a new attack on an IBM security module.     

Low-cost and reliable mutual anonymity protocols in peer-to-peer networks

We present several protocols to achieve mutual communication anonymity between an information requester and a provider in a P2P information-sharing environment, such that neither the requester nor the provider can identify each other, and no other peers can identify the two communicating parties with certainty. Most existing solutions achieve mutual anonymity in pure P2P systems without any trusted central controls. Compared with two such representative ones, our protocols improve efficiency in two different ways. First, utilizing trusted third parties and aiming at both reliability and low-cost, we propose a group of mutual anonymity protocols. We show that with some limited central support, our protocols can accomplish the goals of anonymity, efficiency, and reliability. Second, we propose a mutual anonymity protocol which relies solely on self-organizations among peers without any trusted central controls. In this protocol, the returning path can be shorter than the requesting path. This protocol does not need to broadcast the requested file back to the requester so that the bandwidth is saved and efficiency is improved. In addition, this protocol does not need special nodes to keep indices of sharing files, thus eliminating the index maintenance overhead and the potential for inconsistency between index records and peer file contents. We have evaluated our techniques in a browser-sharing environment. We show that the average increase in response time caused by our protocols is negligible, and these protocols show advantages over existing protocols in a P2P system.     

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

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

An Analysis Study on Zone-Based Anonymous Communication in Mobile Ad Hoc Networks

A zone-based anonymous positioning routing protocol for ad hoc networks, enabling anonymity of both source and destination, is proposed and analyzed. According to the proposed algorithm, a source sends data to an anonymity zone, where the destination node and a number of other nodes are located. The data is then flooded within the anonymity zone so that a tracer is not able to determine the actual destination node. Source anonymity is also enabled because the positioning routing algorithms do not require the source ID or its position for the correct routing. We develop anonymity protocols for both routeless and route-based data delivery algorithms. To evaluate anonymity, we propose a "measure of anonymity," and we develop an analytical model to evaluate it. By using this model, we perform an extensive analysis of the anonymity protocols to determine the parameters that most impact the anonymity level.     

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.     

基于树语言逼近的安全协议形式化分析

利用形式化方法或工具自动化分析实用安全协议十分必要,定理证明技术因其可解决无限状态系统的验证备受关注,但扩展其验证规模和自动化实现时仍然存在一些局限性。以定理证明和重写逼近理论为基础,以项重写形式化定义协议模型,以树自动机模拟协议攻击者知识集,给出攻击者知识集可达项逼近求解的算法,并根据上述模型讨论秘密性和认证性的验证方法,最后以Needham-Schroeder公钥认证协议为例验证模型的有效性,并指出下一步研究方向。     

Security by typing

We present an approach for analyzing cryptographic protocols that are subject to attack from an active intruder who takes advantage of knowledge of the protocol rules. The approach uses a form of type system in which types are communication steps and typing constraints characterize all the messages available to the intruder. This reduces verification of authentication and secrecy properties to a typing problem in our type system. We present the typing rules, prove soundness of a type inference algorithm, and establish the correctness of the typing rules with respect to the protocol execution and intruder actions. The protocol specifications used in the approach can be automatically extracted from the conventional, informal cryptographic protocol notation commonly found in the literature. To validate the approach, we implement our algorithm in a tool called DYMNA, which is a practical and efficient environment for the specification and analysis of cryptographic protocols.     

A novel electronic cash system with trustee-based anonymity revocation from pairing

Untraceable electronic cash is an attractive payment tool for electronic-commerce because its anonymity property can ensure the privacy of payers. However, this anonymity property is easily abused by criminals. In this paper, several recent untraceable e-cash systems are examined. Most of these provide identity revealing only when the e-cash is double spent. Only two of these systems can disclose the identity whenever there is a need, and only these two systems can prevent crime. We propose a novel e-cash system based on identity-based bilinear pairing to create an anonymity revocation function. We construct an identity-based blind signature scheme, in which a bank can blindly sign on a message containing a trustee-approved token that includes the user’s identity. On demand, the trustee can disclose the identity for e-cash using only one symmetric operation. Our scheme is the first attempt to incorporate mutual authentication and key agreement into e-cash protocols. This allows the proposed system to attain improvement in communication efficiency when compared to previous works.     

Automated anonymity verification of the ThreeBallot and VAV voting systems

In recent years, a large number of secure voting protocols have been proposed in the literature. Often these protocols contain flaws, but because they are complex protocols, rigorous formal analysis has proven hard to come by. Rivest’s ThreeBallot and Vote/Anti-Vote/Vote (VAV) voting systems are important because they aim to provide security (voter anonymity and voter verifiability) without requiring cryptography. In this paper, we construct CSP models of ThreeBallot and VAV, and use them to produce the first automated formal analysis of their anonymity properties. Along the way, we discover that one of the crucial assumptions under which ThreeBallot and VAV (and many other voting systems) operate—the short ballot assumption—is highly ambiguous in the literature. We give various plausible precise interpretations and discover that in each case, the interpretation either is unrealistically strong or else fails to ensure anonymity. We give a revised version of the short ballot assumption for ThreeBallot and VAV that is realistic but still provides a guarantee of anonymity.     

Probabilistic and nondeterministic aspects of anonymity

The concept of anonymity comes into play in a wide range of situations, varying from voting and anonymous donations to postings on bulletin boards and sending emails. The protocols for ensuring anonymity often use random mechanisms which can be described probabilistically, while the agents’ behavior may be totally unpredictable, irregular, and hence expressible only nondeterministically. Formal definitions of the concept of anonymity have been investigated in the past either in a totally nondeterministic framework, or in a purely probabilistic one. In this paper, we investigate a notion of anonymity which combines both probability and nondeterminism, and which is suitable for describing the most general situation in which the protocol and the users can have both probabilistic and nondeterministic behavior. We also investigate the properties of the definition for the particular cases of purely nondeterministic users and purely probabilistic users. We formulate the notions of anonymity in terms of probabilistic automata, and we describe protocols and users as processes in the probabilistic π-calculus, whose semantics is again based on probabilistic automata. Throughout the paper, we illustrate our ideas by using the example of the dining cryptographers.     

一种基于智能卡的匿名公平移动支付系统

提出了一种基于智能卡的匿名公平移动支付系统模型,基于该模型提出了一个可追踪匿名的脱线式数字现金协议,它使用智能卡作为分布匿名代理,实现了数字现金的动态匿名和兑零的功能;证明了匿名数字现金满足安全性和可追踪匿名性,该协议的效率高于基于盲签名和匿名代理服务器技术的协议.提出了一个关于时间敏感商品的公平移动支付方案,即使用智...     

移动自组网的匿名路由协议研究综述

移动自组网中的恶意节点对路由协议的安全和隐匿具有严重威胁.现在针对安全路由协议的研究很多,但是很少有人涉及匿名性问题,匿名路由协议能够实现节点身份、位置和通信关系的隐匿,在军事和其它机密通信领域中具有重要意义.首先对匿名路由协议面临的攻击行为进行分析,介绍其定义、分类和匿名性评价方法,然后概括性的介绍已有的典型匿名路由协议,比较其匿名性和安全性,最后对以后研究的问题和方向作了总结和展望.     

Verifying anonymity in voting systems using CSP

We present formal definitions of anonymity properties for voting protocols using the process algebra CSP. We analyse a number of anonymity definitions, and give formal definitions for strong and weak anonymity, highlighting the difference between these definitions. We show that the strong anonymity definition is too strong for practical purposes; the weak anonymity definition, however, turns out to be ideal for analysing voting systems. Two case studies are presented to demonstrate the usefulness of the formal definitions: a conventional voting system, and Prêt à Voter, a paper-based, voter-verifiable scheme. In each case, we give a CSP model of the system, and analyse it against our anonymity definitions by specification checks using the Failures-Divergences Refinement (FDR2) model checker. We give a detailed discussion on the results from the analysis, emphasizing the assumptions that we made in our model as well as the challenges in modelling electronic voting systems using CSP.     

On the efficiency of user identification: a system-based approach

In the Internet era, users’ fundamental privacy and anonymity rights have received significant research and regulatory attention. This is not only a result of the exponential growth of data that users generate when accomplishing their daily task by means of computing devices with advanced capabilities, but also because of inherent data properties that allow them to be linked with a real or soft identity. Service providers exploit these facts for user monitoring and identification, albeit impacting users’ anonymity, based mainly on personal identifiable information or on sensors that generate unique data to provide personalized services. In this paper, we report on the feasibility of user identification using general system features like memory, CPU and network data, as provided by the underlying operating system. We provide a general framework based on supervised machine learning algorithms both for distinguishing users and informing them about their anonymity exposure. We conduct a series of experiments to collect trial datasets for users’ engagement on a shared computing platform. We evaluate various well-known classifiers in terms of their effectiveness in distinguishing users, and we perform a sensitivity analysis of their configuration setup to discover optimal settings under diverse conditions. Furthermore, we examine the bounds of sampling data to eliminate the chances of user identification and thus promote anonymity. Overall results show that under certain configurations users’ anonymity can be preserved, while in other cases users’ identification can be inferred with high accuracy, without relying on personal identifiable information.