Web traffic analysis and classification has been extensively studied, both with classical and deep learning techniques. Many of these systems analyse the entire packet to perform the classification task. Due to the increase of encrypted traffic in …
MTProto 2.0 is a suite of cryptographic protocols for instant messaging at the core of the popular Telegram messenger application. In this paper we analyse MTProto 2.0 using the symbolic verifier ProVerif. We provide fully automated proofs of the …
(Pre)closure spaces are a generalization of topological spaces covering also the notion of neighbourhood in discrete structures, widely used to model and reason about spatial aspects of distributed systems. In this paper we present an abstract …
We introduce partial sessions and partial (multiparty) session types, in order to deal with open systems, i.e., systems with missing components. Partial sessions can be composed, and the type of the resulting system is derived from those of its …
Developing autonomous agents that can reason about the perspective of their (human or artificial) peers is paramount to realistically model a variety of real-world domains. Being aware of the state of mind of others is a key aspect in different …
Attribute-based memory updates (AbU in short) is an interaction mechanism recently introduced for adapting the Event-Condition-Action (ECA) programming paradigm to distributed systems, particularly suited for the IoT. It can be seen as a memory-based …
Ordering the collection of states of a given automaton starting from an order of the underlying alphabet is a natural move towards a computational treatment of the language accepted by the automaton. Along this path, Wheeler graphs have been recently …
In this paper we reason about the notion of proportional lumpability, that generalizes the original definition of lumpability to cope with the state space explosion problem inherent to the computation of the performance indices of large stochastic …
We present a graphical simulator of 1-Tape, k-Tapes, deterministic and non deterministic Turing machines. The simulator is written in Java and as such it runs on most platforms. During and after the computation it returns interesting features such as …