A Formal Framework for Secure Fog Architectures

2021 ◽  
Vol 11 (2) ◽  
pp. 51-74
Author(s):  
Zakaria Benzadri ◽  
Ayoub Bouheroum ◽  
Faiza Belala
Keyword(s):  
Identity Management ◽  
Formal Model ◽  
Formal Analysis ◽  
Fog Computing ◽  
Security Requirements ◽  
Access Management ◽  
Formal Framework ◽  
Supporting Tool ◽  
Refinery Plant ◽  
Oil Gas

Despite the importance of fog computing, few works using formal techniques have been interested in the modelling and verification of fog architectures to ensure their security. The present work fits into this context and proposes a generic formal model (CA-BRS), extending the BRS with control agents. This offers the possibility to specify a fog architecture consisting of a set of secure fog nodes that act both as filters to reduce the amount of data sent to the cloud and as processing units close to the data collected. This formal setting makes possible the description of the multi-layers' collaboration requirements (IoT, fog, and cloud) and the analysis of certain security requirements with regard to identity management and resource access management. The execution of CA-BRS model through the framework supporting tool: “Maude-based Tool for CA-BRS” allows the formal analysis of the reliability and availability properties of an illustrative fog system example which is an oil/gas refinery plant.

scholarly journals Identity and Access Management Resilience against Intentional Risk for Blockchain-Based IOT Platforms

Electronics ◽  
2021 ◽  
Vol 10 (4) ◽  
pp. 378
Author(s):  
Alberto Partida ◽  
Regino Criado ◽  
Miguel Romance
Keyword(s):  
Security Requirements ◽  
Access Management ◽  
Iot Security ◽  
Complex Network Theory ◽  
Scale Free ◽  
Blockchain Technology ◽  
Technology Transfers ◽  
Iot Platforms ◽  
Market Capitalisation ◽  
Security Incidents

Some Internet of Things (IoT) platforms use blockchain to transport data. The value proposition of IoT is the connection to the Internet of a myriad of devices that provide and exchange data to improve people’s lives and add value to industries. The blockchain technology transfers data and value in an immutable and decentralised fashion. Security, composed of both non-intentional and intentional risk management, is a fundamental design requirement for both IoT and blockchain. We study how blockchain answers some of the IoT security requirements with a focus on intentional risk. The review of a sample of security incidents impacting public blockchains confirm that identity and access management (IAM) is a key security requirement to build resilience against intentional risk. This fact is also applicable to IoT solutions built on a blockchain. We compare the two IoT platforms based on public permissionless distributed ledgers with the highest market capitalisation: IOTA, run on an alternative to a blockchain, which is a directed acyclic graph (DAG); and IoTeX, its contender, built on a blockchain. Our objective is to discover how we can create IAM resilience against intentional risk in these IoT platforms. For that, we turn to complex network theory: a tool to describe and compare systems with many participants. We conclude that IoTeX and possibly IOTA transaction networks are scale-free. As both platforms are vulnerable to attacks, they require resilience against intentional risk. In the case of IoTeX, DIoTA provides a resilient IAM solution. Furthermore, we suggest that resilience against intentional risk requires an IAM concept that transcends a single blockchain. Only with the interplay of edge and global ledgers can we obtain data integrity in a multi-vendor and multi-purpose IoT network.

Formal Specification of Information Transmission Architecture Based on Automatic Generation of Primitives in Digital Campus

2013 ◽  
Vol 846-847 ◽  
pp. 1644-1647
Author(s):  
Xiao Le Li ◽  
Ying Wen ◽  
Ming Weng
Keyword(s):  
Information Transmission ◽  
Formal Analysis ◽  
Automatic Generation ◽  
Comprehensive Analysis ◽  
Security Requirements ◽  
Digital Campus ◽  
Application Systems ◽  
Secure Information ◽  
Common Framework ◽  
Automatic Tool

Based on comprehensive analysis on security requirements of information transmission, security primitive is generated by automatic tool in asymmetric key cryptosystem, and improved with addition of compositional factors. And then, formal processes of secure information transmission are constructed with composition method. Formal analysis shows that, secrecy, integrity, availability, controllability, non-repudiation and identifiability during information transmission can be insured by this architecture, as a common framework for development of various application systems in digital campus from the viewpoint of information security.

scholarly journals Fog-Driven Secure Authentication and Key Exchange Scheme for Wearable Health Monitoring System

2021 ◽  
Vol 2021 ◽  
pp. 1-14 ◽  
Author(s):  
Tsu-Yang Wu ◽  
Lei Yang ◽  
Qian Meng ◽  
Xinglan Guo ◽  
Chien-Ming Chen
Keyword(s):  
Health Monitoring ◽  
Formal Analysis ◽  
Fog Computing ◽  
Key Exchange ◽  
Monitoring Systems ◽  
Health Monitoring Systems ◽  
Wearable Health Monitoring Systems ◽  
Secure Authentication ◽  
Internet Of Things Technology ◽  
Smart Wearable

Smart wearable devices, as a popular mobile device, have a broad market. Smart wearable medical devices implemented in wearable health monitoring systems can monitor the data pertaining to a patient’s body and let the patient know their own physical condition. In addition, these data can be stored, analyzed, and processed in the cloud to effectively prevent diseases. As an Internet-of-things technology, fog computing can process, store, and control data around devices in real time. However, the distributed attributes of fog nodes make the monitored body data and medical reports at risk of privacy disclosure. In this paper, we propose a fog-driven secure authentication and key exchange scheme for wearable health monitoring systems. Furthermore, we conduct a formal analysis using the Real-Oracle-Random model, Burrows–Abadi–Needham logic, and ProVerif tools and an informal analysis to perform security verification. Finally, a performance comparison with other related schemes shows that the proposed scheme has the best advantages in terms of security, computing overhead, and communication cost.

scholarly journals Multilayer networks as embodied consciousness interactions. A formal model approach.

2021 ◽  
Author(s):  
Camilo Miguel Signorelli ◽  
joaquin diaz boils
Keyword(s):  
Formal Model ◽  
Conscious Experience ◽  
Formal Analysis ◽  
Mathematical Formulation ◽  
Multilayer Networks ◽  
Topological Network ◽  
Binary Operator ◽  
Algebraic Interpretation ◽  
Embodied Consciousness ◽  
Model Approach

An algebraic interpretation of multilayer networks is introduced in relation to conscious experience, brain and body. The discussion is based on a network model for undirected multigraphs with coloured edges whose elements are time-evolving multilayers, representing complex experiential brain-body networks. These layers have the ability to merge by an associative binary operator, accounting for biological composition. As an extension, they can rotate in a formal analogy to how the activity inside layers would dynamically evolve. Under consciousness interpretation, we also studied a mathematical formulation of splitting layers, resulting in a formal analysis for the transition from conscious to non-conscious activity. From this construction, we recover core structures for conscious experience, dynamical content and causal efficacy of conscious interactions, predicting topological network changes after conscious layer interactions. Our approach provides a mathematical account of coupling and splitting layers co-arising with more complex experiences. These concrete results may inspire the use of formal studies of conscious experience not only to describe it, but also to obtain new predictions and future applications of formal mathematical tools.

Identity and Access Management in the Internet Age

2018 ◽  
pp. 1-13
Keyword(s):  
Social Identity ◽  
Identity Management ◽  
Daily Activities ◽  
The Internet ◽  
Access Management ◽  
Internet Age ◽  
History Of ◽  
Identity Problems

This chapter presents a few scenarios to demonstrate the fact that identity management is employed in many aspects of our daily activities and gives a brief history of Identity and Access Management, showing our readers how the Internet has prompted identity problems. The author will discuss some of the challenges exemplified by some scenarios such as passwords, biometrics, social identity, and identity mobility.

An Extensible Identity Management Framework for Cloud-Based E-Government Systems

2016 ◽  
pp. 399-422
Author(s):  
Hirra Anwar ◽  
Muhammad Awais Shibli ◽  
Umme Habiba
Keyword(s):  
Cloud Computing ◽  
Identity Management ◽  
Security Requirements ◽  
Computing Technology ◽  
Management Framework ◽  
Government Organizations ◽  
Domain Specific ◽  
Government Institutions ◽  
Design And Implementation

Numerous Cloud Identity Management (IdM) systems have been designed and implemented to meet the diverse functional and security requirements of various organizations. These requirements are subjective in nature; for instance, some government organizations require security more than efficiency while others prioritize performance and immediate response over security. However, most of the existing IdM systems are incapable of handling the user-centricity, security & technology requirements and are also domain specific. In this regard, this chapter elaborates the need to use Cloud Computing technology for enhancing the effectiveness and transparency of IdM functions and presents a comprehensive and well-structured Extensible IdM Framework for Cloud based e-government institutions. We present the design and implementation details of the proposed framework, followed by a case study which shows how government organizations of Pakistan would use the proposed framework to improve their IdM processes and achieve diverse IdM services.

scholarly journals A High-Level Petri Net Framework for Genetic Regulatory Networks

2007 ◽  
Vol 4 (3) ◽  
pp. 1-14 ◽  
Author(s):  
Richard Banks ◽  
L. Jason Steggles
Keyword(s):  
Regulatory Networks ◽  
Formal Analysis ◽  
Boolean Model ◽  
Genetic Regulatory Networks ◽  
Cellular Systems ◽  
Logic Minimization ◽  
Formal Framework ◽  
The Individual ◽  
High Level ◽  
Compare And Contrast

Summary To understand the function of genetic regulatory networks in the development of cellular systems, we must not only realise the individual network entities, but also the manner by which they interact. Multi-valued networks are a promising qualitative approach for modelling such genetic regulatory networks, however, at present they have limited formal analysis techniques and tools. We present a flexible formal framework for modelling and analysing multi-valued genetic regulatory networks using high-level Petri nets and logic minimization techniques. We demonstrate our approach with a detailed case study in which part of the genetic regulatory network responsible for the carbon starvation stress response in Escherichia coli is modelled and analysed. We then compare and contrast this multivalued model to a corresponding Boolean model and consider their formal relationship.

Taking Sides in Wars of Attrition

2017 ◽  
Vol 111 (2) ◽  
pp. 219-236 ◽  
Author(s):  
ROBERT POWELL
Keyword(s):  
Asymmetric Information ◽  
Continuous Time ◽  
Formal Analysis ◽  
Third Parties ◽  
The Other ◽  
Third Party ◽  
War Of Attrition ◽  
The Third ◽  
Boomerang Effect ◽  
Formal Framework

Third parties often have a stake in the outcome of a conflict and can affect that outcome by taking sides. This article studies the factors that affect a third party's decision to take sides in a civil or interstate war by adding a third actor to a standard continuous-time war of attrition with two-sided asymmetric information. The third actor has preferences over which of the other two actors wins and for being on the winning side conditional on having taken sides. The third party also gets a flow payoff during the fighting which can be positive when fighting is profitable or negative when fighting is costly. The article makes four main contributions: First, it provides a formal framework for analyzing the effects of endogenous intervention on the duration and outcome of the conflict. Second, it identifies a “boomerang” effect that tends to make alignment decisions unpredictable and coalitions dynamically unstable. Third, it yields several clear comparative-static results. Finally, the formal analysis has implications for empirical efforts to estimate the effects of intervention, showing that there may be significant selection and identification issues.

scholarly journals Formal analysis of security protocols for wireless sensor networks

2010 ◽  
Vol 47 (1) ◽  
pp. 81-97 ◽  
Author(s):  
Marián Novotný
Keyword(s):  
Sensor Networks ◽  
Formal Model ◽  
Formal Analysis ◽  
Security Protocols ◽  
Data Integrity ◽  
Wireless Sensor ◽  
Semantic Model ◽  
Communication Graph ◽  
Pi Calculus ◽  
Security Properties

Abstract Design of security protocols is notoriously error-prone. For this reason, it is required to use formal methods to analyze their security properties. In the paper we present a formal analysis of the Canvas protocol. The Canvas protocol was developed by Harald Vogt and should provide data integrity inWireless Sensor Networks. However, Dieter Gollmann published an attack on the protocol. We consider the fallacy of the Canvas scheme in different models of the attacker and present a solution for correcting the scheme.We propose a formal model of the fixed Canvas protocol in the applied pi-calculus. This model includes a model of the network topology, communication channels, captured nodes, and capabilities of the attacker. Moreover, we formulate and analyze the data integrity property of the scheme in the semantic model of the applied pi-calculus. We prove that the fixed Canvas scheme, in the presence of an active adversary, provides data integrity of messages assuming that captured nodes are not direct neighbors in the communication graph of a sensor network. Finally, we discuss the applicability of the proposed formal model for analysis of other WSN security protocols.

Sign in / Sign up

Export Citation Format

Share Document