nach oben

2015 | Buch

Kapitel lesen Erstes Kapitel lesen

Principles of Security and Trust

4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings

herausgegeben von: Riccardo Focardi, Andrew Myers

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the refereed proceedings of the 4th International Conference on Principles of Security and Trust, POST 2015, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, in London, UK, in April 2015. The 17 regular papers presented in this volume were carefully reviewed and selected from 57 submissions. In addition, one invited talk is included. The papers have been organized in topical sections on information flow and security types, risk assessment and security policies, protocols, hardware and physical security and privacy and voting.

Inhaltsverzeichnis

Frontmatter

Invited Contribution

Frontmatter

Quantitative Approaches to the Protection of Private Information: State of the Art and Some Open Challenges

Abstract

Privacy is a broad concept affecting a variety of modern-life activities. As a consequence, during the last decade there has been a vast amount of research on techniques to protect privacy, such as communication anonymizers [9], electronic voting systems [8], Radio-Frequency Identification (RFID) protocols [13] and private information retrieval schemes [7], to name a few.

Catuscia Palamidessi

Information Flow and Security Types

Frontmatter

IFC Inside: Retrofitting Languages with Dynamic Information Flow Control

Abstract

Many important security problems in JavaScript, such as browser extension security, untrusted JavaScript libraries and safe integration of mutually distrustful websites (mash-ups), may be effectively addressed using an efficient implementation of information flow control (IFC). Unfortunately existing fine-grained approaches to JavaScript IFC require modifications to the language semantics and its engine, a non-goal for browser applications. In this work, we take the ideas of coarse-grained dynamic IFC and provide the theoretical foundation for a language-based approach that can be applied to any programming language for which external effects can be controlled. We then apply this formalism to server- and client-side JavaScript, show how it generalizes to the C programming language, and connect it to the Haskell LIO system. Our methodology offers design principles for the construction of information flow control systems when isolation can easily be achieved, as well as compositional proofs for optimized concrete implementations of these systems, by relating them to their isolated variants.

Stefan Heule, Deian Stefan, Edward Z. Yang, John C. Mitchell, Alejandro Russo

Very Static Enforcement of Dynamic Policies

Abstract

Security policies are naturally dynamic. Reflecting this, there has been a growing interest in studying information-flow properties which change during program execution, including concepts such as declassification, revocation, and role-change.

A static verification of a dynamic information flow policy, from a semantic perspective, should only need to concern itself with two things: 1) the dependencies between data in a program, and 2) whether those dependencies are consistent with the intended flow policies as they change over time. In this paper we provide a formal ground for this intuition. We present a straightforward extension to the principal flow-sensitive type system introduced by Hunt and Sands (POPL ’06, ESOP ’11) to infer both end-to-end dependencies and dependencies at intermediate points in a program. This allows typings to be applied to verification of both static and dynamic policies. Our extension preserves the principal type system’s distinguishing feature, that type inference is independent of the policy to be enforced: a single, generic dependency analysis (typing) can be used to verify many different dynamic policies of a given program, thus achieving a clean separation between (1) and (2).

We also make contributions to the foundations of dynamic information flow. Arguably, the most compelling semantic definitions for dynamic security conditions in the literature are phrased in the so-called knowledge-based style. We contribute a new definition of knowledge-based progress insensitive security for dynamic policies. We show that the new definition avoids anomalies of previous definitions and enjoys a simple and useful characterisation as a two-run style property.

Bart van Delft, Sebastian Hunt, David Sands

The Foundational Cryptography Framework

Abstract

We present the Foundational Cryptography Framework (FCF) for developing and checking complete proofs of security for cryptographic schemes within a proof assistant. This is a general-purpose framework that is capable of modeling and reasoning about a wide range of cryptographic schemes, security definitions, and assumptions. Security is proven in the computational model, and the proof provides concrete bounds as well as asymptotic conclusions. FCF provides a language for probabilistic programs, a theory that is used to reason about programs, and a library of tactics and definitions that are useful in proofs about cryptography. The framework is designed to leverage fully the existing theory and capabilities of the Coq proof assistant in order to reduce the effort required to develop proofs.

Adam Petcher, Greg Morrisett

On the Flow of Data, Information, and Time

Abstract

We study information flow in a model for data-parallel computing. We show how an extant notion of virtual time can help guarantee information-flow properties. For this purpose, we introduce functions that express dependencies between inputs and outputs at each node in a dataflow graph. Each node may operate over a distinct set of virtual times—so, from a security perspective, it may have its own classification scheme. A coherence criterion ensures that those local dependencies yield global properties.

Martín Abadi, Michael Isard

Risk Assessment and Security Policies

Frontmatter

Pareto Efficient Solutions of Attack-Defence Trees

Abstract

Attack-defence trees are a promising approach for representing threat scenarios and possible countermeasures in a concise and intuitive manner. An attack-defence tree describes the interaction between an attacker and a defender, and is evaluated by assigning parameters to the nodes, such as probability or cost of attacks and defences. In case of multiple parameters most analytical methods optimise one parameter at a time, e.g., minimise cost or maximise probability of an attack. Such methods may lead to sub-optimal solutions when optimising conflicting parameters, e.g., minimising cost while maximising probability.

In order to tackle this challenge, we devise automated techniques that optimise all parameters at once. Moreover, in the case of conflicting parameters our techniques compute the set of all optimal solutions, defined in terms of Pareto efficiency. The developments are carried out on a new and general formalism for attack-defence trees.

Zaruhi Aslanyan, Flemming Nielson

Analysis of XACML Policies with SMT

Abstract

The eXtensible Access Control Markup Language (XACML) is an extensible and flexible XML language for the specification of access control policies. However, the richness and flexibility of the language (along with the verbose syntax of XML) come with a price: errors are easy to make and difficult to detect when policies grow in size. If these errors are not detected and rectified, they can result in serious data leakage and/or privacy violations leading to significant legal and financial consequences. To assist policy authors in the analysis of their policies, several policy analysis tools have been proposed based on different underlying formalisms. However, most of these tools either abstract away functions over non-Boolean domains (hence they cannot provide information about them) or produce very large encodings which hinder the performance. In this paper, we present a generic policy analysis framework that employs SMT as the underlying reasoning mechanism. The use of SMT does not only allow more fine-grained analysis of policies but also improves the performance. We demonstrate that a wide range of security properties proposed in the literature can be easily modeled within the framework. A prototype implementation and its evaluation are also provided.

Fatih Turkmen, Jerry den Hartog, Silvio Ranise, Nicola Zannone

Protocols

Frontmatter

Automatically Checking Commitment Protocols in ProVerif without False Attacks

Abstract

ProVerif over-approximates the attacker’s power to enable verification of processes under replication. Unfortunately, this results in ProVerif finding false attacks. This problem is particularly common in protocols whereby a participant commits to a particular value and later reveals their value. We introduce a method to reduce false attacks when analysing secrecy. First, we show how inserting phases into non-replicated processes enables a more accurate translation to Horn clauses which avoids some false attacks. Secondly, we generalise our methodology to processes under replication. Finally, we demonstrate the applicability of our technique by analysing BlueTooth Simple Pairing. Moreover, we propose a simplification of this protocol that achieves the same security goal.

Tom Chothia, Ben Smyth, Chris Staite

Generalizing Multi-party Contract Signing

Abstract

Multi-party contract signing (MPCS) protocols allow a group of signers to exchange signatures on a predefined contract. Previous approaches considered either completely linear protocols or fully parallel broadcasting protocols. We introduce the new class of DAG MPCS protocols which combines parallel and linear execution and allows for parallelism even within a signer role. This generalization is useful in practical applications where the set of signers has a hierarchical structure, such as chaining of service level agreements and subcontracting.

Our novel DAG MPCS protocols are represented by directed acyclic graphs and equipped with a labeled transition system semantics. We define the notion of abort-chaining sequences and prove that a DAG MPCS protocol satisfies fairness if and only if it does not have an abort-chaining sequence. We exhibit several examples of optimistic fair DAG MPCS protocols. The fairness of these protocols follows from our theory and has additionally been verified with our automated tool.

We define two complexity measures for DAG MPCS protocols, related to execution time and total number of messages exchanged. We prove lower bounds for fair DAG MPCS protocols in terms of these measures.

Sjouke Mauw, Saša Radomirović

Leakiness is Decidable for Well-Founded Protocols

Abstract

A limit to algorithmic verification of security protocols is posed by the fact that checking whether a security property such as secrecy is satisfied is undecidable in general. In this paper we introduce the class of well-founded protocols. It is designed to exclude what seems to be common to all protocols used in undecidability proofs: the protocol syntax ensures that honest information cannot be propagated unboundedly without the intruder manipulating it. We show that the secrecy property of leakiness is decidable for well-founded protocols.

Sibylle Fröschle

Abstractions for Security Protocol Verification

Abstract

We present a large class of security protocol abstractions with the aim of improving the scope and efficiency of verification tools. We propose typed abstractions, which transform a term’s structure based on its type, and untyped abstractions, which remove atomic messages, variables, and redundant terms. Our theory improves on previous work by supporting a useful subclass of shallow subterm-convergent rewrite theories, user-defined types, and untyped variables to cover type flaw attacks. We prove soundness results for an expressive property language that includes secrecy and authentication. Applying our abstractions to realistic IETF protocol models, we achieve dramatic speedups and extend the scope of several modern security protocol analyzers.

Binh Thanh Nguyen, Christoph Sprenger

Hardware and Physical Security

Frontmatter

Automated Backward Analysis of PKCS#11 v2.20

Abstract

The PKCS#11 standard describes an API for cryptographic operations which is used in scenarios where cryptographic secrets need to be kept secret, even in case of server compromise. It is widely deployed and supported by many hardware security modules and smart cards. A variety of attacks in the literature illustrate the importance of a careful configuration, as API-level attacks may otherwise extract keys.

Formal verification of PKCS#11 configurations requires the analysis of a system that contains mutable state, a problem that existing methods solved by either artificially restricting the number of keys, introducing model-specific over-approximation or performing proofs by hand. At Security & Privacy 2014, Kremer and Künnemann presented a variant of the applied pi calculus that handles global state and, in conjunction with the tamarin prover for protocol verification, allows for the precise analysis of protocols with state. Using this tool chain, we show secrecy of keys for a PKCS#11 configuration that makes use of features introduced in version 2.20 of the standard, including wrap and unwrap templates in an extensible model.

This configuration supports the creation of so-called wrapping keys for import and export of sensitive keys (e.g., for backup or transfer), and it permits the co-existence of sensitive keys and non-sensitive keys on the same device.

Robert Künnemann

A Safe Update Mechanism for Smart Cards

Abstract

With the advent of the integration of smart card chips into national identity documents, the business model of replacing compromised smart cards becomes uneconomical. We propose a mechanism to safely apply updates to embedded systems, particularly high value smart cards, that are costly to replace. We identify the requirements for such a mechanism and describe how it can be implemented. Our mechanism achieves its properties at the expense of using moderately more non-volatile memory to store program code than contemporary smart cards. We have developed a Common Criteria protection profile package to abstractly describe such a mechanism and summarize it in this paper. The mechanism and the abstract description can be a starting point for a practical realization in consumer products.

Kristian Beilke, Volker Roth

Discrete vs. Dense Times in the Analysis of Cyber-Physical Security Protocols

Abstract

Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two agents. We classify such security protocols as Cyber-Physical. Time plays a key role in design and analysis of many of these protocols. This paper investigates the foundational differences and the impacts on the analysis when using models with discrete time and models with dense time. We show that there are attacks that can be found by models using dense time, but not when using discrete time. We illustrate this with a novel attack that can be carried out on most distance bounding protocols. In this attack, one exploits the execution delay of instructions during one clock cycle to convince a verifier that he is in a location different from his actual position. We propose a Multiset Rewriting model with dense time suitable for specifying cyber-physical security protocols. We introduce Circle-Configurations and show that they can be used to symbolically solve the reachability problem for our model. Finally, we show that for the important class of balanced theories the reachability problem is PSPACE-complete.

Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov, Carolyn Talcott

Timing Attacks in Security Protocols: Symbolic Framework and Proof Techniques

Abstract

We propose a framework for timing attacks, based on (a variant of) the applied-pi calculus. Since many privacy properties, as well as strong secrecy and game-based security properties, are stated as process equivalences, we focus on (time) trace equivalence. We show that actually, considering timing attacks does not add any complexity: time trace equivalence can be reduced to length trace equivalence, where the attacker no longer has access to execution times but can still compare the length of messages. We therefore deduce from a previous decidability result for length equivalence that time trace equivalence is decidable for bounded processes and the standard cryptographic primitives.

As an application, we study several protocols that aim for privacy. In particular, we (automatically) detect an existing timing attack against the biometric passport and new timing attacks against the Private Authentication protocol.

Vincent Cheval, Véronique Cortier

Privacy and Voting

Frontmatter

Type-Based Verification of Electronic Voting Protocols

Abstract

E-voting protocols aim at achieving a wide range of sophisticated security properties and, consequently, commonly employ advanced cryptographic primitives. This makes their design as well as rigorous analysis quite challenging. As a matter of fact, existing automated analysis techniques, which are mostly based on automated theorem provers, are inadequate to deal with commonly used cryptographic primitives, such as homomorphic encryption and mix-nets, as well as some fundamental security properties, such as verifiability.

This work presents a novel approach based on refinement type systems for the automated analysis of e-voting protocols. Specifically, we design a generically applicable logical theory which, based on pre- and post-conditions for security-critical code, captures and guides the type-checker towards the verification of two fundamental properties of e-voting protocols, namely, vote privacy and verifiability. We further develop a code-based cryptographic abstraction of the cryptographic primitives commonly used in e-voting protocols, showing how to make the underlying algebraic properties accessible to automated verification through logical refinements. Finally, we demonstrate the effectiveness of our approach by developing the first automated analysis of Helios, a popular web-based e-voting protocol, using an off-the-shelf type-checker.

Véronique Cortier, Fabienne Eigner, Steve Kremer, Matteo Maffei, Cyrille Wiedling

Composing Security Protocols: From Confidentiality to Privacy

Abstract

Security protocols are used in many of our daily-life applications, and our privacy largely depends on their design. Formal verification techniques have proved their usefulness to analyse these protocols, but they become so complex that modular techniques have to be developed. We propose several results to safely compose security protocols. We consider arbitrary primitives modeled using an equational theory, and a rich process algebra close to the applied pi calculus.

Relying on these composition results, we derive some security properties on a protocol from the security analysis performed on each of its sub-protocols individually. We consider parallel composition and the case of key-exchange protocols. Our results apply to deal with confidentiality but also privacy-type properties (e.g. anonymity) expressed using a notion of equivalence. We illustrate the usefulness of our composition results on protocols from the 3G phone application and electronic passport.

Myrto Arapinis, Vincent Cheval, Stéphanie Delaune

PriCL: Creating a Precedent, a Framework for Reasoning about Privacy Case Law

Abstract

We introduce PriCL: the first framework for expressing and automatically reasoning about privacy case law by means of precedent. PriCL is parametric in an underlying logic for expressing world properties, and provides support for court decisions, their justification, the circumstances in which the justification applies as well as court hierarchies. Moreover, the framework offers a tight connection between privacy case law and the notion of norms that underlies existing rule-based privacy research. In terms of automation, we identify the major reasoning tasks for privacy cases such as deducing legal permissions or extracting norms. For solving these tasks, we provide generic algorithms that have particularly efficient realizations within an expressive underlying logic. Finally, we derive a definition of deducibility based on legal concepts and subsequently propose an equivalent characterization in terms of logic satisfiability.

Michael Backes, Fabian Bendun, Jörg Hoffmann, Ninja Marnau

Backmatter

Titel: Principles of Security and Trust
herausgegeben von: Riccardo Focardi
Andrew Myers
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-662-46666-7
Print ISBN: 978-3-662-46665-0
DOI: https://doi.org/10.1007/978-3-662-46666-7