Sharing of resources on the cloud can be achieved on a large scale, since it is cost effective and location independent. Despite the hype surrounding cloud computing, organizations are still reluctant to deploy their businesses in the cloud computing environment due to concerns in secure resource sharing. In this paper, we propose a cloud resource mediation service offered by cloud service providers, which plays the role of trusted third party among its different tenants. This paper formally specifies the resource sharing mechanism between two different tenants in the presence of our proposed cloud resource mediation service. The correctness of permission activation and delegation mechanism among different tenants using four distinct algorithms (activation, delegation, forward revocation, and backward revocation) is also demonstrated using formal verification. The performance analysis suggests that the sharing of resources can be performed securely and efficiently across different tenants of the cloud.

Service-oriented architecture offers a flexible paradigm for information flow among collaborating organizations. As information moves out of an organization boundary, various security concerns may arise, such as confidentiality, integrity, and authenticity that needs to be addressed. Moreover, verifying the correctness of the communication protocol is also an important factor. This paper focuses on the formal verification of the xDAuth protocol, which is one of the prominent protocols for identity management in cross domain scenarios. We have modeled the information flow of xDAuth protocol using high-level Petri nets to understand the protocol information flow in a distributed environment. We analyze the rules of information flow using Z language, while Z3 SMT solver is used for the verification of the model. Our formal analysis and verification results reveal the fact that the protocol fulfills its intended purpose and provides the security for the defined protocol specific properties, e.g., secure secret key authentication, and Chinese wall security policy and secrecy specific properties, e.g., confidentiality, integrity, and authenticity.

Mashups are a new breed of interactive web applications that aggregate and stitch together data retrieved from one or more sources to create an entirely new and innovative set of services. The paradigm is not limited to social networks and many enterprises are redesigning their business processes to create interactive systems in the form of mashups. However, protecting users' private data from unauthorized access in mashups is a challenging security problem. Existing solutions for addressing the various authorization problems are limited due to all-or-nothing policy, third party dependence and scalability issues. In this paper, we present a general permission delegation model for mashups that is fine-grained, user centric and scalable. This contribution has the following objectives: We formally specify the dependency relationships among multiple web applications. Dependency relationships are categorized on the basis of specific data items. We present an extensible reference architecture for configuring multiple web applications and a session management protocol.