Fog Computing Over IoT: A Secure Deployment and Formal Verification

Fog computing, being an extension to cloud computing has addressed some issues found in cloud computing by providing additional features, such as location awareness, low latency, mobility support, and so on. Its unique features have also opened a way toward security challenges, which need to be focused for making it bug-free for the users. This paper is basically focusing on overcoming the security issues encountered during the data outsourcing from fog client to fog node. We have added Shibboleth also known as security and cross domain access control protocol between fog client and fog node for improved and secure communication between the fog client and fog node. Furthermore to prove whether Shibboleth meets the security requirement needed to provide the secure outsourcing. We have also formally verified the protocol against basic security properties using high level Petri net.

SECTION I. Introduction

Internet of Things are basically physically inter-connected objects. All physical objects connected with each other forms an IoT network. The connected physical devices are also embedded with different software, sensors and also have network connectivity which makes them able to share and access the information. Today’s technology-oriented world has revolutionized the IoT network as each and every physical device is connected with each other. A huge number of IoT devices are connected through the internet which makes the rapid completion of different processes. A wide range of IoT applications include transportation systems, Smart homes, Smart Industries, Media, and Medical etc. The IoT network helps in the information processing and control of these applications [1].

For managing the physical objects involved in the IoT network and the connected devices, data collection and keeping it secure is the noteworthy issue. As different network devices involved in an IoT network can produce data which is too rapid and it must be processed with higher throughput. Moreover, this data volume is increasing rapidly every day and a storage solution is badly needed for managing and scaling the data proficiently. The integration of Cloud and IoT is the best possible solution. As the IoT network with different devices produce a huge amount of non-structured data while Cloud is the most actual solution to deal with the IoT data [2].

While talking about the Clout and IoT integration, the most recent advancement in the cloud Fog Computing must be considered because of its advanced features. Fog computing has trended the evolution of cloud computing by bringing the resources closer to the end-user thus results in low latency rate [3]. Fog computing has provided some advance features to the client like location awareness, mobility support, Low latency etc. However, some security threats like during the outsourcing of data also came forward with it like an external attacker might get access to the sensitive data and can expose user’s privacy [4].

Federation identity management (FIM) can be one solution that supports the implementation of secure data access in a CloudIoT network through its different Cross Domain Access Control (CDAC) protocols such as Shibboleth [5] which is an open-source platform that can be used to deploy single-sign on (SSO) between different organizations in a federation [6]. Specifically, in Shibboleth, the access control mechanism is performed by comparing the attributes provided by the identity provider (IdP). The attributes are compared against the rules defined by the service provider (SP). Shibboleth requires the deployment of an external database for accessing user data. The access request and responses are exchanged securely using Security Assertion and Markup Language (SAML) [7].

In Shibboleth, metadata is the basis for trust establishment between Shibboleth providers, as it contains the information used to identify the providers [5]. To protect the trust between different Shibboleth providers, mechanisms such as digital signatures are used [5]. For making the FogIoT secure the deployed protocol must also be vulnerability-free [7].

In this paper, we have conducted a comprehensive study on security challenges encountered during the data outsourcing between Fog Client and Fog Node. First of all, we have studied the security weaknesses that can be problematic for secure FogIoT network in context with its data security. After this, we have considered few of the security protocols which can be helpful in protecting the user’s privacy in cloud storage. We have selected Shibboleth because of its highest authentication and privacy-preserving capabilities among them. Then to prove the correctness of our selected protocol and the proposed solution we have formally verified the protocol by demonstrating system correctness against selected security-related properties.

The selected properties will be the security basics for a secure FogIoT network. Specifically, we have used the Z3 constraint solver being an efficient automated SMT (satisfiability modulo theories) solver. The Z3 solver by Microsoft Research Labs are frequently used in the analysis and verification of software systems [8], [9].

Motivation: Being a fast-growing network, IoT must be secure. After the integration of cloud and IoT, user’s data is being stored on cloud storage but to overcome the high latency ‘Fog Computing’ become an advancement in cloud computing which has brought the resources closer to the end-user. This has resolved the latency issues but created space for some serious security issues. After analyzing its security issues we came across a possible solution in CloudIoT network. The contribution of this paper includes:

• To critically analyze the Shibboleth protocol in context with CloudIoT network

• Adding an extra layer of Shibboleth protocol between Fog Client and Fog Node for authentication purposes

• To formally verify the protocol to prove the correctness of its requirement needed to make outsourcing secure

This paper is structured as follows: Section II is dedicated to the explanation of background study and the terminologies being used in this paper. Section III will debate the related work. Section IV will converse the deployment of Shibboleth in CloudIoT network. Section V will describe the Formal verification of the Shibboleth protocol. Constitution of Shibboleth’s verification will be done in Section VI. Paper will be inferred in Section VII.

SECTION II. Background Concepts, Terminologies

A. Overview of Internet of Things (IoT)

The concept of IoT in which different virtual information integrates with a different world of things to communicate with each other. Kevin Ashton has used the term Internet of Things (IoT) for the first time, which is now gaining popularity [10]. Mainly the IoT are the physical objects connected with each other forming an information flow network [2], [11]. These physical devices are connected with each other in a network with some software, sensors or network connectivity, this makes the devices share information in an IoT network [12], [13].

1) IoT Security

The growing IoT network has come forward with basic needs for making it secure. A lot of security issues have become a challenge for the IoT network. These issues may include privacy, authenticity, access control or storage and management issues [14].

B. Integration of IoT and Fog Computing

Two independent words ‘Cloud’ and ‘IoT’ have been seen evolving individually. But based on the advantages stemming from their integration they will be seen integrated in future. IoT has profited users in providing new services in real-world things for a large number of real-life consequences. On the other hand, Cloud has offered an effective solution for the management and storage of data. So this integration will introduce more opportunities for data processing, integration and securely sharing it with third parties. As IoT network cannot deal with the huge data processing effectively that’s why it needs Cloud for dealing with the user’s data storage and processing issues. We will be considering the Cloud integrated with Fog Nodes in the integration as its the most recent advancement in Cloud [15].

C. Overview of Shibboleth Protocol

Shibboleth framework basically defines a set of collaboration between its providers in order to facilitate its users with Single-sign-On and attribute exchange processes. Shibboleth system includes two basic components: (a) Service Provider (SP), and (b) Identity Provider (IdP). Service provider and Identity providers are the architectural components of Shibboleth. The aforesaid shibboleth components are also referred as Target site and Origin site respectively [16]. The Shibboleth components mutually form a federation and facilitate the user in accessing the web resources securely [17]. In order to develop the trust between service provider and identity provider, a public key is exchanged between them. User attributes that are provided by origin site are used on the target site. The decision is then made about allowing the user to access the desired source or not [18].

The identity provider or origin site is the user’s home domain and is responsible for authenticating the user’s identity. Shibboleth is not concerned with how the authentication process is done on the behalf of identity provider. The only thing that Shibboleth considers is the authentication process must be Web-based having SSO facility. The IdP has three sub-components. The sub-components of Idp are named as (a) Handle Service (HS), (b) Attribute Authority (AA), and (c) Local Authentication system (LAS) [19]. Handle Service is responsible for providing a handle to the user as a reference after the authentication of the user is done in its home domain. Attribute Authority manages user attributes and provides user attributes whenever needed or requested by the SP in order to provide access to user’s desired resource. The attribute authority is not allowed to send the attributes that have not been allowed by the user to release.

At the target site or SP, the authorization process is being performed. The authorization process depends on the attributes that origin site has asserted. The asserted attributes are then compared against the resource-related policy rules. The policy matching process will choose if the user is permitted to access the requested resource or not. Service provider comprises of two sub-components named as (a) Shibboleth Indexical Reference Establisher (SHIRE) and, (b) Shibboleth Attribute Requestor (SHAR) [20]. The SHIRE is responsible for receiving the user’s request. Besides checking user’s authentication SHIRE also forwards the user’s request to SHAR for further processing. The SHAR sends user along with the required attributes to Resource Manager for access decision.

Discovery Service (DS) is a service which SP uses to identify users home domain. The DS determine users home domain by providing the list of home domains that have been registered in that specific Federation. After the selection of home domain, user is redirected towards that address for authentication. This service is either provided directly by SP or by any other third trusted party.

There is a separate privacy preserving mechanism for users. This mechanism is responsible for inhibiting the exposure of user’s identity to the Service provider. To accomplish the goal of preserving user’s privacy the attributes provided by IdP to SP must not contain any information that exposes user’s identity. The IdP prefer to release attributes like the user belongs to a specific group i.e., the user is a student or a faculty member. Furthermore, the user also has an option to release attributes of his own choice to SP [16].

D. High Level Petrinets (HLPN)

A tool that is used for the mathematical and graphical modeling [21]. Petrinets are an auspicious tool for the description of information flow of different systems having the characteristics of concurrency, parallelism, asynchronous and non-deterministic [22]. (P,T,F) provides net structure whereas the static semantics are provided by ($\varphi $ ,R,L). The high modeling power and convenience of human have made HLPN preferable over LLPN.

A HLPN graph basically consists of two types of node sets. First is a transition and the other is Place. Flow is shown by the arcs which connect arc and places with each other. Place is a non-empty set assigned with one or more than one data types. The values in places are called tokens. Different types of tokens are there in a place like in Figure 2. P1 has $\varphi $ (P1) = Int,Bool and $\varphi $ (P2) = Char. In Figure 2 new tokens can only enter through the transition t1. Let the two nodes of HLPN $\alpha $ and $\beta $ belongs to P $\cup $ T. Node $\alpha $ is an input node of $\beta $ iff $\alpha $ and $\beta $ are connected with each other by an arc which is going from $\alpha $ towards $\beta $ such that ($\alpha $ ,$\beta $ )$\epsilon $ F. On the other side node $\alpha $ will be an output node of $\beta $ iff both are connected by an arc leading from $\beta $ to $\alpha $ such that ($\beta $ ,$\alpha $ )$\epsilon $ F. So for any node $\beta ~\epsilon $ P $\cup $ T, $\beta =\alpha ~\mid $ ($\beta $ ,$\alpha $ )$\epsilon $ F is its pre-condition while $\beta =\alpha ~\mid $ ($\alpha $ ,$\beta $ )$\epsilon $ F is the post-condition. To enable any transition its pre-condition must hold. Tokens are transferred from input place to the output place whenever a transition is fired. What we have used in this paper is the variant of the conventional Petrinets named as High level Petrinets (HLPN). This is used for the formal verification of Shibboleth protocol.

FIGURE 1.

CloudIoT Network.

FIGURE 2.

HLPN Example.

Definition 1 (HLPN)[21]:

It is a 7-tuple N = {P, T, F, $\varphi $ , R, L, M} where:

• P is a set of fixed places

• T is a set of finite transitions such that: P $\cap $ T $= \varphi $

• F is the flow relation such that: F $\subseteq $ (P $\times $ T) $\cup $ (T $\cup $ P)

• $\varphi $ is a mapping function that maps P to data types such that $\varphi $ : P $\rightarrow $ Type

• R is defined as rules that predicate logic formulas such that R: T $\rightarrow $ Formula

• L indicates the label that maps F such that L : F $\rightarrow $ Label

• $M_{0}$ shows the preliminary marking such that M : P $\rightarrow $ Token

(P, T, F) which are three very first variables. They basically provide info about the structure of Petrinets and the variables. ($\varphi $ , R, L) are providing static semantics to show that the information does not alter all over the system.

Figure 2 is illustrating an example of Petrinet having two places P = (P1, P2), transitions T = (T1, T2) and the information flows is shown F = (a, b, c, d, e, f). Each place in HLPN is containing few tokens which is for the sake of enabling adjacent transitions which means that the pre-condition must hold for the transition to be set to fire. Places containing the tokens can be of one type or it can also be the product of two different types.

Table 1 has shown the places with data mapping.

TABLE 1 Places to Data Type Mappings

E. SMT-LIB and Z3 Solver

Satisfiability modulo theories (SMT) is used for checking the accuracy of formula over some theorems [21]. It has its roots from the previous version called Boolean Satisfiability solver (SAT) [23]. A precise difference between these two is that the SMT solver checks the correctness of any formula from different theories like Bit-vector and Arithmetic as well while the other one called SAT solver checks the correctness of propositional formulas. Wide usage of SMT solver has also stepped into different fields including the deductive verification of software [24]. Furthermore, different Computer science applications which are based on planning, modeling, and generation of automated testing also consider this SMT solver as an important usable tool [25].

As trend has shifted from the verification done manually or by simulation using verification tools as mentioned in [26]. SPIN model checker was used to formally verify ad-hoc protocols. Real-time aspects of the protocol were formally verified using Wireless Adaptive Routing Protocol as done in [27]. The Author used SMT Libraries and Z3 solver to verify OSPF protocol in [28]. The Author have used SMT-Lib and Z3 Solver for the formal verification of VM-based cloud management platforms i.e., Eucalyptus, Nimbus and Open Nebula in [21].

We have also used the Z3 constraint solver, which is an effective automated SMT solver by Microsoft Research Labs. This solver is typically used in the analysis and verification of software systems. The essential verification theory for our system’s model is a theory of array. We will use the theory of array to verify the satisfiability of our model’s logical formulae [9]. The array theory is frequently used in the software modeling domain. Our work is different in the perspective that besides the formal analysis of Shibboleth protocol we have also modeled the protocol in HLPN and afterward also verified that model using SMT solver. We have selected Z3 SMT solver for the protocol verification as Z3 is currently being used as an area of research in the field of software verification. It is also an influential solver for the solution of real-world problems, especially the problems with the higher computational power [8].

F. Formal Verification

The process of ensuring correctness of the system under consideration is ‘Verification’ [29]. ‘Formal Verification’ is an application of formal methods. Formal verification is basically the mathematical technique which is further supported by different tools for verifying the system’s correctness. In software, formal methods can be used for specifying a software and to develop a precise statement about the software behavior and specifications. At the implementation level, formal methods are used to verify or refute the accuracy of a code. This verification is to prove the theorem and to find out the reasons of theorem’s failure [30]. Formal verification applies different mathematical arguments to prove the underlying system’s correctness. Formal verification is aimed to detect any type of logical or design error in the system. Being less expensive, Formal verification is now gaining popularity for verifying the software [31]. As formal methods are very active area of research nowadays so it can be used for large-scale computing systems. A different number of promising techniques and methodologies of formal verification have been invented in past few years. Formal verification in computing systems desired for a mathematical proof to show the system satisfying its intended properties or specifications [32]. Mathematical structures are used to model the system and to derive the properties of the system. Formal methods involve different techniques to verify a system. First of all, model is used to represent the possible behavior. Then the correctness requirements are stated as properties of the system. After that, the model of the underlying system is checked to know whether the specification meets the desired behavior or not [33]. In case if the system’s specification is not meeting the desired behavior the model checker will return a counter example. The counterexample will show how that error state is reached. Theorem proving and Bounded model checking are the two frequently used formal verification methods [34].

Formal methods are having following parts:

• A mathematical model of system’s behavior called specifications

• A mathematical model of system’s structure called implementation model

• Analysis of system’s model to state relationships that show that the relations hold [35]

SECTION III. Related Work

Variety of work has been done in IoT network and Fog computing for ensuring its security like, in [36]. Huang et al. [37] has proposed and implemented a model for fog computing to ensure the privacy of data in different applications. The implementation is done by using Raspberry Pi. Abdo [4] has proposed a method for the reduction of latency in a mobile cloud environment where they have made the user authentication faster to decrease the delay. Different security and privacy challenges have been discussed in [38] and the author has also proposed a scheme for focusing these security issues using bloom filters and certificates. Fog computing has played an emerging role in IoT network. Its emergence has been discussed in [39]. A survey has been done on different concepts, applications and issues in Fog computing in [3].

Nowadays Cross-domain access is gaining popularity and it’s different protocols are deployed in different organizations [40]. To ensure that the intended purpose of protocols are being fulfilled, the cross domain access protocols must be checked against their envisioned properties. In order to check the protocol’s correctness we take help of formal verification. Formal verification is an effective method to prove the protocol correctness, against some properties. In case of any issues in the system, formal verification is also aimed to target the issues to be known [41]. Many of the protocols have been exposed with different security flaws like in [42] OAuth has been verified formally to check security issues if any. Formal methods basically involve modeling, analysis, and verification of the system [43]. Formal verification has been used in finding out the flaws and thus improving the system [43]. In [44] work related to rule-based framework has been done which is dedicated to the policies of RBAC model. Needham-Schroeder, Kerberos, and TNM protocols have been analyzed by the authors in [45]. A Tool which is used in [45] is Mur-phi which is used to analyze network having a large number of topologies. Malik et al. [21] has used HLPN to model and analyze different VM based cloud management platforms.

Miculan and Urban [46] have given protocol formalization in Alice-Bob notation and also in High-Level Protocol Specification Language (HLPSL). To check security flaws and attacks author has used AVISPA which is a verification tool for the analysis of security protocols. In another study Akhawe et al. [47] has used Alloy model checker to formally verify the web security and authentication protocols. To discover out some identified or unidentified vulnerabilities of CSRF attacks author has modeled web authentication protocols which is a Kerberos based SSO web solution. The method tracked in [47] is limited to only HTTP communication.

Most of the work has been done to ensure security in Fog computing but our work is different as we have focused on more than one security issue rather addressing only one issue. We have proposed a solution which will address secure data access, user’s privacy, location privacy and authentication as well.

SECTION IV. Security Based Critical Analysis of CloudIoT

For analyzing the security issues in the integration of Fog computing and IoT network as shown in Figure 3, we have evaluated the scenario as shown in Figure. On the basis of some selected security issues. The selected security issues which we have considered are:

1. Secure Data Storage: The huge data created by IoT the client will be outsourced to Fog Node first and the user’s control over data is handed over to the Fog Node. It must be secure enough that the user’s data cannot be compromised.

2. Privacy of Users: Unauthorized access to user’s data results in privacy exposure of user. The usage pattern of some IoT services by a Fog client may result in disclosure of user’s privacy.

3. Location Privacy: The Fog client offload its tasks to nearby Fog node. This means the Fog node is aware of the Fog client’s location too. That’s why the user location must also be kept secure so that no unauthorized person can get access to it.

4. Authentication: Fog client, if want to access or outsource it’s data from its respective Fog node there must be some authentication process so that no unauthenticated person can get illegal access to the data.

All these above mentioned issues are security challenges for Fog computing and need to be addressed. When we have Integration of Fog computing and IoT network, Fog Node acts as a node between the data source and cloud. The IoT network users will be ‘Fog Client’. Fog node provides users to access or outsource their data with low latency as its located at the edge of fog client. This data access or outsourcing must be secure enough to preserve user’s privacy and integrity as well.

FIGURE 3.

FogIoT Network.

SECTION V. Shibboleth Deployment in IoT Network

As per above discussed security issues, we need some solution which can look over these security challenges by considering three highlighted issues i.e., secure data storage, privacy of users, location privacy, and authentication. We have proposed to add Shibboleth between Fog Client and Fog Node for secure data access, data outsourcing and also for preserving user’s privacy. As Shibboleth is one of the most widely used security protocol which focuses on authentication and user’s privacy. That’s why its the best possible solution to overcome the highlighted security challenges in the CloudIoT scenario. Following are the Shibboleth’s security based properties which have made Shibboleth a best fit in this scenario.

1. Integrity It will overcome the data storage issues in Fog computing by protecting the integrity of user’s data. As in Shibboleth, every entity has a metadata file which contains all the information of registered entities for preventing the unauthenticated person from accessing user’s data.

2. Authentication It will make possible the data access only to authenticated users for securing the data. As Shibboleth works by authenticating each user before giving access.

3. Privacy Fog client and Fog node will be given unique ID by Shibboleth. This will hide user’s original identity and protects the privacy as well.

The proposed scenario is shown in Figure 4 and the workflow is as follows:

1. If a Fog client wants to access or outsource its data to nearby Fog Node, Fog Client will send a request to the Service Provider (SP) of Shibboleth

2. SP of Shibboleth will then forward the request of Fog client to its Discovery Service (DS)

3. DS will ask for requested Fog node’s assigned unique ID from the requester Fog client

4. Fog client will send the Fog node’s ID to which it wants to outsource access data

5. DS will send the received Fog node’s credentials

6. SP will then ask the respective Fog node to authenticate Fog client whether it belongs to this Fog node or not

7. Fog node will ask the Fog client to enter its credentials for authentication purposes

8. Fog client will authenticate itself by giving the authentication credentials to Fog node

9. Fog node will send the authentication results to SP for further decision

10. Based on received authentication results SP will accept/decline the Fog client’s request to access/outsource it’s data to specific Fog node

In the above scenario, firstly Fog Nodes and their related Fog Clients will be registered with a unique ID in Shibboleth’s metadata. This will protect the user’s data from an unauthorized person by ensuring the authentication process before accessing/outsourcing data. In this section we have explained the proposed scenario which will ensure the security and privacy of users by limiting their data access to authorized users only. Now to prove the correctness of above mentioned security properties of Shibboleth and to further understand its working we have formally verified the protocol to conclude strength and weaknesses of this proposed scenario.

FIGURE 4.

Shibboleth deployment in FogIoT Network.

SECTION VI. Formal Verification of Shibboleth Protocol

A. Workflow of Shibboleth Architecture

The architectural entities of Shibboleth are shown in Figure 5. Shibboleth has four sub-components on its Origin site: (a) The Handle Service (HS), (b) Local Authentication System (LAS). The HS which is responsible for providing the handle as a reference for the user. The authentication of user at home domain is done using authentication system called Local Authentication System (LAS). The handle is used by SHAR (a sub-component of SP) as it contains the URL of attribute authority. The SHAR uses the URL of AA to redirect the user towards AA for fetching user’s attributes. Handle also helps AA to identify the users home domain and then provide its attributes to SHAR of SP.

FIGURE 5.

Shibboleth Architecture [48].

FIGURE 6.

HLPN model of Shibboleth.

FIGURE 7.

Property 1.

FIGURE 8.

Property 2.

FIGURE 9.

Property 3.

FIGURE 10.

Verification Results of Shibboleth Protocol.

On the Target site, three sub-components of SP are serving: (a) SHIRE, (b) SHAR, and (c) Resource Manager (RM). User’s request is firstly being monitored by SHIRE. If the user is not authenticated i.e., it does not have that handle (reference) it is required to go back to his home domain and return after obtaining handle from the IdP. The SHAR then uses that handle to obtain the required user attributes from AA of his home domain. The aforesaid attributes are then used by RM to make a decision of allowing access to the desired resource.

The workflow of Shibboleth architecture is illustrated in the following step by step description:

1. First step involves the navigation of user by using his browser to access a secure resource. When user knows that the resource is permissible for to access. User sends access request to SHIRE of SP to access the resource.

2. Shibboleth’s sub-component SHIRE located on SP checks the presence of handle with the user’s request. If there is handle attached with the user’s request it means the user is authenticated. In the absence of handle, the user needs to be authenticated first. So the user is redirected next to Discovery Service (DS).

3. The DS shows a list of registered home domains to the user. User has to select his related home domain from the shown list of home domains.

4. After the selection of home domain from the shown list the user’s returns back to Discovery service.

5. From DS the user’s Idp_ID is sent to the SP.

6. From SP the user’s credentials are redirected towards that IdP for authentication.

7. IdP asks the user to enter the credentials of his home domain.

8. If the provided credentials by the user are correct HS generates an opaque handle (ultimately a session identifier). This handle is then attached to the user request. Now user is sent back towards SHIRE of SP.

9. The SHIRE validates the handle. In case of successful validation, it sends the user along with that handle towards the SHAR. The handle contains user’s home address as well as Attribute Authority URL. Then SHAR uses the handle to know the URL of user’s home domain and AA. Then SHAR sends the user to get the required attributes from the AA of user’s home domain. The Attribute authority receives the request and checks the attributes which user has allowed for release. It then send back the user’s required credentials towards SHAR. Now SHAR send user along with its attributes towards Resource Manager. The RM matches the user attributes with the published policy. Based on the decision made by the Resource Manager access is provided. If the policy matching is successful user is permitted to access the resource. Otherwise, the user’s request is declined.

B. System Model of Shibboleth

System model helps in understanding the working and information processing of the system. We have also provided the system model of Shibboleth to better understand the protocol.

Let $U_{r}$ be the user sending a Request {$R_{u}$ }. The $R_{u}$ must contain following set of attributes:\begin{equation} R_{u}=\{U_{r}(n), U_{r}(e), U_{r}(url), U_{r}(Res_{loc})\}, \end{equation} where $U_{r}(n)$ is the name of the $U_{r}$ sending the request, $U_{r}(e)$ is the email of $U_{r}$ , $U_{r}(url)$ is the location from where the $U_{r}$ is sending request and $U_{r}(Res_{loc})$ is the location of the resource which the $U_{r}$ wants to access. SHIRE receives the request $R_{u}$ coming from the user $U_{r}$ . The SHIRE accepts the $R_{u}$ if it contains authentication handle {$h_{auth}$ } along with the other attributes mentioned in (1), where $h_{auth}$ is an authentication handle. The authentication of user can be calculated as follows:\begin{equation} Authentication(U_{r}) = \begin{cases} successful & \text {if}~ h_{auth}\in R_{u}\\ failure & \text {if} ~ h_{auth}\notin R_{u}. \end{cases} \end{equation} If $R_{u}$ contains $h_{auth}$ then the authentication is successful. If the authentication is successful then $R_{u}$ must contain following attributes:\begin{equation} R_{u}=\{U_{r}(n), U_{r}(e), U_{r}(url), U_{r}(Res_{loc}), h_{auth}\}. \end{equation} After authentication check, there are two possible conditions for redirection of $U_{r}$ which is calculated as:\begin{equation} Redirection(U_{r}) = \begin{cases} Redr_{SHAR} & \text {if} ~ h_{auth}\in R_{u}\\ Redr_{DS} & \text {if} ~ h_{auth}\notin R_{u}. \end{cases} \end{equation} Let $U_{r}'$ be the user that contains $h_{auth}$ in its $R_{u}$ . In that case the $U_{r}$ is redirected towards SHAR as in (4). SHAR checks the user’s attributes contained in $R_{u}$ . For getting any further attributes SHAR send $U_{r}'$ towards AA. After getting requested attributes $U_{r}$ is sent back towards SHAR. Now the user $U_{r}$ be ${U}_{r_{i}}$ as its $R_{u}$ contains some additional attributes, as depicted in (5).\begin{equation} {U}_{r_{i}} = R_{u}+add({U}_{r_{att}}), \end{equation} where $R_{u}$ contains the set of $U_{r}$ attributes and $add({U}_{r_{att}})$ are the additional attributes which SHAR has requested from AA.

On the other hand, if $h_{auth}$ is not present in $R_{u}$ then the redirection is towards DS, as in (4). At DS, $U_{r}$ is given a list of home domains to select his home domain (HD). After selection of home domain $U_{r}$ is redirected towards that selected home domain. The authentication of $U_{r}$ done at home domain as follows:\begin{equation} Auth_{u_{i}}^{DS} = \begin{cases} success & \text {if}~ U_{r}{(n)} \in HD\\ failure & \text {if}~ U_{r}{(n)}\notin HD. \end{cases} \end{equation} In case of failure as in (6), $U_{r}$ is sent back without any $h_{auth}$ . If the authentication is successful $U_{r}$ will be given $h_{auth}$ as a reference. Now $R_{u}$ will be sent towards SHIRE, as in (3). Then the process explained in (5) will be repeated. Here the execution of both processes i.e, success and failure will reach a common point where the attributes of ${U}_{r_{i}}$ contained in $R_{u}$ will be matched with the defined policies. These policies will decide whether the user with these attributes are allowed to access the resource or not. This is shown in (7).\begin{equation} RR = \begin{cases} success & \text {if}~ R_{u} \in P_{RR} \\ failure & \text {if}~ R_{u} \notin P_{RR}. \end{cases} \end{equation} Here $P_{RR}$ is the defined policy which is matched against the $U_{r}$ attributes for releasing the resource requested by $U_{r}$ .

In our research, we have used bounded model checking technique to verify the system using SMT Libraries and Z3 solver.

HLPN model for the initiation of cross-domain access through Shibboleth protocol is revealed in Figure 3. As per the definition of HLPN, it is a 7-tuple N = {P, T, F, $\varphi $ , R, L, M}. The initial step for modeling a system is to define the Places (P) and the data types associated with them.

In the HLPN model shown in Figure 3 there are 12 places in Shibboleths HLPN model: User, SHIRE, DS, LAS, UDB, HS, SHAR, AA, RM, RRP, RR and Dead state. In Shibboleth, cross-domain access starts when a user requests for resource access to SHIRE of SP. The SHIRE is basically there to check whether the user is authenticated or not. In other words, it checks if the handle is attached, the user is an authenticated one. If there is handle in user’s request, the user is sent directly to SHAR of SP where SHAR checks the necessary attributes. To get any additional attributes needed SHAR redirects the user along with attribute request to Attribute Authority of IdP and the URL of AA is taken from the user’s handle. Attribute Authority respond back with the attributes that user had allowed to release. The aforesaid attributes along with the user request is sent to RM where after policy matching a decision is made to accept or decline the request. On the other side, if there is no handle attached with the user request, SHIRE redirects the user towards DS. Home domain selection is performed on Discovery service by the user and is then redirected towards the selected home domain for authentication purpose. On IdP side user is firstly authenticated by LAS and after successful authentication user is provided handle as a reference of authentication from his home domain and sent back to SP. From there user is sent to SHAR and further process repeats as in the later scenario.

Table 2 is dedicated to the explanation of names and mappings of P. Detailed workflow of Shibboleth had been discussed in section II. In this section, we will model and verify the details of each and every step in the protocol. Furthermore, information flow will also be defined in the form of equations. Set of transitions of our HLPN model is given by the following set T = {Start, Access-Req,Handle-s, Handle-att, Reg-info, U-auth, Reg-info, Reg-info, Handle-f, Reg-info, Ask for Attributes, Redirect U-att, Reg-info, Policy-match, Reg-info, End}.

TABLE 2 Places and Mappings of Shibboleth Protocol

TABLE 3 Data Types Used in Shibboleth Protocol

*Numbers used in the below equations are showing the attributes as given in Table 4, can be understood by following the sequence of attributes in the table.\begin{align}&\mathbf {R}(Access Req) : \forall {ur} \epsilon {UReq} ,\quad \forall {At} \epsilon {U-Att} \mid \notag \\&\quad {At}[{6}]:= {ur}[{1}] \wedge {At}[{7}]:= {ur}[{2}] \wedge {At}[{10}]:= {ur}[{4}]\notag \\&\quad \Rightarrow {U-Att'} \cup \{{At}[{4}], {At}[{6}], {At}[{7}], {At}[{8}],{At}[{10}]\}\qquad \end{align}

TABLE 4 Execution Time of Security Properties

The user requesting SHIRE of SP for accessing any resource is depicted in equation (8), in which the user is requesting to access the desired resource. User is sending its attributes like user name and URL/Browser for the authentication process to be completed.\begin{align}&\mathbf {R}(handle-s) : \forall {U-cr} \epsilon {U-cr-handle} ,\notag \\&\quad \forall {Uc} \epsilon {U-cr}\mid \notag \\&\quad \Rightarrow {Ucr-h}[{10}] \neq {NULL} \notag \\&\quad {Uc}[{1}]:={Ucr-h}[{1}] \wedge {Uc}[{2}]:={Ucr-h}[{2}]\notag \\&\quad \wedge {Uc}[{3}]:= {Ucr-h}[{3}] \wedge {Uc}[{4}]:={Ucr-h}[{4}] \wedge {Uc}[{6}]\notag \\&\quad :={Uc}[{6}] \wedge {Uc}[{6}]\notag \\&\quad :={Ucr-h}[{8}] \wedge {Uc}[{8}]:={Ucr-h}[{10}]\notag \\&\quad \Rightarrow {U-Cr'}={U-Cr} \cup \{{Uc}[{1}],{Uc}[{2}],{Uc}[{3}],{Uc}[{4}],\notag \\&\quad {Uc}[{6}],{Uc}[{7}], {Uc}[{8}]\}\quad \end{align}

In case if user’s request contains the handle (reference) of authentication than the user is redirected directly to SHAR for further processing towards resource access as shown in Equation (9).\begin{align}&\mathbf {R}(handle-f) : \forall {Ucr-h} \epsilon {U-cr-handle} ,\notag \\&\quad \forall {Isr} \epsilon {Idp-sel-req}\mid \notag \\&\quad \Rightarrow {Ucr-h}[{10}]={NULL}\wedge {Ucr-h}[{11}]={Isr}[{1}]\notag \\&\quad \wedge {Ucr-h}[{1}]={Isr}[{4}] {Isr}[{6}]\notag \\&\quad :={Ucr}[{6}] \wedge {Isr}[{7}]:={Ucr}[{1}] \notag \\&\quad \Rightarrow {Idp-sel-req'}={Idp-sel-req}\cup \{{Uc}[{1}],{Uc}[{2}],\notag \\&\quad {Uc}[{3}],{Uc}[{4}],{Uc}[{6}],{Uc}[{7}],{Uc}[{8}]\} \end{align}

Equation (10) describes the flow in which if the user’s request does not contains the authentication handle the user is redirected towards DS to get itself authenticated from its home domain.\begin{align}&\mathbf {R}(Ask for attributes): \forall {CR}\epsilon {Cr-req} ,\quad \forall {RR} \epsilon {Red-Req}\mid \notag \\&\quad {RR}[{6}]:={CR}[{6}] \wedge {RR[{5}]}:={CR}[{7}]\wedge {RR}[{7}]\notag \\&\quad :={Proxy(CR[{6}])} \notag \\&\quad \Rightarrow {Rdr-Req'}=Rdr-Req\cup \{{RR}[{5}],{RR}[{6}],{RR}[{7}]\}\notag \\ {}\end{align} Equation (11) is depicting the flow in which after the confirmation of authentication handle, user is redirected directly to SHAR. From SHAR, user is redirected towards the attribute authority of it’s home domain for getting user’s attributes for accessing the desired resource.\begin{align}&\mathbf {R}(Redirect u-att): \forall {RA}\epsilon {R-Att} ,\quad \forall {UA} \epsilon {U-Att}\mid \notag \\&\quad {UA}[{4}]:={RA}[{3}] \wedge {UA}[{5}]:={RA}[{4}] \wedge {UA}[{6}]:={RA}[{6}]\notag \\&\quad \Rightarrow {U-Att'}=U-Att\cup \{{UA}[{4}],{UA}[{5}], {UA}[{6}]\} \end{align} The protocol flow in which attributes allowed by the user for release are sent back to SP for access grant to user by Resource Manager is shown in equation (12).\begin{align}&\mathbf {R}(Policy match): \forall {UC}\epsilon {U-Cr} ,\quad \forall {UA} \epsilon {U-att}\mid \notag \\&\quad {UA}[{1}]:={UC}[{2}] \wedge {UA}[{2}]:={UC}[{6}] \wedge {UA}[{3}]:={UC}[{5}] \notag \\&\quad \Rightarrow {U-att'}=U-att\cup \{{UA}[{1}],{UA}[{2}], {UA}[{3}]\} \end{align} The flow in which after getting the user’s attributes is shown in equation (13). After getting attributes Resource manager matches policy to choose whether to allow access to user or to reject.\begin{align}&\mathbf {R}(User Auth): \forall {UC}\epsilon {U-Cr} ,\quad \forall {Cc} \epsilon {Cr-check}\mid \notag \\&\quad {Cc}[{1}]:={UC}[{6}]\wedge {Cc}[{3}]:={UC}[{7}] \notag \\&\quad \Rightarrow {Cr-check'}=Cr-check\cup \{{Cc}[{1}],{Cc}[{3}]\}\qquad \end{align} User has been authenticated by the authentication system of its home domain and is shown in equation (14).\begin{align}&\mathbf {R}(Handle-att): \forall {CR}\epsilon {Cr-req} ,\quad \forall {UC} \epsilon {U-Cr}\mid \notag \\&\quad {Ub}[{8}]:={UC}[{3}] \wedge {Ub}[{7}]:={UC}[{2}] \notag \\&\quad \Rightarrow {U-Cr'}=U-Cr\cup \{{Ub}[{8}],{Ub}[{7}]\} \end{align}

After attaching handle the user is sent back to SHIRE of SP to show that the user is authenticated and is now eligible for further process. The aforesaid protocol flow is depicted in equation (15).

SECTION VII. Verification of Shibboleth Protocol

Demonstrating the correctness of a system is the process called as verification [49]. It is to verify the correctness of the system which is under contemplation. The system must be verified based on some specific parameters. Two of them are 1) The system’s properties 2) The system’s specifications. System’s properties are the axioms of the system. The system’s specifications actually define the system and its capability [50].

A. Shibboleth Model Verification Using Z3 Solver

Three basic steps have been followed for the verification of Shibboleth protocol which are: 1) Modeling of system, 2) Analysis of system, and 3) Verification of system [51]. In first step we have modeled the system using HLPN and the second step is done by describing the transitions and rules by using ${z}$ formal specification language. After this the rules are transformed using SMT-Lib. The Z3-Solver than verify the security properties of protocol and check them against the system’s specification. Z3 solver then after performing the computation gave out result either ‘sat’(satisfiable) or ‘unsat’(unsatisfiable). If ’sat’ then there is violation of the properties that have been asserted but if there is ‘unsat’ it means the properties hold and the system is proved correct.

Definition 2 (SMT Solver)[49]:

Given a theory ‘T’ and a quantifier formula ‘f’. We can say that the formula ‘f’ is T-satisfiable iff there exist a structure which satisfies both the formula ‘f’ and the theory ‘T’ [31].

For performing verification of a given model ‘M’ using Z3 solver we have to unfold the model ‘M’ which will provide $M_{k}$ and the formula ‘f’ that will provide $f_{k}$ . These parameters are then approved to be checked by Z3 solver. After performing the verification Z3 solver will give the results as satisfiable ‘sat’ or unsatisfiable ‘unsat’. In case of ‘sat’ the Z3 solver will also produce a counter example which is for the illustration of why the property or formula is violated. But if the answer is ‘unsat’ this means the formula or the property holds in the given model ${M}$ .

For proving the Shibboleth protocol the best fit for solving all the highlighted security challenges in FogIoT network, we have selected the three related properties which are also protocol specific. These properties will prove whether the Shibboleth deployment in FogIoT network will ensure required security or not. We will also evaluate the strength and weakness of proposed scenario after achieving the verification results.

Security Properties: We have selected following three properties which will prove or disprove the correctness of the Shibboleth.

Property 1:

In Shibboleth protocol SP, IdP and DS contain their own metadata file which contains information related to the attributes of aforesaid components. This metadata file is actually involved in the maintenance of trust between different domains. The information contained in the metadata file is used to identify the registered domains to avoid the involvement of fake domains. This property will hold if the metadata file of one component like SP’s metadata file contains information matching with the IdP and DS’s metadata information. This will ensure the system’s correctness regarding the security of metadata file. The code for this property is displayed below in Figure 15.

Property 2:

As authenticity is to check the source of information whether it’s authentic or not. The information sent by an authenticated user will be considered as authentic information. We have considered this as a property to check system’s correctness from authentication perspective. To check user’s authentication the attributes provided by user is matched with the attributes stored in its respective home domain to know that the user is an authenticated. The code for this property is displayed below in Figure 16.

Property 3:

Proxy is mean to hide your desired information. Like in Shibboleth protocol, the user doesn’t want to reveal his identity to the Service provider. When SP asks for user attributes from it’s home domain there must be a proxy which filters the attributes that have been allowed by the user for release. This proxy property will hold if the response given by attributes authority contain user’s proxy attribute instead of user’s ID which will reveal user’s identity. This property will also be used to prove the system’s correctness. The code for this property is displayed below in Figure 17.

SECTION VIII. Results

We have concluded two types of results, first one is based on the verification results and the second one is based on our literature review.

A. Verification Based Results

Our paper was aimed to propose a scenario for FogIoT network to access and outsource data securely. To prove the correctness of protocol’s security properties which we need to ensure the security in FogIoT network. The verification results show that all the selected security properties executed in finite time which means these properties truly exist in Shibboleth. Table 4 is demonstrating the execution time of Shibboleth protocol when it is verified on those security properties. Execution time taken by Z3 solver on each property has been plotted in Figure 4.

B. Literature Based Results

Based on our literature review the FogIoT network might come across some issues which need to be addressed in future. First of all, Shibboleth deployment in CloudIoT network will result in increased database size to be managed. Secondly, there is possibility of single point failure in FogIoT, as all the information and communication is carried out through the Shibboleth protocol. If Shibboleth gets down or compromised the whole network will be at risk. A backup server integrated with FogIoT which will store all the important backup data can also overcome this issue.

SECTION IX. Conclusion and Future Work

Our work was focused on deploying the Shibboleth protocol in a CloudIoT network for secure data access and outsourcing. As the Shibboleth protocol provides an architecture which manages both security and access. In this paper, we have critically analyzed the Shibboleth protocol which is a widely used security protocol. This critical study has made us to propose ‘Shibboleth based FogIoT network’ which includes Shibboleth for ensuring security between Fog Client and Fog Node. Then to prove its correctness of Shibboleth against selected security properties we have formally verified it using HLPN. The Z3 SMT solver was subsequently used for analyzing the rules of information flow, which proved the correctness of system against the three security properties. Achieved results have exposed the fact that the asserted security properties approved Shibboleth the best fit for ensuring strong security in FogIoT network. And these verification results conclude that the shibboleth deployment will also satisfy the security needs of the FogIoT network.

Future work will be based on the addressing the weaknesses found in our literature review. And also to check the FogIoT network with the latest version of Shibboleth.