Vaishnavi Sundararajan

Giorgio Cignarale, Hans van Ditmarsch, Stephan Felber et al.

We investigate self-correcting gossip protocols with errors. In distributed computing, protocols with errors have been widely investigated in temporal epistemic logics. Instead, we propose a dynamic epistemic logic. We show how to correct transmission errors due to faulty messages without a central authority coordinating protocol execution, how this affects optimality, and how this compares to bounded memory and full information protocols.

R. Ramanujam, Vaishnavi Sundararajan, S. P. Suresh

In the symbolic verification of cryptographic protocols, a central problem is deciding whether a protocol admits an execution which leaks a designated secret to the malicious intruder. Rusinowitch and Turuani (2003) show that, when considering finitely many sessions and a protocol model where only terms are communicated, this ``insecurity problem'' is NP-complete. Central to their proof strategy is the observation that any execution of a protocol can be simulated by one where the intruder only communicates terms of bounded size. However, when we consider models where, in addition to terms, one can also communicate logical formulas, the analysis of the insecurity problem becomes tricky. In this paper we consider the insecurity problem for protocols with logical statements that include equality on terms and existential quantification. Witnesses for existential quantifiers may be of unbounded size, and obtaining small witnesses while maintaining equality proofs complicates the analysis. We use a notion of "typed" equality proofs, and extend techniques from [RT03] to show that this problem is also in NP. We also show that these techniques can be used to analyze the insecurity problem for systems such as the one proposed in Ramanujam, Sundararajan and Suresh (2017).

Alexandros Nikou, Anusha Mujumdar, Vaishnavi Sundararajan et al.

In this paper, we present a Symbolic Reinforcement Learning (SRL) based architecture for safety control of Radio Access Network (RAN) applications. In particular, we provide a purely automated procedure in which a user can specify high-level logical safety specifications for a given cellular network topology in order for the latter to execute optimal safe performance which is measured through certain Key Performance Indicators (KPIs). The network consists of a set of fixed Base Stations (BS) which are equipped with antennas, which one can control by adjusting their vertical tilt angle. The aforementioned process is called Remote Electrical Tilt (RET) optimization. Recent research has focused on performing this RET optimization by employing Reinforcement Learning (RL) strategies due to the fact that they have self-learning capabilities to adapt in uncertain environments. The term safety refers to particular constraints bounds of the network KPIs in order to guarantee that when the algorithms are deployed in a live network, the performance is maintained. In our proposed architecture the safety is ensured through model-checking techniques over combined discrete system models (automata) that are abstracted through the learning process. We introduce a user interface (UI) developed to help a user set intent specifications to the system, and inspect the difference in agent proposed actions, and those that are allowed and blocked according to the safety specification.

Kristijonas Cyras, Ramamurthy Badrinath, Swarup Kumar Mohalik et al.

As a field of AI, Machine Reasoning (MR) uses largely symbolic means to formalize and emulate abstract reasoning. Studies in early MR have notably started inquiries into Explainable AI (XAI) -- arguably one of the biggest concerns today for the AI community. Work on explainable MR as well as on MR approaches to explainability in other areas of AI has continued ever since. It is especially potent in modern MR branches, such as argumentation, constraint and logic programming, planning. We hereby aim to provide a selective overview of MR explainability techniques and studies in hopes that insights from this long track of research will complement well the current XAI landscape. This document reports our work in-progress on MR explainability.

Karl Norrman, Vaishnavi Sundararajan, Alessandro Bruni

Constrained IoT devices are becoming ubiquitous in society and there is a need for secure communication protocols that respect the constraints under which these devices operate. EDHOC is an authenticated key establishment protocol for constrained IoT devices, currently being standardized by the Internet Engineering Task Force (IETF). A rudimentary version of EDHOC with only two key establishment methods was formally analyzed in 2018. Since then, the protocol has evolved significantly and several new key establishment methods have been added. In this paper, we present a formal analysis of all EDHOC methods in an enhanced symbolic Dolev-Yao model using the Tamarin tool. We show that not all methods satisfy the authentication notion injective of agreement, but that they all do satisfy a notion of implicit authentication, as well as Perfect Forward Secrecy (PFS) of the session key material. We identify other weaknesses to which we propose improvements. For example, a party may intend to establish a session key with a certain peer, but end up establishing it with another, trusted but compromised, peer. We communicated our findings and proposals to the IETF, which has incorporated some of these in newer versions of the standard.

R. Ramanujam, Vaishnavi Sundararajan, S. P. Suresh

In earlier work, we extend the Dolev-Yao model with assertions. We build on that work and add existential abstraction to the language, which allows us to translate common constructs used in voting protocols into proof properties. We also give an equivalence-based definition of anonymity in this model, and prove anonymity for the FOO voting protocol.