Publications

Given how common IoT devices that use constrained resources are becoming today, the need of the hour is communication protocols which can operate securely under such limitations. For a few years, the Internet Engineering Task Force (IETF) has been working to standardize EDHOC, an authenticated key establishment protocol for such constrained IoT devices. The first version of EDHOC was proposed in 2016. In 2018, Bruni et al. [3] used the ProVerif tool [2] to formally analyze an early version of EDHOC, which had only two key establishment methods. By 2021, the protocol had been fleshed out much more, with multiple new key establishment methods, and this version was formally analyzed using the Tamarin prover [15] in [17]. In this paper, we build on that work, by modifying the model, analyzing some new properties, and discussing some aspects of the latest EDHOC specification. In particular, we extend the modeling in [17] with trusted execution environments (TEEs), modify the way we model XOR encryption, and in addition to the properties verified in [17], we verify weak post-compromise security (PCS) as well as the secrecy and integrity of some additional data used as part of the protocol.

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.

In the Russian cards problem, a group of communicating agents and an eavesdropper, Eve, draw cards from a deck. The agents then wish to inform each other about their hand without Eve learning any ‘protected’ information, typically in the sense of weak possibilistic security. We consider a weakening of this original problem, whereby the cards are linearly ordered by value. The agents wish to know the value of the best card held between them, without Eve knowing who holds said card. We consider standard solutions to the problem based on combinatorial designs, as well as novel solutions based on secret-bit-exchange protocols. Our results show that this version of the problem can be solved in many instances where the size of each agent’s hand is linear on that of the eavesdropper’s.

We identify a new decidable class of security protocols, both for reachability and equivalence properties. Our result holds for an unbounded number of sessions and for protocols with nonces. It covers all standard cryptographic primitives. Our class sets up three main assumptions. (i) Protocols need to be “simple”, meaning that an attacker can precisely identify from which participant and which session a message originates from. We also consider protocols with no else branches (only positive test). (ii) Protocols should be type-compliant, which is intuitively guaranteed as soon as two encrypted messages of the protocol cannot be confused. (iii) Finally, we define the notion of a dependency graph, which, given a protocol, characterises how actions depend on the other ones (both sequential dependencies and data dependencies are taken into account). Whenever the graph is acyclic, then the protocol falls into our class. We show that many protocols of the literature belong to our decidable class, including for example some of the protocols embedded in the biometric passport.

We study procedures for the derivability problem of fragments of intuitionistic logic. Intuitionistic logic is known to be PSPACE-complete, with implication being one of the main contributors to this complexity. In fact, with just implication alone, we still have a PSPACE-complete logic. We study fragments of intuitionistic logic with restricted implication and develop algorithms for these fragments which are based on the proof rules. We identify a core fragment whose derivability is solvable in linear time. Adding disjunction elimination to this core gives a logic which is solvable in co-NP. These sub-procedures are applicable to a wide variety of logics with rules of a similar flavour. We also show that we cannot do better than co-NP whenever disjunction elimination interacts with other rules.

In (Ramanujam, Sundararajan, and Suresh [2014]), we extended 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 protocol.

In the formal study of security protocols and access control systems, fragments of intuitionistic logic play a vital role. These are required to be efficient, and are typically disjunction-free. In this paper, we study the complexity of adding disjunction to these subsystems. Our lower bound results show that very little needs to be added to disjunction to get co-NP-hardness, while our upper bound results show that even a system with conjunction, disjunction, and restricted forms of negation and implication is in co-NP. Our upper bound proofs also suggest parameters which we can bound to obtain PTIME algorithms.

Cryptographic protocols often require principals to send certifications asserting partial knowledge of terms (for instance, that an encrypted secret is 0 or 1). Such certificates are themselves modelled by cryptographic primitives or sequences of communications. For logical analysis of such protocols based on the Dolev-Yao model [1983], we suggest that it is useful to separate terms and assertions about them in communications. We propose a perfect assertion assumption by which the underlying model ensures the correctness of the assertion when it is generated. The recipient may then rely on the certificate but may only forward it as second-hand information. We use a simple propositional modal assertion language involving disjunction (for partial knowledge) and formulas of the form A says α  (for delegation). We study the complexity of the term derivability problem and safety checking in the presence of an active intruder (for bounded protocols). We show that assertions add complexity to verification, but when they involve only boundedly many disjunctions, the complexity is the same as that of the standard Dolev-Yao model.

This paper introduces a novel method for the prediction of chaotic time series using a combination of Hidden Markov Model (HMM) and Neural Network (NN). In this paper, an algorithm is proposed wherein an HMM, which is a doubly embedded stochastic process, is used for the shape based clustering of data. These data clusters are trained individually with Neural Network. The novel prediction approach used here exploits the Pattern Identification prowess of the HMM for cluster selection and uses the NN associated with each cluster to predict the output of the system. The effectiveness of the method is evaluated by using the benchmark chaotic time series: Mackey Glass Time Series (MGTS). Simulation results show that the given method provides a better prediction performance in comparison to previous methods.

In this paper, we present a method of management of a dynamic scene using octrees. The use of octrees in image rendering in 3D space is suitable as the octree is essentially a tree data structure in three dimensions. Most such methods resort to modification - namely, resizing and rebuilding - of the nodes of the tree used in order to accomplish the desired results. The main concern in such an approach is to minimize, or preferably, avoid resizing of nodes during runtime, as it takes a great toll on system resources. Here we present an algorithm that completely avoids resizing of nodes, hence achieving greater efficiency. This aspect of the algorithm is also borne out by the experimental conclusions we have obtained.

Given how common IoT devices that use constrained resources are becoming today, the need of the hour is communication protocols which can operate securely under such limitations. For a few years, the Internet Engineering Task Force (IETF) has been working to standardize EDHOC, an authenticated key establishment protocol for such constrained IoT devices. The first version of EDHOC was proposed in 2016. In 2018, Bruni et al. [3] used the ProVerif tool [2] to formally analyze an early version of EDHOC, which had only two key establishment methods. By 2021, the protocol had been fleshed out much more, with multiple new key establishment methods, and this version was formally analyzed using the Tamarin prover [15] in [17]. In this paper, we build on that work, by modifying the model, analyzing some new properties, and discussing some aspects of the latest EDHOC specification. In particular, we extend the modeling in [17] with trusted execution environments (TEEs), modify the way we model XOR encryption, and in addition to the properties verified in [17], we verify weak post-compromise security (PCS) as well as the secrecy and integrity of some additional data used as part of the protocol.

In the Russian cards problem, a group of communicating agents and an eavesdropper, Eve, draw cards from a deck. The agents then wish to inform each other about their hand without Eve learning any ‘protected’ information, typically in the sense of weak possibilistic security. We consider a weakening of this original problem, whereby the cards are linearly ordered by value. The agents wish to know the value of the best card held between them, without Eve knowing who holds said card. We consider standard solutions to the problem based on combinatorial designs, as well as novel solutions based on secret-bit-exchange protocols. Our results show that this version of the problem can be solved in many instances where the size of each agent’s hand is linear on that of the eavesdropper’s.

We identify a new decidable class of security protocols, both for reachability and equivalence properties. Our result holds for an unbounded number of sessions and for protocols with nonces. It covers all standard cryptographic primitives. Our class sets up three main assumptions. (i) Protocols need to be “simple”, meaning that an attacker can precisely identify from which participant and which session a message originates from. We also consider protocols with no else branches (only positive test). (ii) Protocols should be type-compliant, which is intuitively guaranteed as soon as two encrypted messages of the protocol cannot be confused. (iii) Finally, we define the notion of a dependency graph, which, given a protocol, characterises how actions depend on the other ones (both sequential dependencies and data dependencies are taken into account). Whenever the graph is acyclic, then the protocol falls into our class. We show that many protocols of the literature belong to our decidable class, including for example some of the protocols embedded in the biometric passport.

We study procedures for the derivability problem of fragments of intuitionistic logic. Intuitionistic logic is known to be PSPACE-complete, with implication being one of the main contributors to this complexity. In fact, with just implication alone, we still have a PSPACE-complete logic. We study fragments of intuitionistic logic with restricted implication and develop algorithms for these fragments which are based on the proof rules. We identify a core fragment whose derivability is solvable in linear time. Adding disjunction elimination to this core gives a logic which is solvable in co-NP. These sub-procedures are applicable to a wide variety of logics with rules of a similar flavour. We also show that we cannot do better than co-NP whenever disjunction elimination interacts with other rules.

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.

In (Ramanujam, Sundararajan, and Suresh [2014]), we extended 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 protocol.

In the formal study of security protocols and access control systems, fragments of intuitionistic logic play a vital role. These are required to be efficient, and are typically disjunction-free. In this paper, we study the complexity of adding disjunction to these subsystems. Our lower bound results show that very little needs to be added to disjunction to get co-NP-hardness, while our upper bound results show that even a system with conjunction, disjunction, and restricted forms of negation and implication is in co-NP. Our upper bound proofs also suggest parameters which we can bound to obtain PTIME algorithms.

Cryptographic protocols often require principals to send certifications asserting partial knowledge of terms (for instance, that an encrypted secret is 0 or 1). Such certificates are themselves modelled by cryptographic primitives or sequences of communications. For logical analysis of such protocols based on the Dolev-Yao model [1983], we suggest that it is useful to separate terms and assertions about them in communications. We propose a perfect assertion assumption by which the underlying model ensures the correctness of the assertion when it is generated. The recipient may then rely on the certificate but may only forward it as second-hand information. We use a simple propositional modal assertion language involving disjunction (for partial knowledge) and formulas of the form A says α  (for delegation). We study the complexity of the term derivability problem and safety checking in the presence of an active intruder (for bounded protocols). We show that assertions add complexity to verification, but when they involve only boundedly many disjunctions, the complexity is the same as that of the standard Dolev-Yao model.

This paper introduces a novel method for the prediction of chaotic time series using a combination of Hidden Markov Model (HMM) and Neural Network (NN). In this paper, an algorithm is proposed wherein an HMM, which is a doubly embedded stochastic process, is used for the shape based clustering of data. These data clusters are trained individually with Neural Network. The novel prediction approach used here exploits the Pattern Identification prowess of the HMM for cluster selection and uses the NN associated with each cluster to predict the output of the system. The effectiveness of the method is evaluated by using the benchmark chaotic time series: Mackey Glass Time Series (MGTS). Simulation results show that the given method provides a better prediction performance in comparison to previous methods.

In this paper, we present a method of management of a dynamic scene using octrees. The use of octrees in image rendering in 3D space is suitable as the octree is essentially a tree data structure in three dimensions. Most such methods resort to modification - namely, resizing and rebuilding - of the nodes of the tree used in order to accomplish the desired results. The main concern in such an approach is to minimize, or preferably, avoid resizing of nodes during runtime, as it takes a great toll on system resources. Here we present an algorithm that completely avoids resizing of nodes, hence achieving greater efficiency. This aspect of the algorithm is also borne out by the experimental conclusions we have obtained.