My initial research was rather theoretical, dating back to my final undergraduate dissertation at UNICT and continuing during my Ph.D. at Cambridge University. It was formal methods what got me started, precisely with Gurevich's "Evolving Algebras", now "Abstract State Machines", then with Paulson's "Inductive Method" for proving security protocols correct. I have worked on various incarnations of security protocols over the years, e.g. for electronic exams and electronic voting, both from a design and from a formal verification standpoint. I have also used more recent tools such as Proverif and Tamarin, but my love remains with crystal-clear inductive reasoning. My early work culminates with
my book, published with Springer, a satisfying fatigue that made me promise it would be first and last in my life.
I am fond of people's different attitudes at thinking and, particularly, of how researchers from other disciplines approach the same challenges as mine. I have therefore worked with Biologists, Sociologists, Psychologists and Lawyers and I am super grateful to them for I can say that they taught me a great lot (we know that the "love of wisdom" drives a
Phylosophiae Doctor). Therefore, I have experienced how formal methods can help over computational and synthetic biology as well as address the human factor in cybersecurity; similarly, I feel I have approached the relevant cybersecurity and privacy regulations, directives and standards by somewhat conjugating a computational logician's and a passionate linguist's stances.
I could not resist getting more practical as well. For example, cybersecurity and privacy in the present automotive domain require a broad skill set. I have therefore contributed to low-level bus security through advanced prototypes of new cryptographic protocols and also to an in-depth understanding of drivers' privacy and corresponding user interface/experience. Last but not the least come the ever so fashionable Vulnerability Assessment and Penetration Testing, albeit dramatically useful too. I have built practical VAPT methodologies for a number of large-scale institutions. More for fun, I have also applied VAPT techniques to various IoT devices and unveiled vulnerabilities over some popular life companions such as printers, VoIP phones,
Amazon's Echo Dot and
TP-Link Tapo's smart bulbs.