Security and Trust Management

This paper examines the necessity to integrate Economic Theories and Trust Theories with Knowledge Science for trustworthy service automation in modern day society’s technology-driven environment. Current demands for open user-centric distributed service systems far outweigh the capabilities of existing systems in application areas such as health care, e-business, and consumer-centric power and water distribution systems. The basis of service transactions, whether in traditional market place or on-line system, is trust and lack of trust will have diminishing effect on the economic value. It is essential to identify user perspectives and relate their social psychology to meaningful trust determinants in the system to be automated. Since the systems are typically large, distributed, and deal with many heterogeneous collection of sensory devices and actuators that are specific to each service domain, it is necessary that the experts of the application domain and system developers share their knowledge and wisdom in the creation of the system. Sharing knowledge requires trust, and using the acquired knowledge requires creativity, born out of tacit knowledge, to go beyond risks. Motivated by this triangular web of Economics, Trust, and Knowledge that impacts on consumer-centric service automation, this paper explores their interesting connections, explains the different kinds of trust to be distilled from it, and identifies the design stages where the appropriate trust determinants are to be fostered in order to achieve a dependable service automation system.

Privacy by design will become a legal obligation in the European Community if the Data Protection Regulation eventually gets adopted. However, taking into account privacy requirements in the design of a system is a challenging task. We propose an approach based on the specification of privacy architectures and focus on a key aspect of privacy, data minimisation, and its tension with integrity requirements. We illustrate our formal framework through a smart metering case study.

There have been many proposals for access control models and authorization policy languages, which are used to inform the design of access control systems. Most, if not all, of these proposals impose restrictions on the implementation of access control systems, thereby limiting the type of authorization requests that can be processed or the structure of the authorization policies that can be specified. In this paper, we develop a formal characterization of the features of an access control model that imposes few restrictions of this nature. Our characterization is intended to be a generic framework for access control, from which we may derive access control models and reason about the properties of those models. In this paper, we consider the properties of monotonicity and completeness, the first being particularly important for attribute-based access control systems. XACML, an XML-based language and architecture for attribute-based access control, is neither monotonic nor complete. Using our framework, we define attribute-based access control models, in the style of XACML, that are, respectively, monotonic and complete.

Crampton and Sellwood recently introduced a variant of relationship-based access control based on the concepts of relationships, paths and principal matching, to which we will refer as the RPPM model. In this paper, we show that the RPPM model can be extended to provide support for caching of authorization decisions and enforcement of separation of duty policies. We show that these extensions are natural and powerful. Indeed, caching provides far greater advantages in RPPM than it does in most other access control models and we are able to support a wide range of separation of duty policies.

With the increasing popularity of Bitcoin, a digital decentralized currency and payment system, the number of malicious third parties attempting to steal bitcoins has grown substantially. Attackers have stolen bitcoins worth millions of dollars from victims by using malware to gain access to the private keys stored on the victims’ computers or smart phones. In order to protect the Bitcoin private keys, we propose the use of a hardware token for the authorization of transactions. We created a proof-of-concept Bitcoin hardware token: BlueWallet. The device communicates using Bluetooth Low Energy and is able to securely sign Bitcoin transactions. The device can also be used as an electronic wallet in combination with a point of sale and serves as an alternative to cash and credit cards.

Non-interference is a security property which states that improper information leakages due to direct and indirect flows have not occurred through executing programs. In this paper we investigate a game semantics based formulation of non-interference that allows to perform a security analysis of closed and open procedural programs. We show that such formulation is amenable to automated verification techniques. The practicality of this method is illustrated by several examples, which also emphasize its advantage compared to known operational methods for reasoning about open programs.

This paper proposes a framework for regulating data sharing on Android mobile devices. In our approach, the user downloads a copy of the data on his Android device, then the framework controls the data usage by enforcing the usage control policies which have been embedded in the data itself by the data producer. The usage control policy is based on the Usage Control model, whose main feature is to allow the usage of the downloaded data as long as conditions specified in the policy are satisfied. The proposed framework secures the data access procedure relying on both the Android security mechanisms and the introduction of Trusted Platform Module functions. The paper details the proposed framework, presents some preliminary results from the prototype that has been developed, and discusses the security of the prototype.

We propose in this paper a formal model for soft enforcement, where a decision-maker is influenced towards a decision, rather than forced to select that decision. This novel type of enforcement is particularly useful when the policy enforcer cannot fully control the environment of the decision-maker, as we illustrate in the context of attribute-based access control, by limiting the control over attributes. We also show that soft enforcement can improve the security of the system when the influencer is uncertain about the environment, and when neither forcing the decision-maker nor leaving them make their own selection is optimal. We define the general notion of optimal influencing policy, that takes into account both the control of the influencer and the uncertainty in the system.

Devising a successful risk mitigation plan requires estimation of risk and loss impact. However, the information security industry suffers from the problem of information asymmetry, thus leading to not-so correct estimates for risk and loss impact. Prediction markets have been found to be highly effective in the prediction of future events in several domains such as politics, sports, governance, and so on. Also, many organizations such as Google, General Electric, Hewlett Packard, and others have used prediction markets to forecast various business management issues. Based on the application of prediction markets in other domains and various types of financial markets discussed in the literature, such as macro-markets, weather derivatives and economic derivative markets, we hypothesize that: (i) a well-designed prediction market can be used for risk estimation and estimation of loss impact in information security domain. This will help the decision makers in adopting appropriate risk mitigation strategy; (ii) Prediction markets can further be useful in hedging information security risks by allowing trading of financial instruments linked to the risk of information security events. In this paper, we explore the possibility of information security market where financial and insurance-linked instruments can be traded to facilitate the mitigation of a substantial proportion (if not all) of the information security risk. We present the key design issues relevant to the market for trading of information security related financial instruments. Further, we present a risk assessment of such a market’s relevance to its usefulness in hedging information security risks.

Authorization conditions of access control policies are complex and varied as they might depend, e.g., on the current time, the position of the users, selected parts of the system state, and even on the history of the computations. Several models, languages, and enforcement mechanisms have been proposed for different scenarios. Unfortunately, this complicates the verification of safety, i.e. no permission is leaked to unauthorized users. To avoid these problems, we present an intermediate language called Action Language for Policy Specification. Two desiderata drive its definition: (i) it should support as many models and policies as possible and (ii) it should be easily integrated in existing verification systems so that robust techniques (e.g., model checking or satisfiability solving) can be exploited to safety. We argue (i) by using selected examples of access control models and policies taken from the literature. For (ii), we prove some theoretical properties of the language that pave the way to the definition of automatic translations to available verification techniques.

Intuitively, two protocols \({\mathcal P}_1\) and \({\mathcal P}_2\) are indistinguishable if an attacker cannot tell the difference between interactions with \({\mathcal P}_1\) and with \({\mathcal P}_2\). In this paper we: (i) propose an intuitive notion of indistinguishability in Maude-NPA; (ii) formalize such a notion in terms of state unreachability conditions on their synchronous product; (iii) prove theorems showing how —assuming the protocol’s algebraic theory has a finite variant (FV) decomposition– these conditions can be checked by the Maude-NPA tool; and (iv) illustrate our approach with concrete examples. This provides for the first time a framework for automatic analysis of indistinguishability modulo as wide a class of algebraic properties as FV, which includes many associative-commutative theories of interest to cryptographic protocol analysis.