Marino Miculan

Associate Professor of Computer Science at DMIF, University of Udine. (Qualified as full professor since March 2018)

This webpage collects some information about my research, including my publications, the projects I am involved in, and my teaching and professional activities.

Currently, I am mostly interested in security issues of distributed, component-based and smart systems, whose overall behavior is determined by the interaction of many heterogeneous entities. To this end, I am applying formal methods (possibly with a pinch of Machine Learning) to define new models, languages, methodologies and techniques for the formalisation, verification and certification of security properties of these systems.
If this sounds interesting to you too, drop me a note.

Besides, I know one or two things about process calculi, distributed ledgers, session types, category theory and logic, bigraphs, coalgebras, structured operational semantics, nominal sets, systems biology, type theory, logical frameworks, proof assistants. (In a sense, I am a horizontal researcher.)

I founded and lead the Models and Applications of Distributed Systems laboratory, the Udine node of the CINI National CyberSecurity laboratory, and the MadrHacks, the ethical hacking team of the University of Udine.
I have the fortune to work with great people.

latest news (more)

Jun 4, 2023	MadrHacks have maxed the DanteCTF 🐍
May 24, 2023	Talk about "Behavioral Equivalences for AbU: Verifying Security and Safety in Distributed IoT Systems" at IMT, Lucca
May 23, 2023	Talk about "Bigraphical models for Container-based Systems" at DI, UniPI
May 5, 2023	I am honored to serve on the Program Committee of IEEE SBAC-PAD 2023.
May 3, 2023	I am chairing the Encryption and Formal Methods session of the Scientific Track at ITASEC 2023.

selected publications (more)

Automated Verification of Telegram’s MTProto 2.0 in the Symbolic Model

Marino Miculan, and Nicola Vitacolonna

Computers & Security 2023

Abs HTML

MTProto 2.0 is the suite of security protocols for instant messaging at the core of the popular Telegram messenger application. In this paper we analyse MTProto 2.0 using ProVerif, a state-of-the-art symbolic security protocol verifier based on the Dolev-Yao model. We provide the first formal symbolic model of MTProto 2.0; in this model, we provide fully automated proofs of the soundness of authentication, normal chat, end-to-end encrypted chat, and rekeying mechanisms with respect to several security properties, including authentication, integrity, secrecy and perfect forward secrecy. At the same time, we discover that the rekeying protocol is vulnerable to an unknown key-share (UKS) attack. To achieve these results, we proceed in an incremental way: each protocol is examined in isolation, relying only on the guarantees provided by the previous ones and the robustness of the basic cryptographic primitives. The importance of this research is threefold. First, it proves the formal correctness of MTProto 2.0 with respect to most relevant security properties. Secondly, we isolate the aspects of cryptographic primitives that escape the symbolic model and thus require further investigation in the computational model. Finally, our modelisation can serve as a reference for the implementation and analysis of clients and servers.
Composable partial multiparty session types for open systems

Claude Stolze, Marino Miculan, and Pietro Di Gianantonio

Software and Systems Modeling 2023

HTML
The AbU Language: IoT Distributed Programming Made Easy

Michele Pasqua, Massimo Comuzzo, and Marino Miculan

IEEE Access 2022

HTML
Computing (optimal) embeddings of directed bigraphs

Alessio Chiapperini, Marino Miculan, and Marco Peressotti

Sci. Comput. Program. 2022

HTML