Verifying security protocols using BAN logic

Speaker: Alexandru Dragomir (University of Bucharest)


Abstract: Epistemic logics – logics aimed at reasoning about knowledge and belief – are widely considered to be suitable for modelling, analyzing and predicting vulnerabilities of security protocols. One of the first and most discussed logical approaches to the problem of verifying security protocols is the one proposed in BAN logic (Burrows, Abadi & Needham 1989), a many-sorted epistemic logic used for its intuitive and compelling set of inference rules devised for reasoning about an agent’s beliefs, trust and message exchange. My presentation will focus on (1) briefly presenting the language and inference rules of BAN logic, (2) offering a presentation of the Otway-Rees, Needham-Schroeder and Kerberos protocols, and (3) analysing the aforementioned protocols using BAN logic.

Fully Homomorphic Encryption (FHE)

Speaker:  Ana Costache


Abstract:

Fully homomorphic encryption este un tip de criptare care permite manipularea datelor criptate pastrand securitatea acestora. Ana va introduce notiunea de latice, si va defini FHE. De asemenea, va vorbi despre librarii FHE si despre relevanta FHE in lumea comerciala.

Lindström’s Theorems

Speaker: Mihai Prunescu (University of Bucharest)


Abstract: Regular logic systems which are strictly stronger than the first order predicate calculus cannot satisfy in the same time Löwenheim-Skolem for statements and compacity (Lindström 1). Effectively presented such systems cannot satisfy in the same time Löwenheim-Skolem for statements and the condition that the set of generally valid sentences is recursively enumerable (Lindström 2). We sketch the proof that uses partial isomorphisms.

References:
[1] H.-D. Ebbinghaus, J. Flum, W. Thomas, Mathematical Logic. Second edition, Undergraduate Texts in Mathematics, Springer, 1996.

Functional Encryption (FE)

Speaker:  Radu Titiu


Abstract:

Functional Encryption (FE) este o primitiva criptografica moderna care generalizeaza notiunea de criptografie cu cheie publica in felul urmator. In mod normal algoritmul de decriptare se foloseste de cheia secreta pentru a recupera intreg mesajul criptat cu cheia publica. FE permite o decriptare controlata a mesajului: detinatorul cheii secrete K poate sa produca alta cheie secreta K_f asociata unei functionalitati f. Folosind cheia K_f un utilizator poate sa obtina f(mesaj) si nimic mai mult. O astfel de primitiva criptografica ar putea fi utilizata de un spital care tine datele pacientilor criptate dar care poate totusi oferi acces cercetatorilor la anumite statistici care ar putea ajuta la intelegerea anumitor boli. Toate acestea sunt posibile fara a divulga informatii despre pacienti.
In aceasta prezentare Radu va explica detaliat ce inseamna Functional Encryption si posibile aplicatii. De asemenea, va exemplifica conceptul printr-o constructie pentru o clasa restransa de functionalitati [2] si va vorbi despre cerintele de securitate pe care le satisface aceasta constructie.
Referinte:
[1] https://link.springer.com/chapter/10.1007%2F978-3-319-70500-2_8
[2] https://eprint.iacr.org/2015/608.pdf

An introduction to BAN logic (a logic of authentication)

Speaker: Alexandru Dragomir (University of Bucharest)


Abstract: One of the first and most discussed logical approaches to the problem of verifying security protocols is the one proposed in BAN logic (Burrows, Abadi & Needham 1989), a many-sorted modal logic used for its intuitive and compelling set of inference rules devised for reasoning about an agent’s beliefs, trust and message exchange. My presentation will focus on (1) presenting the language and inference rules of BAN logic, (2) following the original paper’s analysis of the Otway-Rees protocol, (3) presenting some objections to using BAN, and (4) discussing the problem of offering a semantics of BAN logic.

The hybridization of many-sorted polyadic modal logic

Speaker: Natalia Moangă (University of Bucharest).

Abstract: Hybrid logics are obtained by enriching modal logics with nominals and state variables, that directly refer the individual points in a Kripke model. In the present work we develop a hybrid version on top of our many-sorted polyadic logic, previously defined. Our system has nominals and state variables on each sort, as well as binders that act like the universal and the existential quantfiers on state variables. In doing this, we follow various approaches for hybrid modal logic, especially the work of Blackburn and Tsakova.