Search

We present StatVerif, which is an extension of the ProVerif process calculus with constructs for explicit state, in order to be able to reason about protocols that manipulate global state. Global state is required by protocols used in hardware devices (such as smart cards and the trusted platform module), as well as by protocols involving databases that store persistent information. We provide the operational semantics of StatVerif. We extend the ProVerif compiler to a compiler for StatVerif, which takes processes written in the extended process language and produces Horn clauses. Our compilation is carefully engineered to avoid many false attacks. We prove the correctness of the StatVerif compiler. We illustrate our method on two examples: a small hardware security device and a contract signing protocol. We are able to prove their desired properties automatically. [ABSTRACT FROM AUTHOR]

We take a model-theoretic viewpoint on security goals and how to establish them. The models are (possibly fragmentary) executions. Security goals such as authentication and confidentiality are geometric sequents, i.e. implications Φ→Ψ where Φ and Ψ are built from atomic formulas without negations, implications, or universal quantifiers.Security goals are then statements about homomorphisms, where the source is a minimal (fragmentary) model of the antecedent Φ. If every homomorphism to a non-fragmentary, complete execution factors through a model in which Ψ is satisfied, then the goal is achieved. One can validate security goals via a process of information enrichment. We call this approach enrich-by-need protocol analysis.This idea also clarifies protocol transformation. A protocol transformation preserves security goals when it preserves the form of the information enrichment process. We formalize this idea using simulation relations between labeled transition systems. These labeled transition systems formalize the analysis of the protocols, i.e. the information enrichment process, not the execution behavior of the protocols. [ABSTRACT FROM AUTHOR]

We present a new type system for verifying the security of reference implementations of cryptographic protocols written in a core functional programming language. The type system combines prior work on refinement types, with union, intersection, and polymorphic types, and with the novel ability to reason statically about the disjointness of types. The increased expressivity enables the analysis of important protocol classes that were previously out of scope for the type-based analyses of reference protocol implementations. In particular, our types can statically characterize: (i) more usages of asymmetric cryptography, such as signatures of private data and encryptions of authenticated data; (ii) authenticity and integrity properties achieved by showing knowledge of secret data; (iii) applications based on zero-knowledge proofs. The type system comes with a mechanized proof of correctness and an efficient type-checker. [ABSTRACT FROM AUTHOR]

In this paper, we analyse the Transport Layer Security (TLS) protocol (in particular, bilateral TLS in public-key mode) within the strand spaces setting. In Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW), IEEE Computer Society, 2003, pp. 141-154, Broadfoot and Lowe suggested an abstraction of TLS. The abstraction models the security services that appear to be provided by the protocol to the high-level security layers. The outcome of our analysis provides a formalisation of the security services provided by TLS and proves that, under reasonable assumptions, the abstract model suggested by Broadfoot and Lowe is correct. To that end, we reduce the complexity of the protocol using fault-preserving simplifying transformations. We extend the strand spaces model in order to include the cryptographic operations used in TLS and facilitate its analysis. Finally, we use the extended strand spaces model to fully analyse the public-key mode of bilateral TLS with its two main components: the Handshake and Record Layer protocols. [ABSTRACT FROM AUTHOR]

Protocol authentication properties are generally trace-based, meaning that authentication holds for the protocol if authentication holds for individual traces (runs of the protocol and adversary). Computational secrecy conditions, on the other hand, often are not trace based: the ability to computationally distinguish a system that transmits a secret from one that does not is measured by overall success on the set of all traces of each system. Non-trace-based properties present a challenge for inductive or compositional methods: induction is a natural way of reasoning about traces of a system, but it does not appear directly applicable to non-trace properties. We therefore investigate the semantic connection between trace properties that could be established by induction and non-trace-based security requirements. Specifically, we prove that a certain trace property implies computational secrecy and authentication properties, assuming the encryption scheme provides chosen ciphertext security and ciphertext integrity. We also prove a similar theorem for computational secrecy assuming Decisional Diffie–Hellman and a chosen plaintext secure encryption scheme. [ABSTRACT FROM AUTHOR]

First-order logic models of security for cryptographic protocols, based on variants of the Dolev–Yao model, are now well-established tools. Given that we have checked a given security protocol π using a given first-order prover, how hard is it to extract a formally checkable proof of it, as required in, e.g., common criteria at the highest evaluation level (EAL7)? We demonstrate that this is surprisingly hard in the general case: the problem is non-recursive. Nonetheless, we show that we can instead extract finite models M from a set S of clauses representing π, automatically, and give two ways of doing so. We then define a model-checker testing M |= S, and show how we can instrument it to output a formally checkable proof, e.g., in Coq. Experience on a number of protocols shows that this is practical, and that even complex (secure) protocols modulo equational theories have small finite models, making our approach suitable. [ABSTRACT FROM AUTHOR]

We introduce constraint differentiation, a powerful technique for reducing search when model-checking security protocols using constraint-based methods. Constraint differentiation works by eliminating certain kinds of redundancies that arise in the search space when using constraints to represent and manipulate the messages that may be sent by an active intruder. We define constraint differentiation in a general way, independent of the technical and conceptual details of the underlying constraint-based method and protocol model. Formally, we prove that constraint differentiation terminates and is correct, under the assumption that the original constraint-based approach has these properties. Practically, as a concrete case study, we have integrated this technique into OFMC, a state-of-the-art model-checker for security protocol analysis, and demonstrated its effectiveness by extensive experimentation. Our results show that constraint differentiation substantially reduces search and considerably improves the performance of OFMC, enabling its application to a wider class of problems. [ABSTRACT FROM AUTHOR]

A type flaw attack on a security protocol is an attack where an honest principal is cheated on interpreting a field in a message as the one with a type other than the intended one. In this paper, we shall present an extension of the LYSA calculus to cope with types, by using tags to represent the intended types of terms. We develop a Control Flow Analysis for this calculus which soundly over-approximates all the possible behaviour of a protocol and, in particular, is able to capture any type confusion that may occur during the protocol execution. The analysis acts in a descriptive way: it describes which violations may occur. In the same setting, our approach also offers a prescriptive usage: we can impose a type discipline, by forcing some data to be of the expected types. At this point, the analysis may statically check that type violations are not possible any longer. In other words, we instrument the code with the only checks necessary to enforce type security. Finally, we apply our framework to a multi-protocol setting, where the risk of having type flaw attacks is higher. Our analysis has been implemented and successfully applied to a number of security protocols, showing it is able to capture type flaw attacks. The implementation complexity of the analysis is low polynomial. [ABSTRACT FROM AUTHOR]

The secrecy problem for security protocols is the problem to decide whether or not a given security protocol has leaky runs. In this paper, the (initial) secrecy problem for bounded protocols with freshness check is shown to be NEXPTIME-complete. Relating the formalism in this paper to the multiset rewriting (MSR) formalism we obtain that the initial secrecy problem for protocols in restricted form, with bounded length messages, bounded existentials, with or without disequality tests, and an intruder with no existentials, is NEXPTIME-complete. If existentials for the intruder are allowed but disequality tests are not allowed, the initial secrecy problem still is NEXPTIME-complete. However, if both existentials for the intruder and disequality tests are allowed and the protocols are not well-founded (and, therefore, not in restricted form), then the problem is undecidable. These results also correct some wrong statements in Durgin et al., JCS 12 (2004), 247–311. [ABSTRACT FROM AUTHOR]

We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol, where timing information allows the study of different attack scenarios. We model check the protocols using UPPAAL. Further, a taxonomy is obtained by studying and categorising protocols from the well known Clark Jacob library and the Security Protocol Open Repository (SPORE) library. Finally, we present some new challenges and threats that arise when considering time in the analysis, by providing a novel protocol that uses time challenges and exposing a timing attack over an implementation of an existing security protocol. [ABSTRACT FROM AUTHOR]

Selfish behavior at the Medium Access (MAC) Layer can have devastating side effects on the performance of wireless networks, with effects similar to those of Denial of Service (DoS) attacks. In this paper we consider the problem of detection and prevention of node misbehavior at the MAC layer, focusing on the back-off manipulation by selfish nodes. We first propose an algorithm that ensures honest behavior of non-colluding participants. Furthermore, we analyze the problem of colluding selfish nodes, casting the problem within a minimax robust detection framework and providing an optimal detection rule for the worst-case attack scenarios. Finally, we evaluate the performance of single and colluding attackers in terms of detection delay. Although our approach is general and can be used with any probabilistic distributed MAC protocol, we focus our analysis on the IEEE 802.11 MAC. [ABSTRACT FROM AUTHOR]

We present three case studies, investigating the use of probabilistic model checking to automatically analyse properties of probabilistic contract signing protocols. We use the probabilistic model checker PRISM to analyse three protocols: Rabin's probabilistic protocol for fair commitment exchange; the probabilistic contract signing protocol of Ben-Or, Goldreich, Micali, and Rivest; and a randomised protocol for signing contracts of Even, Goldreich, and Lempel. These case studies illustrate the general methodology for applying probabilistic model checking to formal verification of probabilistic security protocols. For the Ben-Or et al. protocol, we demonstrate the difficulty of combining fairness with timeliness. If, as required by timeliness, the judge responds to participants' messages immediately upon receiving them, then there exists a strategy for a misbehaving participant that brings the protocol to an unfair state with arbitrarily high probability, unless unusually strong assumptions are made about the quality of the communication channels between the judge and honest participants. We quantify the tradeoffs involved in the attack strategy, and discuss possible modifications of the protocol that ensure both fairness and timeliness. For the Even et al. protocol, we demonstrate that the responder enjoys a distinct advantage. With probability 1, the protocol reaches a state in which the responder possesses the initiator's commitment, but the initiator does not possess the responder's commitment. We then analyse several variants of the protocol, exploring the tradeoff between fairness and the number of messages that must be exchanged between participants. [ABSTRACT FROM AUTHOR]

The A-GDH.2 and SA-GDH.2 authenticated group key agreement protocols showed to be flawed in 2001. Even though the corresponding attacks (or some variants of them) have been rediscovered in several different frameworks, no fixed version of these protocols has been proposed until now. In this paper, we prove that it is in fact impossible to design a scalable authenticated group key agreement protocol based on the same design assumptions as the A-GDH ones. We proceed by providing a systematic way to derive an attack against any A-GDH-type protocol with at least four participants and exhibit protocols with two and three participants which we cannot break using our technique. As far as we know, this is the first generic insecurity result reported in the literature concerning authentication protocols. [ABSTRACT FROM AUTHOR]

There has been concern over the apparent conflict between privacy and data mining. There is no inherent conflict, as most types of data mining produce summary results that do not reveal information about individuals. The process of data mining may use private data, leading to the potential for privacy breaches. Secure Multiparty Computation shows that results can be produced without revealing the data used to generate them. The problem is that general techniques for secure multiparty computation do not scale to data-mining size computations. This paper presents an efficient protocol for securely determining the size of set intersection, and shows how this can be used to generate association rules where multiple parties have different (and private) information about the same set of individuals. [ABSTRACT FROM AUTHOR]

Many authentication and key exchange protocols are built using an accepted set of standard concepts such as Diffie–Hellman key exchange, nonces to avoid replay, certificates from an accepted authority, and encrypted or signed messages. We propose a general framework for deriving security protocols from simple components, using composition, refinements, and transformations. As a case study, we examine the structure of a family of key exchange protocols that includes Station-To-Station (STS), ISO-9798-3, Just Fast Keying (JFK), IKE and related protocols, deriving all members of the family from two basic protocols. In order to associate formal proofs with protocol derivations, we extend our previous security protocol logic with preconditions, temporal assertions, composition rules, and several other improvements. Using the logic, which we prove is sound with respect to the standard symbolic model of protocol execution and attack (the “Dolev–Yao model”), the security properties of the standard signature based Challenge-Response protocol and the Diffie–Hellman key exchange protocol are established. The ISO-9798-3 protocol is then proved correct by composing the correctness proofs of these two simple protocols. Although our current formal logic is not sufficient to modularly prove security for all of our current protocol derivations, the derivation system provides a framework for further improvements. [ABSTRACT FROM AUTHOR]

Non‐interference has been advocated by various authors as a uniform framework for the formal specification of security properties in cryptographic protocols. Unfortunately, specifications based on non‐interference are often non‐effective, as they require protocol analyses in the presence of all possible intruders. This paper develops new characterizations of non‐interference that rely on a finitary representation of intruders. These characterizations draw on equivalence relations built on top of labelled transition systems in which the presence of intruders is accounted for, indirectly, in terms of their (the intruders') knowledge of the protocols' initial data. The new characterizations apply uniformly to trace and bisimulation non‐interference, yielding proof techniques for the analysis of various security properties. We demonstrate the effectiveness of such techniques in the analysis of different properties of a fair exchange protocol. [ABSTRACT FROM AUTHOR]

When formalizing security protocols, different specification languages support very different reasoning methodologies, whose results are not directly or easily comparable. Therefore, establishing clear mappings among different frameworks is highly desirable, as it permits various methodologies to cooperate by interpreting theoretical and practical results of one system into another. In this paper, we examine the relationship between two general verification frameworks: multiset rewriting (MSR) and a process algebra (PA) inspired to CCS and the π‐calculus. Although defining a simple and general bijection between MSR and PA appears difficult, we show that the sublanguages needed to specify cryptographic protocols admit an effective translation that is not only trace‐preserving, but also induces a correspondence relation between the two languages. In particular, the correspondence sketched in this paper permits transferring several important trace‐based properties such as secrecy and many forms of authentication. [ABSTRACT FROM AUTHOR]

An important problem in the analysis of security protocols is that of checking whether a protocol preserves secrecy, i.e., no secret owned by the honest agents is unintentionally revealed to the intruder. This problem has been proved to be undecidable in several settings. In particular, Durgin et al. prove the undecidability of the secrecy problem in the presence of an unbounded set of nonces, even when the message length is bounded. In this paper we prove that even in the presence of an unbounded set of nonces the secrecy problem is decidable for a reasonable subclass of protocols, which we call context‐explicit protocols. [ABSTRACT FROM AUTHOR]

Dolev and Yao initiated an approach to studying cryptographic protocols which abstracts from possible problems with the cryptography so as to focus on the structural aspects of the protocol. Recent work in this framework has developed easily applicable methods to determine many security properties of protocols. A separate line of work, initiated by Bellare and Rogaway, analyzes the way specific cryptographic primitives are used in protocols. It gives asymptotic bounds on the risk of failures of secrecy or authentication. In this paper we show how the Dolev–Yao model may be used for protocol analysis, while a further analysis gives a quantitative bound on the extent to which real cryptographic primitives may diverge from the idealized model. We illustrate this method where the cryptographic primitives are based on Carter–Wegman universal classes of hash functions. This choice allows us to give specific quantitative bounds rather than simply asymptotic bounds. [ABSTRACT FROM AUTHOR]

We propose a formal model of rational exchange and exchange protocols in general, which is based on game theory. In this model, an exchange protocol is represented as a set of strategies in a game that is played by the protocol parties and the network that they use to communicate with each other. Within this model, we give a formal definition for rational exchange and various other properties of exchange protocols, including fairness. In particular, rational exchange is defined in terms of a Nash equilibrium in the protocol game. We also study the relationship between rational and fair exchange, and prove that fairness implies rationality, but not vice versa. Finally, we illustrate the usage of our formal model for the analysis of existing rational exchange protocols by analyzing a protocol proposed by Syverson. We show that the protocol is rational only under the assumption that the network is reliable. [ABSTRACT FROM AUTHOR]

We describe a protocol design process, and illustrate its use by creating ATSPECT, an Authentication Test‐based Secure Protocol for Electronic Commerce Transactions. The design process is organized around the authentication tests, a method for protocol verification based on the strand space theory. The authentication tests dictate how randomly generated values such as nonces may be combined with encryption to achieve authentication and freshness. ATSPECT offers functionality and security guarantees akin to the purchase request, payment authorization, and payment capture phases of SET, the secure electronic transaction standard created by the major credit card firms. [ABSTRACT FROM AUTHOR]

Important properties of many protocols are liveness or availability, i.e., that something good happens now and then. In asynchronous scenarios, these properties depend on the scheduler, which is usually considered to be fair in this case. The standard definitions of fairness and liveness are based on infinite sequences. Unfortunately, this cannot be applied to most cryptographic protocols since one must restrict the adversary and the runs as a whole to length polynomial in the security parameter. We present the first general definition of polynomial fairness and liveness in asynchronous scenarios which can cope with cryptographic protocols. Furthermore, our definitions provide a link to the common approach of simulatability which is used throughout modern cryptography: We show that polynomial liveness is maintained under simulatability. As an example, we present an abstract specification and a secure implementation of secure message transmission with reliable channels, and prove them to fulfill the desired liveness property, i.e., reliability of messages. [ABSTRACT FROM AUTHOR]

We present the first type and effect system for proving authenticity properties of security protocols based on asymmetric cryptography. The most significant new features of our type system are: (1) a separation of public types (for data possibly sent to the opponent) from tainted types (for data possibly received from the opponent) via a subtype relation; (2) trust effects, to guarantee that tainted data does not, in fact, originate from the opponent; and (3) challenge/response types to support a variety of idioms used to guarantee message freshness. We illustrate the applicability of our system via protocol examples. [ABSTRACT FROM AUTHOR]

We use the probabilistic model checker PRISM to analyze the Crowds system for anonymous Web browsing. This case study demonstrates how probabilistic model checking techniques can be used to formally analyze security properties of a peer‐to‐peer group communication system based on random message routing among members. The behavior of group members and the adversary is modeled as a discrete‐time Markov chain, and the desired security properties are expressed as PCTL formulas. The PRISM model checker is used to perform automated analysis of the system and verify anonymity guarantees it provides. Our main result is a demonstration of how certain forms of probabilistic anonymity degrade when group size increases or random routing paths are rebuilt, assuming that the corrupt group members are able to identify and/or correlate multiple routing paths originating from the same sender. [ABSTRACT FROM AUTHOR]

We carry forward the work described in our previous papers [5,18,20] on the application of data independence to the model checking of security protocols using CSP [19] and FDR [10]. In particular, we showed how techniques based on data independence [12,19] could be used to justify, by means of a finite FDR check, systems where agents can perform an unbounded number of protocol runs. Whilst this allows for a more complete analysis, there was one significant incompleteness in the results we obtained: while each individual identity could perform an unlimited number of protocol runs sequentially, the degree of parallelism remained bounded (and small to avoid state space explosion). In this paper, we report significant progress towards the solution of this problem, by means anticipated in [5], namely by “internalising” protocol roles within the “intruder” process. The internalisation of protocol roles (initially only server‐type roles) was introduced in [20] as a state‐space reduction technique (for which it is usually spectacularly successful). It was quickly noticed that this had the beneficial side‐effect of making the internalised server arbitrarily parallel, at least in cases where it did not generate any new values of data independent type. We now consider the case where internal roles do introduce fresh values and address the issue of capturing their state of mind (for the purposes of analysis). [ABSTRACT FROM AUTHOR]

We formalize the Dolev–Yao model of security protocols, using a notation based on multiset rewriting with existentials. The goals are to provide a simple formal notation for describing security protocols, to formalize the assumptions of the Dolev–Yao model using this notation, and to analyze the complexity of the secrecy problem under various restrictions. We prove that, even for the case where we restrict the size of messages and the depth of message encryption, the secrecy problem is undecidable for the case of an unrestricted number of protocol roles and an unbounded number of new nonces. We also identify several decidable classes, including a DEXP‐complete class when the number of nonces is restricted, and an NP‐complete class when both the number of nonces and the number of roles is restricted. We point out a remaining open complexity problem, and discuss the implications these results have on the general topic of protocol analysis. [ABSTRACT FROM AUTHOR]

During the last few years, a number of authenticated group key agreement protocols have been proposed in the literature. We observed that the efforts in this domain were mostly dedicated to the improvement of their performance in term of bandwidth or computational requirements, but that there were very few systematic studies on their security properties. In this paper, we tried to develop a systematic way to analyse protocol suites extending the Diffie‐Hellman key‐exchange scheme to a group setting and presented in the context of the Cliques project. This led us to propose a very simple machinery that allowed us to manually pinpoint several unpublished attacks against the main security properties claimed in the definition of these protocols (implicit key agreement, perfect forward secrecy, resistance to known‐key attacks). [ABSTRACT FROM AUTHOR]

We present a logic for proving security properties of protocols that use nonces (randomly generated numbers that uniquely identify a protocol session) and public‐key cryptography. The logic, designed around a process calculus with actions for each possible protocol step, consists of axioms about protocol actions and inference rules that yield assertions about protocols composed of multiple steps. Although assertions are written using only steps of the protocol, the logic is sound in a stronger sense: each provable assertion about an action or sequence of actions holds in any run of the protocol that contains the given actions and arbitrary additional actions by a malicious attacker. This approach lets us prove security properties of protocols under attack while reasoning only about the sequence of actions taken by honest parties to the protocol. The main security‐specific parts of the proof system are rules for reasoning about the set of messages that could reveal secret data and an invariant rule called the “honesty rule”. [ABSTRACT FROM AUTHOR]

The development of new classes of distributed applications such as telephony, remote video, and virtual reality introduces new quality requirements that make inadequate even the current best-effort service model provided by international networks. Recent research activity has proposed new approaches to accommodate these new application requirements. While exploiting the resource needs of different applications to use the network resources efficiently, these approaches require the maintenance of a considerable amount of state information at the network nodes. Correctness and availability of such information are the basic requirements for the proper working of the network.In this paper we present a system, called Global Infrastructure Protection System (GIPS), to control improper modifications to this state information. We illustrate the GIPS's architecture and identify topology conditions to guarantee the distributed fault tolerant detection of anomalies. The system is based on the use of a hierarchical structure to organize and maintain the information at each node. Improper network states are described through rules that characterize state information updates that may result anomalous (or uncommon) with respect to the network status, past events occurred, or statistical measures. We introduce a notation to represent state information coming from heterogeneous protocols, and statistical operators to examine the history of state updates accumulated during operation. Finally, we present some examples using our notation to express heuristical rules detecting anomalous operations in a network. [ABSTRACT FROM AUTHOR]

A strand is a sequence of events; it represents either an execution by a legitimate party in a security protocol or else a sequence of actions by a penetrator. A strand space is a collection of strands, equipped with a graph structure generated by causal interaction. In this framework, protocol correctness claims may be expressed in terms of the connections between strands of different kinds. Preparing for a first example, the Needham--Schroeder--Lowe protocol, we prove a lemma that gives a bound on the abilities of the penetrator in any protocol. Our analysis of the example gives a detailed view of the conditions under which it achieves authentication and protects the secrecy of the values exchanged. We also use our proof methods to explain why the original Needham--Schroeder protocol fails. Before turning to a second example, we introduce ideals as a method to prove additional bounds on the abilities of the penetrator. We can then prove a number of correctness properties of the Otway-Rees protocol, and we clarify its limitations. We believe that our approach is distinguished from other work by the simplicity of the model, the precision of the results it produces, and the ease of developing intelligible and reliable proofs even without automated support. [ABSTRACT FROM AUTHOR]

Model checking approaches to the analysis of security protocols have proved remarkably successful. The basic approach is to produce a model of a small system running the protocol, together with a model of the most general intruder who can interact with the protocol, and then to use a state exploration tool to search for attacks. This has led to a number of new attacks upon protocols being discovered. However, if no attack is found, this only tells us that there is no attack upon the small system we modelled; there may be an attack upon some larger system. This is the question we consider in this paper: we prove that under certain conditions on the protocol and the environment in which it operates, if there is no attack upon a particular small system (with one honest agent for each role of the protocol) leading to a breach of secrecy, then there is no attack on any larger system leading to a breach of secrecy. [ABSTRACT FROM AUTHOR]

Conventional host-based and network-based intrusion and misuse detection systems have concentrated on detecting network-based and internal attacks, but little work has addressed host-based detection of low-level network attacks. A major reason for this is the misuse detection system's dependence on audit data and the absence of low-level network data in audit trails. This work defines low-level IP vulnerabilities and distinguishes between low-level IP and IP-based vulnerabilities. Furthermore, we analyze a number of different low-level IP attacks and the vulnerabilities that they exploit. We develop attack signatures for each attack, and based upon our analysis, we determine a baseline collection of information needed to detect the attacks. We suggest locations within protocol stacks where the needed data can be collected. Finally, we generalize from the baseline audit data to try to predict audit content suitable not only for detecting these attacks, but possible future ones. [ABSTRACT FROM AUTHOR]