Strengthening and formally verifying privacy in identity management systems

In a digital world, users’ Personally Identifiable Information (PII) is normally managed with a system called an Identity Management System (IMS). There are many types of IMSs. There are situations when two or more IMSs need to communicate with each other (such as when a service provider needs to obtain some identity information about a user from a trusted identity provider). There could be interoperability issues when communicating parties use different types of IMS. To facilitate interoperability between different IMSs, an Identity Meta System (IMetS) is normally used. An IMetS can, at least theoretically, join various types of IMSs to make them interoperable and give users the illusion that they are interacting with just one IMS. However, due to the complexity of an IMS, attempting to join various types of IMSs is a technically challenging task, let alone assessing how well an IMetS manages to integrate these IMSs. The first contribution of this thesis is the development of a generic IMS model called the Layered Identity Infrastructure Model (LIIM). Using this model, we develop a set of properties that an ideal IMetS should provide. This idealized form is then used as a benchmark to evaluate existing IMetSs. Different types of IMS provide varying levels of privacy protection support. Unfortunately, as observed by Jøsang et al (2007), there is insufficient privacy protection in many of the existing IMSs. In this thesis, we study and extend a type of privacy enhancing technology known as an Anonymous Credential System (ACS). In particular, we extend the ACS which is built on the cryptographic primitives proposed by Camenisch, Lysyanskaya, and Shoup. We call this system the Camenisch, Lysyanskaya, Shoup - Anonymous Credential System (CLS-ACS). The goal of CLS-ACS is to let users be as anonymous as possible. Unfortunately, CLS-ACS has problems, including (1) the concentration of power to a single entity - known as the Anonymity Revocation Manager (ARM) - who, if malicious, can trivially reveal a user’s PII (resulting in an illegal revocation of the user’s anonymity), and (2) poor performance due to the resource-intensive cryptographic operations required. The second and third contributions of this thesis are the proposal of two protocols that reduce the trust dependencies on the ARM during users’ anonymity revocation. Both protocols distribute trust from the ARM to a set of n referees (n > 1), resulting in a significant reduction of the probability of an anonymity revocation being performed illegally. The first protocol, called the User Centric Anonymity Revocation Protocol (UCARP), allows a user’s anonymity to be revoked in a user-centric manner (that is, the user is aware that his/her anonymity is about to be revoked). The second protocol, called the Anonymity Revocation Protocol with Re-encryption (ARPR), allows a user’s anonymity to be revoked by a service provider in an accountable manner (that is, there is a clear mechanism to determine which entity who can eventually learn - and possibly misuse - the identity of the user). The fourth contribution of this thesis is the proposal of a protocol called the Private Information Escrow bound to Multiple Conditions Protocol (PIEMCP). This protocol is designed to address the performance issue of CLS-ACS by applying the CLS-ACS in a federated single sign-on (FSSO) environment. Our analysis shows that PIEMCP can both reduce the amount of expensive modular exponentiation operations required and lower the risk of illegal revocation of users’ anonymity. Finally, the protocols proposed in this thesis are complex and need to be formally evaluated to ensure that their required security properties are satisfied. In this thesis, we use Coloured Petri nets (CPNs) and its corresponding state space analysis techniques. All of the protocols proposed in this thesis have been formally modeled and verified using these formal techniques. Therefore, the fifth contribution of this thesis is a demonstration of the applicability of CPN and its corresponding analysis techniques in modeling and verifying privacy enhancing protocols. To our knowledge, this is the first time that CPN has been comprehensively applied to model and verify privacy enhancing protocols. From our experience, we also propose several CPN modeling approaches, including complex cryptographic primitives (such as zero-knowledge proof protocol) modeling, attack parameterization, and others. The proposed approaches can be applied to other security protocols, not just privacy enhancing protocols.

Where money and meanings meet : theorizing the emergence of new values in media and education

Recent developments in technology, globalization, and consumer activism have challenged the "broadcasting model" of natonally bounded, vertically integrated, monopolistic, expert-paradigm media industries, dedicated to supplying leisure entertainment to more or less passive consumers. Instead, attention has turned to globally traded formats, social network markets, consumer-created content, multiplatform "publication," and a semiotic long tail where niche representations can be as valuable as blockbusters. Such chenges are just as much a challenge to education as they are to business models. And education, both formal and informal, is a dynamic agent in these processes, participation, and creative content require a rethink of "studies" just as much as of "media."

Risky business : making decisions off the cuff

In line with accepted decision making theory, individuals engage in rational decision making. Decisions made under conditions of bounded rationality may have serious adverse consequences. Employees making decisions on behalf of their employer are often faced with situations where perfect and complete information is not available, and time is limited. Under such conditions, we posit that employees will make decisions that are increasingly bounded. At its most extreme neither time nor information is available to make a decision and rational decision making, bounded or not, reaches its limits. Many authors suggest that this is the point at which improvisation takes place. Although opinion in the literature is mixed regarding the efficacy of improvised decisions, we argue that improvised decisions place the organisation at considerable risk and as a consequence are undesirable.

Multi-version documents : A digitisation solution for textual cultural artefacts

Textual cultural heritage artefacts present two serious problems for the encoder: how to record different or revised versions of the same work, and how to encode conflicting perspectives of the text using markup. Both are forms of textual variation, and can be accurately recorded using a multi-version document, based on a minimally redundant directed graph that cleanly separates variation from content.

Social infrastructure planning and sustainable community : example from south east Queensland, Australia

Social infrastructure and sustainable development represent two distinct but interlinked concepts bounded by a geographic location. For those involved in the planning of a residential development, the notion of social infrastructure is crucial to the building of a healthy community and sustainable environment. This is because social infrastructure is provided in response to the basic needs of communities and to enhance the quality of life, equity, stability and social well being. It also acts as the building block to the enhancement of human and social capital. While acknowledging the different levels of social infrastructure provision from neighbourhood, local, district and sub-regional levels, past evidence has shown that the provision at neighbourhood and local level and are affecting well-being of residents and the community sustainability. With intense physical development taking place in Australia's South East Queensland (SEQ) region, local councils are under immense pressure to provide adequate social and community facilities for their residents. This paper shows how participation-oriented, need-sensitive Integrated Social Infrastructure Planning Guideline is used to offer a solution for the efficient planning and provision of multi-level social infrastructure for the SEQ region. The paper points out to the successful implementation of the guideline for social infrastructure planning in multiple levels of spatial jurisdictions of Australia's fastest growing region.

Towards defining semantic foundations for purpose-based privacy policies

We define a semantic model for purpose, based on which purpose-based privacy policies can be meaningfully expressed and enforced in a business system. The model is based on the intuition that the purpose of an action is determined by its situation among other inter-related actions. Actions and their relationships can be modeled in the form of an action graph which is based on the business processes in a system. Accordingly, a modal logic and the corresponding model checking algorithm are developed for formal expression of purpose-based policies and verifying whether a particular system complies with them. It is also shown through various examples, how various typical purpose-based policies as well as some new policy types can be expressed and checked using our model.

Overview of the INEX 2010 focused relevance feedback track

The INEX 2010 Focused Relevance Feedback track offered a refined approach to the evaluation of Focused Relevance Feedback algorithms through simulated exhaustive user feedback. As in traditional approaches we simulated a user-in-the loop by re-using the assessments of ad-hoc retrieval obtained from real users who assess focused ad-hoc retrieval submissions. The evaluation was extended in several ways: the use of exhaustive relevance feedback over entire runs; the evaluation of focused retrieval where both the retrieval results and the feedback are focused; the evaluation was performed over a closed set of documents and complete focused assessments; the evaluation was performed over executable implementations of relevance feedback algorithms; and �finally, the entire evaluation platform is reusable. We present the evaluation methodology, its implementation, and experimental results obtained for nine submissions from three participating organisations.

Dryness : the aesthetic condition of landscape design in Australia

Despite having a band of greenness around the edge, Australia is fundamentally a dry country. Australian vegetation has developed a high range of mechanisms to cope with the dryness, but after 200 years of white settlement, Australians still have not really come to terms with the real dryness of their country, and still exploit European paradigms that attempted to transplant European aesthetic conditions, greenness, to the brown land of Australia. Australia is going through serious water shortages that are still and will continue with the Greenhouse effect, to become a major factor in the location and extent of urbanisation, and also Australia's carrying capacity. While such aesthetic concerns might seem ornamental, until the population changes its attitude to the real condition of the country, it will keep using water and operating unsustainably. The design of the public landscape, however, offers the opportunity to contribute to changing people's aesthetic perception of the country, which might in turn help to redirect their water use practices. This essay develops a language for discussion dryness based around the experiences of water. After having developed this sensibility it then discusses a range of different approaches that landscape design in Australia has used to try to develop geographically appropriate design languages, including the Bush Garden and the Mediterranean Garden. It then discusses four design projects, one from the 1970's, the other three from the last five years that demonstrate what such an aesthetic might look like.

Soundness of workflow nets with reset arcs

Petri nets are often used to model and analyze workflows. Many workflow languages have been mapped onto Petri nets in order to provide formal semantics or to verify correctness properties. Typically, the so-called Workflow nets are used to model and analyze workflows and variants of the classical soundness property are used as a correctness notion. Since many workflow languages have cancelation features, a mapping to workflow nets is not always possible. Therefore, it is interesting to consider workflow nets with reset arcs. Unfortunately, soundness is undecidable for workflow nets with reset arcs. In this paper, we provide a proof and insights into the theoretical limits of workflow verification.

Managing process model complexity via concrete syntax modifications

While Business Process Management (BPM) is an established discipline, the increased adoption of BPM technology in recent years has introduced new challenges. One challenge concerns dealing with the ever-growing complexity of business process models. Mechanisms for dealing with this complexity can be classified into two categories: 1) those that are solely concerned with the visual representation of the model and 2) those that change its inner structure. While significant attention is paid to the latter category in the BPM literature, this paper focuses on the former category. It presents a collection of patterns that generalize and conceptualize various existing mechanisms to change the visual representation of a process model. Next, it provides a detailed analysis of the degree of support for these patterns in a number of state-of-the-art languages and tools. This paper concludes with the results of a usability evaluation of the patterns conducted with BPM practitioners.

Why teaching about Asia matters in higher education

I commence this opinion piece with specific reference to the Gillard Government's decision to cut funding for the Australian Learning and Teaching Council (ALTC)in 2011. I then consider impact of this decision on quality teaching in higher education with specific reference to Studies of Asia. In particular, I reflect on the teaching of Asian languages and cultures in Australia since the 1970 Auchmuty report, and conclude that despite the efforts of policy makers, not much has really changed. In doing so, I emphasise the importance of quality teaching in higher education for inspiring students to challenge their cultural assumptions and to prompt them to develop new views of the world.

Policy filtering with XACML

This paper presents a modified approach to evaluate access control policy similarity and dissimilarity based on the proposal by Lin et al. (2007). Lin et al.'s policy similarity approach is intended as a filter stage which identifies similar XACML policies that can be analysed further using more computationally demanding techniques based on model checking or logical reasoning. This paper improves the approach of computing similarity of Lin et al. and also proposes a mechanism to calculate a dissimilarity score by identifying related policies that are likely to produce different access decisions. Departing from the original algorithm, the modifications take into account the policy obligation, rule or policy combining algorithm and the operators between attribute name and value. The algorithms are useful in activities involving parties from multiple security domains such as secured collaboration or secured task distribution. The algorithms allow various comparison options for evaluating policies while retaining control over the restriction level via a number of thresholds and weight factors.

The concealed difficulties of aligning CRE decisions to corporate goals

Realisation of the importance of real estate asset strategic decision making has inspired a burgeoning corporate real estate management (CREM) literature. Much of this criticises the poor alignment between strategic business direction and the ‘enabling’ physical environment. This is based on the understanding that corporate real estate assets represent the physical resource base that supports business, and can either complement or impede that business. In the hope of resolving this problem, CRE authors advocate a deeper integration of strategic and corporate real estate decisions. However this recommendation appears to be based on a relatively simplistic theoretical approach to organization where decision-making tends to be viewed as a rationally managed event rather than a complex process. Defining decision making as an isolated event has led to an uncritical acceptance of two basic assumptions: ubiquitous, conflict-free rationality and profit maximisation. These assumptions have encouraged prescriptive solutions that clearly lack the sophistication necessary to come to grips with the complexity of the built and organizational environment. Alternatively, approaching CREM decision making from a more sophisticated perspective, such as that of the “Carnegie School”, leads to conceptualise it as a ‘process’, creating room for bounded rationality, multiple goals, intra-organizational conflict, environmental matching, uncertainty avoidance and problem searching. It is reasonable to expect that such an approach will result in a better understanding of the organizational context, which will facilitate the creation of organizational objectives, assist with the formation of strategies, and ultimately will aid decision.

Regrounding critical literacy : representation, facts and reality

A discussion of the pivotal theoretical and practical issue in the teaching of critical literacies: the relationship between representation and material social, economic and ecosystemic reality. The argument here is that models of critical literacy are contingent upon a principled and grounded pursuit of material social, economic and ecological realities 'outside' of textual representation per se.

Soundness of workflow nets: classification, decidability, and analysis

Workflow nets, a particular class of Petri nets, have become one of the standard ways to model and analyze workflows. Typically, they are used as an abstraction of the workflow that is used to check the so-called soundness property. This property guarantees the absence of livelocks, deadlocks, and other anomalies that can be detected without domain knowledge. Several authors have proposed alternative notions of soundness and have suggested to use more expressive languages, e.g., models with cancellations or priorities. This paper provides an overview of the different notions of soundness and investigates these in the presence of different extensions of workflow nets.We will show that the eight soundness notions described in the literature are decidable for workflow nets. However, most extensions will make all of these notions undecidable. These new results show the theoretical limits of workflow verification. Moreover, we discuss some of the analysis approaches described in the literature.