nach oben

2010 | Buch

Kapitel lesen Erstes Kapitel lesen

Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security

Joint Workshop, ARSPA-WITS 2010, Paphos, Cyprus,March 27-28, 2010. Revised Selected Papers

herausgegeben von: Alessandro Armando, Gavin Lowe

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

Inhaltsverzeichnis

Frontmatter

The CaPiTo Approach to Protocol Validation

(Invited Talk)

Abstract

We show how to model service-oriented applications using the process algebra CaPiTo so that, on the one hand, we can achieve an abstract specification without being overwhelmed by the underlying implementation details and, on the other hand, we can obtain a concrete specification respecting the industrial standards used for ensuring security. We consider this development important in order to get a good agreement between the protocols analysed by formal tools and the applications developed by practitioners.

We then show how to transform the concrete specification into the LySa analysis framework, used in the SENSORIA EU project and originally developed in the DEGAS EU project, for analysing cryptographic protocols under a Dolev-Yao attacker. This allows us to perform a control flow analysis for ensuring the authenticity (as well as confidentiality) of messages exchanged between services. The LySa analysis framework is implemented in polynomial time in the size of the protocol specification using the Succinct Solver, that can solve a superset of Datalog clauses.

Flemming Nielson, Han Gao, Hanne Riis Nielson

Reasoning about Probabilistic Security Using Task-PIOAs

Abstract

Task-structured probabilistic input/output automata (Task-PIOAs) are concurrent probabilistic automata that, among other things, have been used to provide a formal framework for the universal composability paradigms of protocol security. One of their advantages is that that they allow one to distinguish high-level nondeterminism that can affect the outcome of the protocol, from low-level choices, which can’t. We present an alternative approach to analyzing the structure of Task-PIOAs that relies on ordered sets. We focus on two of the components that are required to define and apply Task-PIOAs: discrete probability theory and automata theory. We believe our development gives insight into the structure of Task-PIOAs and how they can be utilized to model crypto-protocols. We illustrate our approach with an example from anonymity, an area that has not previously been addressed using Task-PIOAs. We model Chaum’s Dining Cryptographers Protocol at a level that does not require cryptographic primitives in the analysis. We show via this example how our approach can leverage a proof of security in the case a principal behaves deterministically to prove security when that principal behaves probabilistically.

Aaron D. Jaggard, Catherine Meadows, Michael Mislove, Roberto Segala

Secrecy and Authenticity Types for Secure Distributed Messaging

Abstract

We introduce a calculus with mobile names, distributed principals and primitives for secure remote communication, without any reference to explicit cryptography. The calculus is equipped with a system of types and effects providing static guarantees of secrecy and authenticity in the presence of a Dolev-Yao intruder. The novelty with respect to existing type systems for security is in the structure of our secrecy and authenticity types, which are inspired by the formulas of BAN Logic, and retain much of the simplicity and intuitive reading of such formulas. Drawing on these types, the type system makes it possible to characterize authenticity directly as a property of the data exchanged during a protocol rather than indirectly by extracting and interpreting the effects the protocol has on that data.

Michele Bugliesi, Stefano Calzavara, Damiano Macedonio

Modular Plans for Secure Service Composition

Abstract

Service Oriented Computing (SOC) is a programming paradigm aiming at characterising Service Networks. Services are entities waiting for clients requests and they often result from the composition of many services.

We address here the problem of statically guaranteeing security of open services, i.e. services with unknown components. Security constraints are expressed by local policies that service components must obey.

We present here a type and effect system that safely over-approximates, in the form of history expressions, the possible run-time behaviour of open services, collecting partial information on the behaviours of their components. From a history expression, we then extract a plan that drives executions that never rise security violations.

Finally, we show how partial plans satisfying security requirements can be put together to obtain a safe orchestration plan.

Gabriele Costa, Pierpaolo Degano, Fabio Martinelli

A Type System for Access Control Views in Object-Oriented Languages

Abstract

Access control to objects in common object-oriented languages is statically verified but cannot be changed at run-time. However, dynamic authorization is required by most applications and it would be desirable to check more flexible access control policies also statically, at least partially. In this work, we introduce a model where “views” to object references represent the current access control policy of a principal for a given object, and first class authorizations support dynamic modification of those policies. To demonstrate our concepts, we have developed a core language, equipped with a provably correct type and effect system capable of detecting unauthorized method calls at compile-time, and defined and implemented a typechecking algorithm.

Mário Pires, Luís Caires

Formal Analysis of Key Integrity in PKCS#11

Abstract

PKCS#11 is a standard API to cryptographic devices such as smarcards, hardware security modules and usb crypto-tokens. Though widely adopted, this API has been shown to be prone to attacks in which a malicious user gains access to the sensitive keys stored in the devices. In 2008, Delaune, Kremer and Steel proposed a model to formally reason on this kind of attacks. We extend this model to also describe flaws that are based on integrity violations of the stored keys. In particular, we consider scenarios in which a malicious overwriting of keys might fool honest users into using attacker’s own keys, while performing sensitive operations. We further enrich the model with a trusted key mechanism ensuring that only controlled, non-tampered keys are used in cryptographic operations, and we show how this modified API prevents the above mentioned key-replacement attacks.

Andrea Falcone, Riccardo Focardi

Secure Upgrade of Hardware Security Modules in Bank Networks

Abstract

We study the secure upgrade of critical components in wide networked systems, focussing on the case study of PIN processing Hardware Security Modules (HSMs). These tamper-resistant devices, used by banks to securely transmit and verify the PIN typed at the ATMs, have been shown to suffer from API level attacks that allow an insider to recover user PINs and, consequently, clone cards. Proposed fixes require to reduce and modify the HSM functionality by, e.g., sticking on a single format of the transmitted PIN or adding MACs for the integrity of user data. Upgrading HSMs worldwide is, of course, unaffordable. We thus propose strategies to incrementally upgrade the network so to obtain upgraded, secure subnets, while preserving the compatibility towards the legacy system. Our strategies aim at finding tradeoffs between the cost for special “guardian” HSMs used on the borderline between secure and insecure nodes, and the size of the team working in the upgrade process, representing the maximum number of nodes that can be simultaneously upgraded.

Riccardo Focardi, Flaminia L. Luccio

Interactive Information Flow

(Invited Talk)

Abstract

In recent years, there has been a growing interest in considering the quantitative aspects of Information Flow, partly because often the a priori knowledge of the secret information can be represented by a probability distribution, and partly because the mechanisms to protect the information may use randomization to obfuscate the relation between the secrets and the observables.

We consider the problem of defining a measure of information leakage in interactive systems. We show that the information-theoretic approach which interprets such systems as (simple) noisy channels is not valid anymore when the secrets and the observables can alternate during the computation, and influence each other. However, the principle can be retrieved if we consider more complicated types of channels, that in Information Theory are known as channels with memory and feedback. We show that there is a complete correspondence between interactive systems and such kind of channels. Furthermore, the proposed framework has good topological properties which allow to reason compositionally about the worst-case leakage in these systems.

Catuscia Palamidessi, Mário S. Alvim, Miguel E. Andrés

Portunes: Representing Attack Scenarios Spanning through the Physical, Digital and Social Domain

Abstract

The security goals of an organization are realized through security policies, which concern physical security, digital security and security awareness. An insider is aware of these security policies, and might be able to thwart the security goals by combining physical, digital and social means. A systematic analysis of such attacks requires the whole environment where the insider operates to be formally represented. This paper presents Portunes, a framework which integrates all three security domains in a single environment. Portunes consists of a high-level abstraction model focusing on the relations between the three security domains and a lower abstraction level language able to represent the model and describe attacks which span the three security domains.

Using the Portunes framework, we are able to represent a whole new family of attacks where the insider is not assumed to use purely digital actions to achieve a malicious goal.

Trajce Dimkov, Wolter Pieters, Pieter Hartel

Match It or Die: Proving Integrity by Equality

Abstract

Cryptographic hash functions are commonly used as modification detection codes. The goal is to provide message integrity assurance by comparing the digest of the original message with the hash of what is thought to be the intended message. This paper generalizes this idea by applying it to general expressions instead of just digests: success of an equality test between a tainted data and a trusted one can be seen as a proof of high-integrity for the first item. Secure usage of hash functions is also studied with respect to the confidentiality of digests by extending secret-sensitive noninterference of Demange and Sands.

Matteo Centenaro, Riccardo Focardi

Towards Automatic Analysis of Election Verifiability Properties

Abstract

We present a symbolic definition that captures some cases of election verifiability for electronic voting protocols. Our definition is given in terms of reachability assertions in the applied pi calculus and is amenable to automated reasoning using the software tool ProVerif. The definition distinguishes three aspects of verifiability, which we call individual, universal, and eligibility verifiability. We demonstrate the applicability of our formalism by analysing the protocols due to Fujioka, Okamoto & Ohta and a variant of the one by Juels, Catalano & Jakobsson (implemented as Civitas by Clarkson, Chong & Myers).

Ben Smyth, Mark Ryan, Steve Kremer, Mounira Kourjieh

AnBx - Security Protocols Design and Verification

Abstract

Designing distributed protocols is challenging, as it requires actions at very different levels: from the choice of network-level mechanisms to protect the exchange of sensitive data, to the definition of structured interaction patterns to convey application-specific guarantees. Current security infrastructures provide very limited support for the specification of such guarantees. As a consequence, the high-level security properties of a protocol typically must often be hard-coded explicitly, in terms of low-level cryptographic notions and devices which clutter the design and undermine its scalability and robustness.

To counter these problems, we propose an extended Alice & Bob notation for protocol narrations (AnBx) to be employed for a purely declarative modelling of distributed protocols. These abstractions provide a compact specification of the high-level security guarantees they convey, and help shield the design from the details of the underlying cryptographic infrastructure. We discuss an implementation of the abstractions based on a translation from the AnBx notation to the AnB language supported by the OFMC [1,2] verification tool. We show the practical effectiveness of our approach by revisiting the iKP e-payment protocols, and showing that the security goals achieved by our declarative specification outperform those offered by the original protocols.

Michele Bugliesi, Paolo Modesti

Backmatter

Titel: Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security
herausgegeben von: Alessandro Armando
Gavin Lowe
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-642-16074-5
Print ISBN: 978-3-642-16073-8
DOI: https://doi.org/10.1007/978-3-642-16074-5