Skip to main content

Über dieses Buch

This book constitutes the thoroughly refereed post-proceedings of the 7th International Workshop on Formal Aspects of Security and Trust, FAST 2010, held as part of the 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2010 in Pisa, Italy in September 2010. The 14 revised full papers presented together with one invited paper were carefully reviewed and selected from 42 submissions. The papers focus of formal aspects in security and trust policy models, security protocol design and analysis, formal models of trust and reputation, logics for security and trust, distributed trust management systems, trust-based reasoning, digital assets protection, data protection, privacy and id issues, information flow analysis, language-based security, security and trust aspects in ubiquitous computing, validation/analysis tools, web service security/trust/privacy, grid security, security risk assessment, and case studies.



Quantifying and Qualifying Trust: Spectral Decomposition of Trust Networks

In a previous FAST paper, I presented a quantitative model of the process of trust building, and showed that trust is accumulated like wealth: the rich get richer. This explained the pervasive phenomenon of adverse selection of trust certificates, as well as the fragility of trust networks in general. But a simple explanation does not always suggest a simple solution. It turns out that it is impossible to alter the fragile distribution of trust without sacrificing some of its fundamental functions. A solution for the vulnerability of trust must thus be sought elsewhere, without tampering with its distribution. This observation was the starting point of the present paper. It explores different methods for securing trust: not by redistributing, but by qualifying it. The methods used to break privacy can be used to secure trust.
Dusko Pavlovic

Bounded Memory Dolev-Yao Adversaries in Collaborative Systems

This paper extends existing models for collaborative systems. We investigate how much damage can be done by insiders alone, without collusion with an outside adversary. In contrast to traditional intruder models, such as in protocol security, all the players inside our system, including potential adversaries, have similar capabilities. They have bounded storage capacity, that is, they can only remember at any moment a bounded number of facts. This is technically imposed by only allowing balanced actions, that is, actions that have the same number of facts in their pre and post conditions. On the other hand, the adversaries inside our system have many capabilities of the standard Dolev-Yao intruder, namely, they are able, within their bounded storage capacity, to compose, decompose, overhear, and intercept messages as well as update values with fresh ones. We investigate the complexity of the decision problem of whether or not an adversary is able to discover secret data. We show that this problem is PSPACE-complete when all actions are balanced and can update values with fresh ones. As an application we turn to security protocol analysis and demonstrate that many protocol anomalies, such as the Lowe anomaly in the Needham-Schroeder public key exchange protocol, can also occur when the intruder is one of the insiders with bounded memory.
Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov

Efficient Decision Procedures for Message Deducibility and Static Equivalence

We consider two standard notions in formal security protocol analysis: message deducibility and static equivalence under equational theories. We present new polynomial-time algorithms for deciding both notions under subterm convergent equational theories and under a theory representing symmetric encryption with the prefix property. For these equational theories, polynomial-time algorithms for the decision problems associated to both notions are well-known (although this has not been proven for static equivalence under the prefix theory). However, our algorithms have a significantly better asymptotic complexity than existing approaches.
As an application, we use our algorithm for static equivalence to discover off-line guessing attacks on the Kerberos protocol when implemented using a symmetric encryption scheme for which the prefix property holds.
Bruno Conchinha, David Basin, Carlos Caleiro

Understanding Abstractions of Secure Channels

Many security architectures make use of layered security protocols, where a special-purpose application protocol is layered on top of a general-purpose secure transport protocol. When analysing such an architecture, it makes sense to abstract away from the implementation details of the secure transport protocol and just model the services it provides. But is this abstraction sound, or might it risk losing attacks? This is the question we consider in this paper. We show that —under certain assumptions— the abstraction is sound, in the sense that it correctly models the application-layer behaviour as seen by honest principals.
Allaa Kamil, Gavin Lowe

Information Flow Analysis via Path Condition Refinement

We present a new approach to information flow control (IFC), which exploits counterexample-guided abstraction refinement (CEGAR) technology. The CEGAR process is built on top of our existing IFC analysis in which illegal flows are characterized using program dependence graphs (PDG) and path conditions (as described in [12]). Although path conditions provide an already precise abstraction that can be used to generate witnesses to the illegal flow, they may still cause false alarms. Our CEGAR process recognizes false witnesses by executing them and monitoring their executions, and eliminates them by automatically refining path conditions in an iterative way as needed. The paper sketches the foundations of CEGAR and PDG-based IFC, and describes the approach in detail. An example shows how the approach finds illegal flow, and demonstrates how CEGAR eliminates false alarms.
Mana Taghdiri, Gregor Snelting, Carsten Sinz

Foundations of Attack–Defense Trees

We introduce and give formal definitions of attack–defense trees. We argue that these trees are a simple, yet powerful tool to analyze complex security and privacy problems. Our formalization is generic in the sense that it supports different semantical approaches. We present several semantics for attack–defense trees along with usage scenarios, and we show how to evaluate attributes.
Barbara Kordy, Sjouke Mauw, Saša Radomirović, Patrick Schweitzer

Reasoning with Past to Prove PKCS#11 Keys Secure

PKCS#11 is a widely adopted standard that defines a security API for accessing devices such as smartcards and hardware security modules. Motivated by experiments on several devices we develop an approach that allows us to formally establish security properties of keys stored on such devices. We use first-order linear time logic extended by past operators. The expressiveness of a first-order language allows us to model the security API and its features close to how it is specified while the past operators enable proof by backwards analysis. We apply this approach to prove that keys that initially have the attribute extractable set to false are secure.
Sibylle Fröschle, Nils Sommer

A Formal Analysis of Authentication in the TPM

The Trusted Platform Module (TPM) is a hardware chip designed to enable computers to achieve a greater level of security than is possible in software alone. To this end, the TPM provides a way to store cryptographic keys and other sensitive data in its shielded memory. Through its API, one can use those keys to achieve some security goals. The TPM is a complex security component, whose specification consists of more than 700 pages.
We model a collection of four TPM commands, and we identify and formalise their security properties. Using the tool ProVerif, we rediscover some known attacks and some new variations on them. We propose modifications to the API and verify our properties for the modified API.
Stéphanie Delaune, Steve Kremer, Mark D. Ryan, Graham Steel

Modeling Identity-Related Properties and Their Privacy Strength

In the last years several attempts to define identity-related properties such as identifiability, pseudonymity and anonymity have been made to analyze the privacy offered by information systems and protocols. However, these definitions are generally incomparable, making it difficult to generalize the results of their analysis. In this paper, we propose a novel framework for formalizing and comparing identity-related properties. The framework employs the notions of detectability, associability and provability to assess the knowledge of an adversary. We show how these notions can be used to specify well-known identity-related properties and classify them with respect to their logical relations and privacy strength. We also demonstrate that the proposed framework is able to capture and compare several existing definitions of identity-related properties.
Meilof Veeningen, Benne de Weger, Nicola Zannone

Semantics of Trust

The meaning assigned to the word ‘trust’ is diverse. We present a formalism that allows various interpretations of trust.
To this end, we introduce terms that specify the observations of agents, called connections. Then we apply epistemic semantics to reason about the knowledge of agents. We allow specifications of interpretations of trust in terms of facts, and analyze whether agents know the relevant facts. If agents know that a target is trustworthy under an interpretation, that agent trusts the target.
We illustrate the formalism on three specific existing interpretations.
Tim Muller

Semi-automatic Synthesis of Security Policies by Invariant-Guided Abduction

We present a specification approach of secured systems as transition systems and security policies as constraints that guard the transitions. In this context, security properties are expressed as invariants. Then we propose an abduction algorithm to generate possible security policies for a given transition-based system. Because abduction is guided by invariants, the generated security policies enforce security properties specified by these invariants. In this framework we are able to tune abduction in two ways in order to: (i) filter out bad security policies and (ii) generate additional possible security policies. Invariant-guided abduction helps designing policies and thus allows using formal methods much earlier in the process of building secured systems. This approach is illustrated on role-based access control systems.
Clément Hurlin, Hélène Kirchner

Corrective Enforcement of Security Policies

Monitoring is a powerful security policy enforcement paradigm that allows the execution of a potentially malicious software by observing and transforming it, thus ensuring its compliance with a user-defined security policy. Yet some restrictions must be imposed on the monitor’s ability to transform sequences for the enforcement to be meaningful. The intuition behind our model is that the monitor should be bounded to output a sequence that both respects the desired security property and preserves key elements of the execution’s semantics. An approximation of the sequence is executed rather than an equivalent one. This approximation must preserve the essential behavior of the sequence as intended by the user. In this paper, we propose a framework to express and study such a restriction based on partial orders. We give several examples of real-life security policies and propose monitors capable of enforcing these properties. We then turn to the question of comparing several monitors enforcing the same security property.
Raphael Khoury, Nadia Tawbi

Cryptographic Enforcement of Role-Based Access Control

Many cryptographic schemes have been designed to enforce information flow policies. However, enterprise security requirements are often better encoded, or can only be encoded, using role-based access control policies rather than information flow policies. In this paper, we provide an alternative formulation of role-based access control that enables us to apply existing cryptographic schemes to core and hierarchical role-based access control policies. We then show that special cases of our cryptographic enforcement schemes for role-based access control are equivalent to cryptographic enforcement schemes for temporal access control and to ciphertext-policy and key-policy attribute-based encryption schemes. Finally, we describe how these special cases can be extended to support richer forms of temporal access control and attribute-based encryption.
Jason Crampton

A Calculus for the Analysis of Wireless Network Security Protocols

We propose a timed broadcasting calculus for wireless systems. The operational semantics of our calculus is given both in terms of a Reduction Semantics and in terms of a Labelled Transition Semantics. We prove that the two semantics coincide. The labelled transition system is used to derive a standard notion of (weak) bi-similarity which is proved to be a congruence. We use our simulation theory to adapt Gorrieri and Martinelli’s tGNDC scheme to investigate, in our setting, the safety of non-trivial wireless network security protocols.
Francesco Ballardin, Massimo Merro

Analysis of a Receipt-Free Auction Protocol in the Applied Pi Calculus

We formally study two privacy-type properties for online auction protocols: bidding-price-secrecy and receipt-freeness. These properties are formalised as observational equivalences in the applied π calculus. We analyse the receipt-free auction protocol by Abe and Suzuki. Bidding-price-secrecy of the protocol is verified using ProVerif, whereas receipt-freeness of the protocol is proved manually.
Naipeng Dong, Hugo Jonker, Jun Pang


Weitere Informationen

Premium Partner