Modular coinduction up-to for higher-order languages via first-order transition systems

The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible functions. We transport this theory onto languages whose bisimilarity and LTS go beyond those of first-order models. The approach consists in exhibiting fully abstract translations of the more sophisticated LTSs and bisimilarities onto the first-order ones. This allows us to reuse directly the large corpus of up-to techniques that are available on first-order LTSs. The only ingredient that has to be manually supplied is the compatibility of basic up-to techniques that are specific to the new languages. We investigate the method on the pi-calculus, the lambda-calculus, and a (call-by-value) lambda-calculus with references.

DCSS Protocol for Data Caching and Sharing Security in a 5G Network

Fifth Generation mobile networks (5G) promise to make network services provided by various Service Providers (SP) such as Mobile Network Operators (MNOs) and third-party SPs accessible from anywhere by the end-users through their User Equipment (UE). These services will be pushed closer to the edge for quick, seamless, and secure access. After being granted access to a service, the end-user will be able to cache and share data with other users. However, security measures should be in place for SP not only to secure the provisioning and access of those services but also, should be able to restrict what the end-users can do with the accessed data in or out of coverage. This can be facilitated by federated service authorization and access control mechanisms that restrict the caching and sharing of data accessed by the UE in different security domains. In this paper, we propose a Data Caching and Sharing Security (DCSS) protocol that leverages federated authorization to provide secure caching and sharing of data from multiple SPs in multiple security domains. We formally verify the proposed DCSS protocol using ProVerif and applied pi-calculus. Furthermore, a comprehensive security analysis of the security properties of the proposed DCSS protocol is conducted.

Formal Verification of Authentication and Service Authorization Protocols in 5G-Enabled Device-to-Device Communications Using ProVerif

Device-to-Device (D2D) communications will be used as an underlay technology in the Fifth Generation mobile network (5G), which will make network services of multiple Service Providers (SP) available anywhere. The end users will be allowed to access and share services using their User Equipments (UEs), and thus they will require seamless and secured connectivity. At the same time, Mobile Network Operators (MNOs) will use the UE to offload traffic and push contents closer to users relying on D2D communications network. This raises security concerns at different levels of the system architecture and highlights the need for robust authentication and authorization mechanisms to provide secure services access and sharing between D2D users. Therefore, this paper proposes a D2D level security solution that comprises two security protocols, namely, the D2D Service security (DDSec) and the D2D Attributes and Capability security (DDACap) protocols, to provide security for access, caching and sharing data in network-assisted and non-network-assisted D2D communications scenarios. The proposed solution applies Identity-based Encryption (IBE), Elliptic Curve Integrated Encryption Scheme (ECIES) and access control mechanisms for authentication and authorization procedures. We formally verified the proposed protocols using ProVerif and applied pi calculus. We also conducted a security analysis of the proposed protocols.

An Extensive Formal Analysis of Multi-factor Authentication Protocols

Passwords are still the most widespread means for authenticating users, even though they have been shown to create huge security problems. This motivated the use of additional authentication mechanisms in so-called multi-factor authentication protocols. In this article, we define a detailed threat model for this kind of protocol: While in classical protocol analysis attackers control the communication network, we take into account that many communications are performed over TLS channels, that computers may be infected by different kinds of malware, that attackers could perform phishing, and that humans may omit some actions. We formalize this model in the applied pi calculus and perform an extensive analysis and comparison of several widely used protocols—variants of Google 2-step and FIDO’s U2F (Yubico’s Security Key token). The analysis is completely automated, generating systematically all combinations of threat scenarios for each of the protocols and using the P ROVERIF tool for automated protocol analysis. To validate our model and attacks, we demonstrate their feasibility in practice, even though our experiments are run in a laboratory environment. Our analysis highlights weaknesses and strengths of the different protocols. It allows us to suggest several small modifications of the existing protocols that are easy to implement, as well as an extension of Google 2-step that improves security in several threat scenarios.

Types for Complexity of Parallel Computation in Pi-Calculus

Type systems as a technique to analyse or control programs have been extensively studied for functional programming languages. In particular some systems allow to extract from a typing derivation a complexity bound on the program. We explore how to extend such results to parallel complexity in the setting of the pi-calculus, considered as a communication-based model for parallel computation. Two notions of time complexity are given: the total computation time without parallelism (the work) and the computation time under maximal parallelism (the span). We define operational semantics to capture those two notions, and present two type systems from which one can extract a complexity bound on a process. The type systems are inspired both by size types and by input/output types, with additional temporal information about communications.

Compositional Analysis of Protocol Equivalence in the Applied $$\pi $$-Calculus Using Quasi-open Bisimilarity

This paper shows that quasi-open bisimilarity is the coarsest bisimilarity congruence for the applied $$\pi $$ π -calculus. Furthermore, we show that this equivalence is suited to security and privacy problems expressed as an equivalence problem in the following senses: (1) being a bisimilarity is a safe choice since it does not miss attacks based on rich strategies; (2) being a congruence it enables a compositional approach to proving certain equivalence problems such as unlinkability; and (3) being the coarsest such bisimilarity congruence it can establish proofs of some privacy properties where finer equivalences fail to do so.

Explainable AI for Workflow Verification in VIPLE

Teaching students the concepts behind computational thinking is a difficult task, often gated by the inherent difficulty of programming languages. In the classroom, teaching assistants may be required to interact with students to help them learn the material. Time spent in grading and offering feedback on assignments removes from this time to help students directly. As such, we offer a framework for developing an explainable Artificial Intelligence that performs automated analysis of student code while offering feedback and partial credit. The creation of this system is dependent on three core components. Those components are a knowledge base, a set of conditions to be analyzed, and a formal set of inference rules. In this paper, we develop such a system for our own language by employing Pi-Calculus and Hoare Logic. Our detailed system can also perform self-learning of rules. Given solution files, the system is able to extract the important aspects of the program and develop feedback that explicitly details the errors students make when they veer away from these aspects. The level of detail and expected precision can be easily modified through parameter tuning and variety in sample solutions.

COMPARATIVE ANALYSIS BETWEEN ULTRASONIC TIPS AND HAND INSTRUMENTS ON THE CLINICAL PARAMETERS OF PERIODONTAL DISEASE.

Aims To compare hand versus ultrasonic scaling and root planning (SRP) on the clinical parameters of periodontal disease and to assess left over calculus by open flap approach. Methods and Material The study sample consisted of random selection of 30 patients with the evidence of chronic inflammatory periodontal disease. Two groups were made in each patient by split mouth design. Pre treatment measurements recorded were plaque index (PI) , calculus index(CI) and probing pocket depth(PPD). Post treatment measurements recorded were PI , PPD and left over calculus after flap elevation Results In hand instrumentation group (HIG),, mean percentage of plaque score was slightly lesser as compared to ultrasonic but not significant.. Overall mean reduction in PPD after instrumentation in HIG was greater as compared to ultrasonic, but it was not statistically significant (p>0.05). The percentage efficiency in removal of calculus of HIG was greater compared to ultrasonic but it was also not statistically significant (p>0.05). There was no significant difference between HIG and ultrasonic for number of sites with residual calculus and moreover no. of sites increased apically. Conclusions There was significant post-treatment change in the clinical parameters taken in the present clinical study in both HIG & UIG and also slightly more favourable with HIG but not statistically significant.