Operational Semantics of Security Protocols
2019-11-21 10:00 - 12:00 UTC | Facultatea de Matematica si Informatica, sala 202
Speaker: Ioana Leustean (University of Bucharest)

Abstract: After a brief overview of the formal methods used for analyzing security protocols, we will focus on the operational semantics developed in:
C. Cremers, S. Mauw, Operational Semantics and Verification of Security Protocols, Springer, 2012.

Executarea, detecţia și prevenţia atacurilor de tip R.O.P
2019-12-12 08:30 - 11:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala Google
Speaker: Sorin-Gabriel Radu (University of Bucharest)

Abstract: Va fi prezentată o versiune extinsă a lucrări de licență ce va prezenta concepte de Return Orientated Programming, o tehnică de reciclare și combinare a bucăților de cod existent, curat, astfel încât cod nou, nedorit, în general de tip malware, să fie executat.

Operational Semantics of Security Protocols II
2019-12-12 10:00 - 12:00 UTC | Facultatea de Matematica si Informatica, sala 202
Speaker: Ioana Leustean (University of Bucharest)

Abstract: We continue our presentation on operational semantics of security protocols, as developed in:
C. Cremers, S. Mauw, Operational Semantics and Verification of Security Protocols, Springer, 2012.

First-order logic and vagueness
2019-12-19 10:00 - 12:00 UTC | Facultatea de Matematica si Informatica, sala 202
Speaker: Marian Calborean (University of Bucharest)

Abstract: The Sorites paradox is usually studied as a propositional paradox. However, the general form of the Sorites is second-order, with three main features. It doesn’t contain any arbitrary parameters. It can be used to generate the propositional Sorites by appropriate replacement of the second-order premise with arbitrary clauses. Finally, it is generally nonfirstorderizable, relying on the notion of transitive closure of a relation. However, it can be expressed in FOL with a finite upper bound on the elements of the relation. This leads to a definition of vagueness in classical FOL, using the interplay between a total preorder and a monadic predicate. A notational extension of FOL will introduce a vague structure formed by the predicate (e.g.tall), the broad predicate (e.g. broadly tall) and the strict predicate (e.g. strictly tall). It allows the failure of a weak non-contradiction (e.g. ‘Some men are both broadly tall and broadly short’), the failure of a weak LEM (e.g. ‘Some men are neither strictly tall nor strictly short`), and the truth of a non-paradoxical tolerance (e.g. ‘If a person of n cm is strictly tall, a person of n-1 cm is broadly tall’).
References:
[1] P. Cobreros, P. Egré, D. Ripley, R, Van Rooij, Tolerant, Classical, Strict, Journal of Philosophical Logic 41 (2019), 347-385.
[2] D. Graff, Shifting Sands: An Interest-Relative Theory of Vagueness, Philosophical Topics 28 (2000), 45-81.
[3] U. Keller, Some remarks on the definability of transitive closure in first-order logic and Datalog, Internal report, Digital Enterprise Research Institute (DERI), University of Innsbruck, 2004.
[4] K.G. Lucey, he ancestral relation without classes, Notre Dame Journal of Formal Logic 20 (1979), 281-284.

Off-the-Record Communication (OTR) si CryptoGo (joc de carti de criptografie)
2019-12-19 18:30 - 20:00 UTC | Facultatea de Matematica si Informatica, amf.2 (Pompei)
Title: Off-the-Record Communication (OTR)
Speaker: Mihail-Iulian Plesa

Abstract: Off-the-Record Communication (OTR) este un protocol care modealeaza o discutie dintre doua entitati, care ar trebui sa satisfaca anumite proprietati de securitate. Vom vorbi despre proprietatile acestui tip de comunicatie si despre cum pot fi acestea implementate in mediul online. Vom discuta apoi despre protocolul OTR integrat in Signal si cum anume difera acesta fata de versiunea originala.
Nota: Prezentarea va fi urmata de o sesiune de joc CryptoGo – joc de carti educational pentru criptografie.
Mai multe informatii aici.

Challenges in Banking
2020-01-30 08:30 - 10:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala Google
Speaker: Horia Velicu (BRD – Groupe Societe Generale)

Abstract: Presentation of topics of interest for 2020, objectives and data available at BRD. Proposals for the themes for the applied research institute that will be sponsored this year. Presentation of the new BRD AI Hub.

A quantitative analysis of the “Lion-Man” game
2020-02-27 10:00 - 12:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala Google
Speaker: Ulrich Kohlenbach (Technische Universität Darmstadt)
Title: A quantitative analysis of the “Lion-Man” game
Abstract: We analyze, based on an interplay between ideas and techniques from logic and geometric analysis, a pursuit-evasion game. More precisely, we focus on a discrete lion and man game with an ε-capture criterion. We prove that in uniformly convex bounded domains the lion always wins and, using ideas stemming from proof mining, we extract a uniform rate of convergence for the successive distances between the lion and the man. As a byproduct of our analysis, we study the relation among different convexity properties in the setting of geodesic spaces.
Joint work with Genaro López-Acedo and Adriana Nicolae.

References:
[1] U. Kohlenbach, G. López-Acedo, A. Nicolae, A quantitative analysis of the “Lion-Man” game. arXiv:1806.04496 [math.MG], 2019. Submitted.

BLOCKCHAIN - More than a buzzword
2020-03-02 18:30 - 20:00 UTC | Facultatea de Matematica si Informatica, sala 219
Title: BLOCKCHAIN – More than a buzzword
Speaker: Ionut-Daniel Dobos (MBN Technologies)

Abstract: In this presentation we will take a look at the concept of a blockchain as a mean to hold historical transactional data (while maintaining all the core concepts of Cryptography) and moreover, to see how IPFS uses such approaches to ensure a way of general data storage with the same capabilities. We will choose the Ethereum network as a use case for the first topic, taking a deeper look into the upcoming Casper update for the consensus mechanism, introducing the Proof of Stake paradigm.

POSTPONED: Securing Businesses and Critical Infrastructure
2020-03-12 08:30 - 10:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala Google
POSTPONED UNTIL FURTHER NOTICE.

Speaker: Ioan Constantin (Orange Romania)

Abstract: A brief walkthrough some of the challenges in offering advanced cyber security solutions for Business and Critical Infrastructures, from a Managed Security Services Provider’s standpoint. We’ll talk threat detection and mitigation, the specifics of OT Security in Critical Infrastructure, compliance and best practices. We’ll also glance at some of the research and development in these areas.

POSTPONED: Protocols in Dynamic Epistemic Logic
2020-03-12 10:00 - 12:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala 202
POSTPONED UNTIL FURTHER NOTICE.

Speaker: Alexandru Dragomir (University of Bucharest)

Title: Protocols in Dynamic Epistemic Logic
Abstract: Dynamic epistemic logics are useful in reasoning about knowledge and certain acts of learning (epistemic actions). However, not all epistemic actions are allowed to be executed in an initial epistemic model, and this is where the concept of a protocol comes in: a protocol stipulates what epistemic actions are allowed to be performed in a model. The aim of my presentation is to introduce the audience to the account of protocols in [1, 2].

References:
[1] H. van Ditmarsch, S. Ghosh, R. Verbrugge, Y. Wang, Hidden protocols: Modifying our expectations in an evolving world, Artificial Intelligence 208 (2014), 18-40.
[2] Y. Wang, Epistemic Modelling and Protocol Dynamics, PhD thesis, University of Amsterdam, 2010.

Formalizing Gödel's System T in Lean
2021-02-25 10:00 - 12:00 (Europe/Bucharest)
Title: Formalizing Gödel’s System T in Lean
Speaker: Horațiu Cheval (University of Bucharest)

Abstract:

In 1958, Gödel introduced his functional interpretation as a method of reducing the consistency of first-order arithmetic to that of a quantifier-free system of primitive recursive functionals of higher type. His work has since enabled other advances in proof theory, notably the program of proof mining. We give a brief overview of Gödel’s System T and then explore a formalization thereof as a deep embedding in the Lean proof assistant.
References:

[1] mathlib Community, The Lean Mathematical Library, 2019.

Unwinding of proofs
2021-03-04 10:00 - 12:00 (Europe/Bucharest)
Title: Unwinding of proofs
Speaker: Pedro Pinto (TU Darmstadt)

Abstract:
The unwinding of proofs program dates back to Kreisel in the fifties and rests on the following broad question: “What more do we know if we have proved a theorem by restricted means than if we merely know that it is true?”

This research program has since been dubbed proof mining and has been greatly developed during the last two decades and emerged as a new form of applied proof theory [1,2]. Through the use of proof-theoretical tools, the proof mining program is concerned with the unveil of hidden finitary and combinatorial content from proofs that use infinitary noneffective principles.

In this talk, we set out to give a brief introduction to the proof mining program, focusing on the following points:

functional interpretations in an introductory way;
the bounded functional interpretation [3,4];
a concrete translation example: the metric projection argument.

We finish with a brief discussion of some recent results [5,6].
References:

[1] U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg, 2008.
[2] U. Kohlenbach. Proof-theoretic methods in nonlinear analysis. In M. Viana B. Sirakov, P. Ney de Souza, editor, Proceedings of the International Congress of Mathematicians – Rio de Janeiro 2018, Vol. II: Invited lectures, pages 61–82. World Sci. Publ., Hackensack, NJ, 2019.
[3] F. Ferreira and P. Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic, 135:73-112, 2005.
[4] F. Ferreira. Injecting uniformities into Peano arithmetic. Annals of Pure and Applied Logic, 157:122-129, 2009.
[5] B. Dinis and P. Pinto. Effective metastability for a method of alternating resolvents. arXiv:2101.12675 [math.FA], 2021.
[6] U. Kohlenbach and P. Pinto. Quantitative translations for viscosity approximation methods in hyperbolic spaces. arXiv:2102.03981 [math.FA], 2021.

References:

Exponential Diophantine equations over ℚ
2021-03-11 10:00 - 12:00 (Europe/Bucharest)
Title: Exponential Diophantine equations over ℚ
Speaker: Mihai Prunescu (University of Bucharest & IMAR)

Abstract:

In a previous exposition [1] we have seen that the solvability over ℚ is undecidable for systems of exponential Diophantine equations. We now show that the solvability of individual exponential Diophantine equations is also undecidable, and that this happens as well for some narrower families of exponential Diophantine equations.
References:

[1] M. Prunescu, The exponential Diophantine problem for ℚ. The Journal of Symbolic Logic, Volume 85, Issue 2, 671–672, 2020.

A proof mining case study on the unit interval
2021-03-18 10:00 - 12:00 (Europe/Bucharest)
Title: A proof mining case study on the unit interval
Speaker: Andrei Sipoș (University of Bucharest & IMAR)

Abstract:

In 1991, Borwein and Borwein proved [1] the following: if L>0, f : [0,1] → [0,1] is L-Lipschitz, (xn), (tn) ⊆ [0,1] are such that for all n, xn+1=(1-tn)xn+tnf(xn) and there is a δ>0 such that for all n, tn≤(2-δ)/(L+1), then the sequence (xn) converges.
The relevant fact here is that the main argument used in their proof is of a kind that hasn’t been analyzed yet from the point of view of proof mining, and thus it may serve as an illustrative new case study. We shall present our work [2] on the proof, showing how to extract a uniform and computable rate of metastability for the above family of sequences.
References:

[1] D. Borwein, J. Borwein, Fixed point iterations for real functions. J. Math. Anal. Appl. 157, no. 1, 112–126, 1991.
[2] A. Sipoș, Rates of metastability for iterations on the unit interval. arXiv:2008.03934 [math.CA], 2020.

Regular matching problems for infinite trees
2021-03-25 10:00 - 12:00 (Europe/Bucharest)
Title: Regular matching problems for infinite trees
Speaker: Mircea Marin (West University of Timișoara)

Abstract:
We study the matching problem “∃σ:σ(L)⊆R?” where L and R are regular tree languages over finite ranked alphabets X and Σ respectively, and σ is a substitution such that σ(x) is a set of trees in T(Σ∪H)∖H for all x∈X. Here, H denotes a set of holes which are used to define a concatenation of trees. Conway studied this problem in the special case for languages of finite words in his classical textbook Regular algebra and finite machines and showed that if L and R are regular, then the problem “∃σ:∀x∈X:σ(x)≠∅∧σ(L)⊆R?” is decidable. Moreover, there are only finitely many maximal solutions, which are regular and effectively computable. We extend Conway’s results when L and R are regular languages of finite and infinite trees, and language substitution is applied inside-out. We show that if L⊆T(X) and R⊆T(Σ) are regular tree languages then the problem “∃σ∀x∈X:σ(x)≠∅∧σio(L)⊆R?” is decidable. Moreover, there are only finitely many maximal solutions, which are regular and effectively computable. The corresponding question for the outside-in extension σoi remains open, even in the restricted setting of finite trees. Our main result is the decidability of “∃σ:σio(L)⊆R?” if R is regular and L belongs to a class of tree languages closed under intersection with regular sets. Such a special case pops up if L is context-free.
This is joint work with Carlos Camino, Volker Diekert, Besik Dundua and Géraud Sénizergues.

References:
[1] C. Camino, V. Diekert, B. Dundua, M. Marin, G. Sénizergues, Regular matching problems for infinite trees. arXiv:2004.09926 [cs.FL], 2021.

An Introduction to Protocols in Dynamic Epistemic Logic
2021-04-01 10:00 - 12:00 (Europe/Bucharest)
Title: An Introduction to Protocols in Dynamic Epistemic Logic
Speaker: Alexandru Dragomir (University of Bucharest)

Abstract:
Dynamic epistemic logics are useful in reasoning about knowledge and acts of learning, seen as epistemic actions. However, not all epistemic actions are allowed to be executed in an initial epistemic model, and this is where the concept of a protocol comes in: a protocol stipulates what epistemic actions are allowed to be performed in a model. The aim of my presentation is to introduce the audience to two accounts of protocols in DEL: Hoshi’s [1], and Wang’s [2].

References:
[1] T. Hoshi, Epistemic dynamics and protocol information. PhD thesis, Stanford, CA, USA, 2009.
[2] Y. Wang, Epistemic Modelling and Protocol Dynamics. PhD thesis, University of Amsterdam, 2010.

Kernelization, Proof Complexity and Social Choice
2021-04-22 10:00 - 12:00 (Europe/Bucharest)
Title: Kernelization, Proof Complexity and Social Choice
Speaker: Gabriel Istrate (West University of Timișoara)

Abstract:

We display an application of the notions of kernelization and data reduction from parameterized complexity to proof complexity: Specifically, we show that the existence of data reduction rules for a parameterized problem having (a) a small-length reduction chain, and (b) small-size (extended) Frege proofs certifying the soundness of reduction steps implies the existence of subexponential size (extended) Frege proofs for propositional formalizations of the given problem. We apply our result to infer the existence of subexponential Frege and extended Frege proofs for a variety of problems. Improving earlier results of Aisenberg et al. (ICALP 2015), we show that propositional formulas expressing (a stronger form of) the Kneser-Lovasz Theorem have polynomial size Frege proofs for each constant value of the parameter k. Previously only quasipolynomial bounds were known (and only for the ordinary Kneser-Lovasz Theorem). Another notable application of our framework is to impossibility results in computational social choice: we show that, for any fixed number of agents, propositional translations of the Arrow and Gibbard-Satterthwaite impossibility theorems have subexponential size Frege proofs.
This is joint work with Cosmin Bonchiș and Adrian Crăciun.

Active Defense in Cybersecurity
2021-05-26 16:00 - 20:00 (Europe/Bucharest) | online (via Teams)
Title: Active Defense in Cybersecurity
Speaker: Sergiu Bogdan Meseșan & Andreea Drugă, Cybersecurity Specialists at ENEA

Agenda:

Active Defense Mechanisms – Notions, principles and Active Defense mechanisms (ca.1h)

Practical Application for Honeypot Analytics and Attacks Data Collection – Presentation of a platform implemented by ENEA specially for this lecture, a practical demo of Active Defense (ca.1h)

Active Defense DIY – Workshop installation, running, Internet access for a Honeypot type VM using an open source platform (Telekom Tpot CE) (ca.1h-1.5h)

For the students interested to attend the meeting: please contact Ruxandra Olimid (ruxandra.olimid@fmi.unibuc.ro)

Introduction in Quantum Computing
2026-03-06 09:00 - 10:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala S.211
Title: Introduction in Quantum Computing
Speaker: Mihai Prunescu (UB)

Abstract: Basing QC notions are presented: superposition, wave-function and probability, qubit, independence, entanglement.

Introduction in Quantum Computing (II)
2026-03-27 09:00 - 10:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala S.213
Title: Introduction in Quantum Computing (II)
Speaker: Mihai Prunescu (UB)

Abstract: We continue the discussion on QC.

Cybersecurity of Industrial Control Systems
2026-04-02 14:00 - 16:00 (Europe/Bucharest) | 503 PBT
Title: Cybersecurity of Industrial Control Systems
Speaker: Stéphane Mocanu (INRIA)

Abstract: In this talk, we discuss the state of the art of industrial control systems cybersecurity. Based on classical events, we analyse the typical threats and the vulnerabilities that they exploit. In the second part of the talk, we present the security architectures and security practices as recommended by international standards (ISO 27000, IEC 62443) and NIST Cybersecurity Framework).

Introduction in Quantum Computing (III)
2026-04-03 09:00 - 10:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala S.213
Title: Introduction in Quantum Computing (III)
Speaker: Mihai Prunescu (UB)

Abstract: We continue the discussion on QC.
