Lightweight Failover Authentication Mechanism for IoT-Based Fog Computing Environment

Fog computing as an extension to the cloud computing infrastructure has been invaluable in enhancing the applicability of the Internet of Things (IoT) paradigm. IoT based Fog systems magnify the range and minimize the latency of IoT applications. However, as fog nodes are considered transient and they offer authenticated services, when an IoT end device loses connectivity with a fog node, it must authenticate freshly with a secondary fog node. In this work, we present a new security mechanism to leverage the initial authentication to perform fast lightweight secondary authentication to ensure smooth failover among fog nodes. The proposed scheme is secure in the presence of a current de-facto Canetti and Krawczyk (CK)-adversary. We demonstrate the security of the proposed scheme with a detailed security analysis using formal security under the broadly recognized Real-Or-Random (ROR) model, informal security analysis as well as through formal security verification using the broadly-used Automated Validation of Internet Security Protocols and Applications (AVISPA) software tool. A testbed experiment for measuring computational time for different cryptographic primitives using the Multiprecision Integer and Rational Arithmetic Cryptographic Library (MIRACL) has been done. Finally, through comparative analysis with other related schemes, we show how the presented approach is uniquely advantageous over other schemes.

Hierarchic Superposition Revisited

In 1994,Bachmair, Ganzinger, and Waldmann introduced the hierarchicalsuperposition calculus as a generalization of the superpositioncalculus for black-box style theory reasoning.Their calculus works in a framework of hierarchic specifications.It tries to prove theunsatisfiability of a set of clauses with respect to interpretationsthat extend a background model such as the integers with linear arithmeticconservatively, that is, withoutidentifying distinct elements of old sorts ("confusion") and withoutadding new elements to old sorts ("junk").We show how the calculus can be improved,report on practical experiments,and present a new completeness result fornon-compact classes of background models(i.e., linear integer or rational arithmetic restricted tostandard models).

PEBBLE GAMES AND LINEAR EQUATIONS

We give a new, simplified and detailed account of the correspondence between levels of the Sherali–Adams relaxation of graph isomorphism and levels of pebble-game equivalence with counting (higher-dimensional Weisfeiler–Lehman colour refinement). The correspondence between basic colour refinement and fractional isomorphism, due to Tinhofer [22; 23] and Ramana, Scheinerman and Ullman [17], is re-interpreted as the base level of Sherali–Adams and generalised to higher levels in this sense by Atserias and Maneva [1] and Malkin [14], who prove that the two resulting hierarchies interleave. In carrying this analysis further, we here give (a) a precise characterisation of the level k Sherali–Adams relaxation in terms of a modified counting pebble game; (b) a variant of the Sherali–Adams levels that precisely match the k-pebble counting game; (c) a proof that the interleaving between these two hierarchies is strict. We also investigate the variation based on boolean arithmetic instead of real/rational arithmetic and obtain analogous correspondences and separations for plain k-pebble equivalence (without counting). Our results are driven by considerably simplified accounts of the underlying combinatorics and linear algebra.