Disputation: Antonio Gonzalez Burgueño

Doctoral candidate Antonio Gonzalez Burgueño at the Department of informatics, Faculty of Mathematics and Natural Sciences, is defending the thesis: Formal Analysis for Security Ceremonies for the degree of Philosophiae Doctor.

Image may contain: Tie, White-collar worker, Chin, Forehead, Tie.

The University of Oslo is closed. The PhD defence and trial lecture will therefore be fully digital and streamed directly using Zoom. The host of the session will moderate the technicalities while the chair of the defence will moderate the disputation.

Ex auditorio questions: the chair of the defence will invite the audience to ask ex auditorio questions either written or oral. This can be requested by clicking 'Participants -> Raise hand'. 


Trial lecture

"Verifying and attacking machine learning systems for cyber security"

Main research findings

In this thesis, I have developed a mathematical framework that can be used to accurately represent and reason about communication processes that include different kinds of actors, including human beings, with different capabilities and knowledge.

I have also used this mathematical framework to analyze the security properties of a range of systems, including the YubiKey authentication device and its secure hardware module (YubiHSM) used by a wide range of companies like Google, Facebook, GitHub or Microsoft. Furthermore, it provided me with the possibility to analyze security properties as secrecy and authentication in communication processes in which different actors with different capabilities and knowledge, including human beings, can interact to achieve a common goal.

I also present how some of today’s modern security systems, as the RSA Laboratories Public Key Standards PKCS#11, a standard in the industry, the YubiKey, and the YubiHSM, can be logically and automatically analyzed using the state-of-the-art Maude-NPA security analysis tool. This research progresses with the research on the PKCS#11 verification by performing the API analysis in a more general and realistic model than in other previous works. Besides, by using the Maude-NPA tool, we can perform the analysis of the PKCS#11 API in a fully-unbounded session model. Furthermore, in the YubiKey and YubiHSM devices’ analysis, we automatically prove the secrecy and authentication properties of YubiKey and found two different attacks on the YubiHSM HSM, going further than any other previous work.


Contact information to Department: Mozhdeh Sheibani Harat

Publisert 4. juni 2020 10:14 - Sist endret 29. juni 2021 10:35