See also my pages on IRIS, Google Scholar, DBLP, Scopus, Orcid, ResearchGate, SemanticScholar, MathSciNet.
My Erdős number is 3 (Miculan – Rizzi – Hell – Erdős).
2023
-
Composable partial multiparty session types for open systems
Claude Stolze, Marino Miculan, and Pietro Di Gianantonio
Software and Systems Modeling 2023
-
Automated Verification of Telegram’s MTProto 2.0 in the Symbolic Model
Marino Miculan, and Nicola Vitacolonna
Computers & Security 2023
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.
-
DBCChecker: a bigraph-based tool for checking security properties of container compositions
Andrea Altarui, Marino Miculan, and Matteo Paier
In Proceedings of the Seventh Italian Conference on Cyber Security, ITASEC 2023 2023
-
Modeling Carne PRI supply chain with the *-Chain Platform
Stefano Bistarelli, Francesco Faloci, Paolo Mori, Carlo Taticchi, and Marino Miculan
In Proceedings of the Fifth Distributed Ledger Technology Workshop (DLT 2023), Bologna, Italy, May 25-26, 2023 2023
-
AbU: A calculus for distributed event-driven programming with attribute-based interaction
Michele Pasqua, and Marino Miculan
Theoretical Computer Science 2023
In recent years, event-driven programming languages, in particular those based on Event Condition Action (ECA) rules, have emerged as a promising paradigm for implementing ubiquitous and pervasive systems. These implementations are mostly centralized, where a single server (often in the cloud) collects and processes all the inputs from the environment. In fact, placing the computation on the nodes interacting with the environment requires suitable abstractions for effective communication and coordination of (possibly large) ensembles of these distributed components — abstractions that current ECA languages are still missing. To this end, in this paper we present AbU, a calculus for modeling and reasoning about ECA-based systems with attribute-based communication. The latter is an interaction model recently introduced for the coordination of (possibly large) families of nodes: communication is similar to broadcast but the actual receivers are selected on the spot, by means of predicates over nodes properties. Thus, the programmer can specify interactions between nodes in a declarative way, abstracting from details such as nodes identity, number, or even their existence, without the need for a central server: the computation is moved on the “edge”, thus improving reliability, scalability, privacy and security. After having defined syntax and formal semantics of AbU, we showcase its expressiveness by providing some example applications and the encoding of AbC, the archetypal calculus with attribute-based communication. Then, we focus on two key properties of reactive systems: stabilization (i.e., termination of internal steps) and confluence. For both these properties we provide formal semantic definition, sufficient syntactic conditions on AbU systems, and algorithms to statically check such conditions. Hence, AbU is both a basis for the formal analysis of event-driven architectures with attributed-based interaction, and a reference model for a full-fledged language for IoT and edge computing.
-
Pairing an Autoencoder and a SF-SOINN for Implementing an Intrusion Detection System
Gabriele Voltan, Gian Luca Foresti, and Marino Miculan
In Proceedings of the Thematic Workshops co-located with the 3rd CINI National Lab AIIS Conference on Artificial Intelligence (Ital-IA 2023) 2023
2022
-
A new criterion for M,N-adhesivity, with an application to hierarchical graphs
Davide Castelnovo, Fabio Gadducci, and Marino Miculan
In Proc. FoSSaCS 2022
-
Fuzzy Algebraic Theories
Davide Castelnovo, and Marino Miculan
In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) 2022
-
The AbU Language: IoT Distributed Programming Made Easy
Michele Pasqua, Massimo Comuzzo, and Marino Miculan
IEEE Access 2022
-
CVE-2022-3203: ORing net IAP-420(+) Hidden Functionality
Lorenzo Bazzana, Marino Miculan, and Michele Codutti
2022
-
Computing (optimal) embeddings of directed bigraphs
Alessio Chiapperini, Marino Miculan, and Marco Peressotti
Sci. Comput. Program. 2022
-
A Calculus for Subjective Communication
Marino Miculan, and Matteo Paier
In Proceedings of the 23rd Italian Conference on Theoretical Computer Science, ICTCS 2022, Rome, Italy, September 7-9, 2022 2022
-
Distributed Programming of Smart Systems with Event-Condition-Action Rules
Michele Pasqua, and Marino Miculan
In Proceedings of the 23rd Italian Conference on Theoretical Computer Science, ICTCS 2022, Rome, Italy, September 7-9, 2022 2022
2021
-
Automated Symbolic Verification of Telegram’s MTProto 2.0
Marino Miculan, and Nicola Vitacolonna
In Proceedings of the 18th International Conference on Security and Cryptography, SECRYPT 2021 2021
-
On the Security and Safety of AbU Systems
Michele Pasqua, and Marino Miculan
In Software Engineering and Formal Methods (SEFM 2021) 2021
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 counterpart of attribute-based communication, keeping the simplicity of ECA rules.
-
Composable Partial Multiparty Session Types
Claude Stolze, Marino Miculan, and Pietro Di Gianantonio
In FACS 2021 Conference Proceedings 2021
-
Closure Hyperdoctrines
Davide Castelnovo, and Marino Miculan
In CALCO 2021 Conference Proceedings 2021
-
A time-series classification approach to shallow web traffic de-anonymization
Axel De Nardin, Marino Miculan, Claudio Piciarelli, and Gian Luca Foresti
In Proceedings of the Fifth Italian Conference on Cyber Security, ITASEC 2021 2021
-
A Calculus for Attribute-based Memory Updates
Marino Miculan, and Michele Pasqua
In Proceedings of the 18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021 2021
2020
-
Securing the Art Market with Distributed Public Ledgers
Marino Miculan, and Daniel Tosone
In Proceedings of the 3rd Distributed Ledger Technology Workshop (DLT 2020) 2020
-
Towards a Formal Model for Composable Container Systems
Fabio Burco, Marino Miculan, and Marco Peressotti
In Proceedings of the 35th Annual ACM Symposium on Applied Computing 2020
-
Computing Embeddings of Directed Bigraphs
Alessio Chiapperini, Marino Miculan, and Marco Peressotti
In Graph Transformation - 13th International Conference, ICGT 2020 2020
2019
-
An Abstract Distributed Middleware for Transactions over Heterogeneous Stores
Luca Geatti, Federico Igne, and Marino Miculan
In Proc. 20th Italian Conference on Theoretical Computer Science, ICTCS 2019 2019
-
Constructive logical characterizations of bisimilarity for reactive probabilistic systems
Marco Bernardo, and Marino Miculan
Theor. Comput. Sci. 2019
-
Towards User Recognition by Shallow Web Traffic Inspection
Marino Miculan, Gian Luca Foresti, and Claudio Piciarelli
In Proceedings of the Third Italian Conference on Cyber Security, Pisa, Italy, February 13-15, 2019 2019
2018
-
First and Second International Workshops on Meta Models for Process Languages (MeMo), Selected Papers
Thomas Hildebrandt, and Marino Miculan
2018
-
Deciding Hedged Bisimilarity
Alessio Mansutti, and Marino Miculan
In Proceedings of ICTCS 2018 2018
-
Loose Graph Simulations
Alessio Mansutti, Marino Miculan, and Marco Peressotti
In Software Technologies: Applications and Foundations 2018
We introduce loose graph simulations (LGS), a new notion about labelled graphs which subsumes in an intuitive and natural way subgraph isomorphism (SGI), regular language pattern matching (RLPM) and graph simulation (GS). Being a unification of all these notions, LGS allows us to express directly also problems which are “mixed” instances of previous ones, and hence which would not fit easily in any of them. After the definition and some examples, we show that the problem of finding loose graph simulations is NP-complete, we provide formal translation of SGI, RLPM, and GS into LGSs, and we give the representation of a problem which extends both SGI and RLPM. Finally, we identify a subclass of the LGS problem that is polynomial.
2017
-
Deciding Weak Weighted Bisimulation
Marino Miculan, and Marco Peressotti
In Proceedings of ICTCS 2017 2017
-
Reductions for Transition Systems at Work: Deriving a Logical Characterization of Quantitative Bisimulation
Marino Miculan, and Marco Peressotti
arXiv preprint arXiv:1704.07181 2017
-
LFMTP ’17: Proceedings of the Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
2017
2016
-
Disjunctive Probabilistic Modal Logic is Enough for Bisimilarity on Reactive Probabilistic Systems
Marco Bernardo, and Marino Miculan
In Proceedings of ICTCS 2016 2016
-
Special Issue on Methodologies, Technologies and Tools Enabling e-Government
2016
-
Structural operational semantics for non-deterministic processes with quantitative aspects
Marino Miculan, and Marco Peressotti
Theoretical Computer Science 2016
Abstract Recently, unifying theories for processes combining non-determinism with quantitative aspects (such as probabilistic or stochastically timed executions) have been proposed with the aim of providing general results and tools. This paper provides two contributions in this respect. First, we present a general {GSOS} specification format and a corresponding notion of bisimulation for non-deterministic processes with quantitative aspects. These specifications define labelled transition systems according to the {ULTraS} model, an extension of the usual {LTSs} where the transition relation associates any source state and transition label with state reachability weight functions (like, e.g., probability distributions). This format, hence called Weight Function {GSOS} (WF-GSOS), covers many known systems and their bisimulations (e.g. PEPA, TIPP, PCSP) and {GSOS} formats (e.g. GSOS, Weighted GSOS, Segala-GSOS). The second contribution is a characterization of these systems as coalgebras of a class of functors, parametric in the weight structure. This result allows us to prove soundness and completeness of the WF-GSOS specification format, and that bisimilarities induced by these specifications are always congruences.
-
A Specification of Open Transactional Memory for Haskell
Marino Miculan, and Marco Peressotti
CoRR 2016
-
On the bisimulation hierarchy of state-to-function transition systems
Marino Miculan, and Marco Peressotti
In Proceedings of ICTCS 2016 2016
2015
-
Distributed execution of bigraphical reactive systems
Alessio Mansutti, Marino Miculan, and Marco Peressotti
ECEASST 2015
-
Structural operational semantics for continuous state stochastic transition systems
Giorgio Bacci, and Marino Miculan
Journal of Computer and System Sciences 2015
Abstract In this paper we show how to model syntax and semantics of stochastic processes with continuous states, respectively as algebras and coalgebras of suitable endofunctors over the category of measurable spaces Meas. Moreover, we present an SOS-like rule format, called MGSOS, representing abstract {GSOS} over Meas, and yielding fully abstract universal semantics, for which behavioral equivalence is a congruence. An {MGSOS} specification defines how semantics of processes are composed by means of measure terms, which are expressions specifically designed for describing finite measures. The syntax of these measure terms, and their interpretation as measures, are part of the {MGSOS} specification. We give two example applications, with a simple and neat {MGSOS} specification: a “quantitative CCS”, and a calculus of processes living in the plane R 2 whose communication rate depends on their distance. The approach we follow in these cases can be readily adapted to deal with other quantitative aspects.
-
Behavioural equivalences for coalgebras with unobservable moves
Tomasz Brengos, Marino Miculan, and Marco Peressotti
Journal of Logical and Algebraic Methods in Programming 2015
We introduce a general categorical framework for the definition of weak behavioural equivalences, building on and extending recent results in the field. This framework is based on special order enriched categories, i.e. categories whose hom-sets are endowed with suitable complete orders. Using this structure we provide an abstract notion of saturation, which allows us to define various (weak) behavioural equivalences. We show that the Kleisli categories of many common monads are categories of this kind. On one hand, this allows us to instantiate the abstract definitions to a wide range of existing systems (weighted LTS, Segala systems, calculi with names, etc.), recovering the corresponding notions of weak behavioural equivalences; on the other, we can readily provide new weak behavioural equivalences for more complex behaviours, like those definable on presheaves, topological spaces, measurable spaces, etc.
-
PreProceedings of the 2nd International Workshop on Meta Models for Process Languages (MeMo 2015)
Marino Miculan
2015
-
Open Transactions on Shared Memory
Marino Miculan, Marco Peressotti, and Andrea Toneguzzo
In Coordination Models and Languages - 17th IFIP WG 6.1 International Conference, COORDINATION 2015, Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Grenoble, France, June 2-4, 2015, Proceedings 2015
2014
-
Multi-agent Systems Design and Prototyping with Bigraphical Reactive Systems
Alessio Mansutti, Marino Miculan, and Marco Peressotti
In Proc. DAIS 2014 2014
-
MeTTeG14, Proceedings of the 8th International Conference on Methodologies, Technologies and Tools Enabling e-Government
Barbara Re, and Marino Miculan
2014
-
A CSP implementation of the bigraph embedding problem
Marino Miculan, and Marco Peressotti
CoRR 2014
-
GSOS for non-deterministic processes with quantitative aspects
Marino Miculan, and Marco Peressotti
In Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014, Grenoble, France, 12-13 April 2014. 2014
-
Finding a Forest in a Tree — The matching problem for wide reactive systems
Giorgio Bacci, Marino Miculan, and Romeo Rizzi
In Trustworthy Global Computing - 9th International Symposium, TGC 2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers 2014
-
A Model of Countable Nondeterminism in Guarded Type Theory
A. Bizjak, Lars Birkedal, and Marino Miculan
In Proc. RTA-TLCA 2014
-
Behavioural equivalences for coalgebras with unobservable moves
Tomasz Brengos, Marino Miculan, and Marco Peressotti
CoRR 2014
-
Tutorial on Bigraphical Reactive Systems (slides)
Marino Miculan
In 1st International Workshop on Meta Models for Process Languages (MeMo) 2014
2013
-
Bigraphs Reloaded
Marino Miculan, and Marco Peressotti
2013
-
Weak bisimulations for labelled transition systems weighted over semirings
Marino Miculan, and Marco Peressotti
CoRR 2013
2012
-
Synthesis of Distributed Mobile Programs Using Monadic Types in Coq
Marino Miculan, and Marco Paviotti
In Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings 2012
-
Measurable Stochastics for Brane Calculus
Giorgio Bacci, and Marino Miculan
Theoretical Computer Science 2012
-
Structural operational semantics for continuous state probabilistic processes
Giorgio Bacci, and Marino Miculan
In Proc. CMCS’12 2012
-
Implementing the Stochastics Brane Calculus in a Generic Stochastic Abstract Machine
Marino Miculan, and Ilaria Sambarino
In Proceedings 6th Workshop on Membrane Computing and Biologically Inspired Process Calculi, Newcastle, UK, 8th September 2012 2012
2011
-
Unobservable Intrusion Detection Based on Call Traces in Paravirtualized Systems
Carlo Maiero, and Marino Miculan
In Proc. SECRYPT 2011
-
Formal analysis of Facebook Connect Single Sign-On authentication protocol
Marino Miculan, and Caterina Urban
In SofSem 2011, Proceedings of Student Research Forum 2011
2010
-
Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice
Karl Crary, and Marino Miculan
2010
-
Graph Algebras for Bigraphs
Davide Grohmann, and Marino Miculan
In Proc. 9th International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT’10) 2010
-
Measurable Stochastics for Brane Calculus
Giorgio Bacci, and Marino Miculan
In Proc. MeCBIC 2010
2009
-
DBtk: a Toolkit for Directed Bigraphs
Giorgio Bacci, Davide Grohmann, and Marino Miculan
In CALCO 2009 Conference Proceedings - Calco Tools 2009
-
Bigraphical models for protein and membrane interactions
Giorgio Bacci, Davide Grohmann, and Marino Miculan
In Proc. MeCBIC’09 2009
-
Deriving Barbed Bisimulations for Bigraphical Reactive Systems
Davide Grohmann, and Marino Miculan
In Proceedings of International Conference on Graph Transformation (ICGT-DS 2008) 2009
-
A framework for protein and membrane interactions
Giorgio Bacci, Davide Grohmann, and Marino Miculan
In Proc. MeCBIC’09 2009
2008
-
Undecidability of Model checking in Brane Logic
Giorgio Bacci, and Marino Miculan
Electronic Notes in Theoretical Computer Science 2008
-
Controlling resource access in Directed Bigraphs (long version)
Davide Grohmann, and Marino Miculan
In Proc. 7th International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT’08) 2008
-
Types for Proofs and Programs, International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers
Marino Miculan, Ivan Scagnetto, and Furio Honsell
2008
-
A categorical model of the Fusion calculus
Marino Miculan
In Proc. XXIV MFPS 2008
-
An Algebra for Directed Bigraphs
Davide Grohmann, and Marino Miculan
Electronic Notes in Theoretical Computer Science 2008
-
Implementing Spi-Calculus Using Nominal Techniques
Temesghen Kahsai, and Marino Miculan
In Proc. Computability in Europe (CiE) 2008
-
PicNIc – Pi-calculus Non-Interference checker
Silvia Crafa, Matteo Mio, Marino Miculan, Carla Piazza, and Sabina Rossi
In Proc. ACSD’08 2008
2007
-
Reactive Systems over Directed Bigraphs
Davide Grohmann, and Marino Miculan
In Proc. CONCUR 2007 2007
-
Directed bigraphs
Davide Grohmann, and Marino Miculan
In Proc. XXIII MFPS 2007
-
Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts
Alberto Ciaffaglione, Luigi Liquori, and Marino Miculan
J. Autom. Reasoning 2007
2006
-
Directed bigraphs: theory and applications
Davide Grohmann, and Marino Miculan
2006
-
Consistency of the Theory of Contexts
Anna Bucalo, Martin Hofmann, Furio Honsell, Marino Miculan, and Ivan Scagnetto
Journal of Functional Programming 2006
-
Modal Logics for Brane Calculus
Marino Miculan, and Giorgio Bacci
In Proc. CMSB 2006
-
On permutation algebras, (pre)sheaves and named sets
Fabio Gadducci, Marino Miculan, and Ugo Montanari
Higher-Order and Symbolic Computation 2006
2005
-
Implementazione di Memoria Distribuita su cluster CompactPCI
Maja Massarini, Marino Miculan, and Francesco Sepic
In Atti del Congresso AICA 2005 2005
-
A unifying model of variables and names
Marino Miculan, and Kidane Yemane
In Proc. FOSSACS’05 2005
2004
-
-
Modeling Fresh Names in π-calculus Using Abstractions
Roberto Bruni, Furio Honsell, Marina Lenisa, and Marino Miculan
In Proc. CMCS’04 2004
-
Unifying Recursive and Co-recursive Definitions in Sheaf Categories
Pietro Di Gianantonio, and Marino Miculan
In Proc. FOSSACS’04 2004
2003
-
Foundations of Software Science and Computation Structures (FOSSACS 2001), Selected Papers
Furio Honsell, and Marino Miculan
2003
-
Imperative Object-based Calculi in (Co)Inductive Type Theories
Alberto Ciaffaglione, Luigi Liquori, and Marino Miculan
In Proc. LPAR 2003
-
Reasoning on an Imperative Object-based Calculus in Higher Order Abstract Syntax
Alberto Ciaffaglione, Luigi Liquori, and Marino Miculan
In Proc. 2nd MERLIN 2003
-
A Unifying Approach to Recursive and Co-recursive Definitions
Pietro Di Gianantonio, and Marino Miculan
In Proc. TYPES’02 2003
-
A Framework for Typed HOAS and Semantics
Marino Miculan, and Ivan Scagnetto
In Proc. PPDP’03 2003
-
Mechanized Reasoning about Languages with Variable Binding
Furio Honsell, Marino Miculan, and Alberto Momigliano
2003
2002
-
Ambient Calculus and its Logic in the Calculus of Inductive Constructions
Ivan Scagnetto, and Marino Miculan
In Proc. Third International Workshop on Logical Frameworks and Meta-Languages (LFM’02) 2002
-
Comparing higher-order encodings in logical frameworks and tile logic
Roberto Bruni, Furio Honsell, Marina Lenisa, and Marino Miculan
Electronic Notes in Theoretical Computer Science 2002
2001
-
Proceedings of TOSCA 2001 - Theory of Concurrency, Higher Order Languages and Types
Marina Lenisa, and Marino Miculan
2001
-
The Theory of Contexts for First-Order and Higher-Order Abstract Syntax
Furio Honsell, Marino Miculan, and Ivan Scagnetto
In Proc. TOSCA’01 2001
-
Developing (Meta)Theory of Lambda-calculus in the Theory of Contexts
Marino Miculan
In Proc. MERLIN 2001 2001
-
An axiomatic approach to metareasoning on systems in higher-order abstract syntax
Furio Honsell, Marino Miculan, and Ivan Scagnetto
In Proc. ICALP’01 2001
-
On the formalization of the modal µ-calculus in the Calculus of Inductive Constructions
Marino Miculan
Information and Computation 2001
-
Proceedings of FOSSACS 2001
Furio Honsell, and Marino Miculan
2001
-
π-calculus in (Co)Inductive Type Theory
Furio Honsell, Marino Miculan, and Ivan Scagnetto
Theoretical Computer Science 2001
1999
-
Formalizing a lazy substitution proof system for µ-calculus in the Calculus of Inductive Constructions
Marino Miculan
In Proc. ICALP’99 1999
-
The Journal of High Energy Physics: Scientific Publishing on the Web
Simona Cerrato, Fabio Asnicar, Paolo Dall’Aglio, Amanda Felice, Massimo Di Fant, Marco Mizzaro, Fabrizio Nesti, Maria Candusso, and Marino Miculan
In Proceedings of WebNet 99 - World Conference on the WWW and Internet, Honolulu, Hawaii, USA, October 24-30, 1999 1999
1998
-
Encoding Modal Logics in Logical Frameworks
Arnon Avron, Furio Honsell, Marino Miculan, and Cristian Paravano
Studia Logica 1998
-
A Natural Deduction style proof system for propositional µ-calculus and its formalization in inductive type theories
Marino Miculan
In Proc. ICTCS’98 1998
1997
-
Encoding Logical Theories of Programs
Marino Miculan
1997
1995
-
Modal µ-Types for Processes
Marino Miculan, and Fabio Gadducci
In Proc. 10th LICS 1995
-
A Natural Deduction Approach to Dynamic Logics
Furio Honsell, and Marino Miculan
In Proc. TYPES’95 1995
1994
-
The Expressive Power of Structural Operational Semantics with Explicit Assumptions
Marino Miculan
In Types for Proofs and Programs, International Workshop TYPES’93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers 1994