EMV is the international protocol standard for smartcard payments and is used in billions of payment cards worldwide. Despite the standard’s advertised security, various issues have been previously uncovered, deriving from logical flaws that are hard to spot in EMV’s lengthy and complex specification, running over 2,000 pages.

We have formalized various models of EMV in Tamarin, a symbolic model checker for cryptographic protocols. Tamarin was extremely effective in finding critical flaws, both known and new. For example, we discovered multiple ways that an attacker can use a victim's EMV card (e.g., Mastercard or Visa Card) for high-valued purchases without the victim's supposedly required PIN. Said more simply, the PIN on your EMV card is useless! We report on this, as well as followup work with an EMV consortium member on verifying the latest, improved version of the protocol, the EMV Kernel C-8. Overall our work provides evidence that security protocol model checkers like Tamarin have an essential role to play in developing real-world payment protocols and that they are up to this challenge.

Phishing remains one of the most effective cyber threats, affecting millions of organizations. Phishing education, training, and awareness programs are used to address employees’ lack of knowledge about phishing attacks. However, despite being very expensive, these interventions are not always effective, mainly due to the lack of customization of training materials based on the employees’ needs and profiles. In fact, creating customized training content for each employee and each context would require a huge effort from security practitioners and educators thus increasing costs even more. The proposal we present in this talk is to use Large Language Models to automate some steps in the design process of training content, which is tailored to the specific user profile. Joint work with Giuseppe Desolda and Francesco Greco of the University of Bari.

No-go theorems (Bell, Kochen–Specker, …) formally show the departure of quantum theory from the classical worldview. These are formulated in the framework of ontological models and, if one accepts such framework, entail that quantum theory involves problematic (“fine-tuned”) properties. I will argue that the lesson to take from the no-go theorems is to abandon the framework of ontological models as the way to model reality. I will analyze what I believe to be the unnatural assumptions of such framework and I will propose a way to change it. The basic principle of the new notion of reality I propose is that for something to exist is for something to be recorded. I will motivate the principle and explore its consequences. In order to implement such proposal into a precise theory-independent mathematical framework I will make use of point-free topological spaces (locales). I will discuss why this new proposal should be promising for circumventing the conclusions of Bell’s theorem and understanding quantum theory. I will conclude by presenting several open questions.