Dear all, The next talk in the IARCS Verification Seminar Series will be given by S P Suresh, a faculty member of Theoretical Computer Science at the Chennai Mathematical Institute. The talk is scheduled on Tuesday, January 7, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=N2xkbWs1a2xzcGhzNTY5bGszc3Q5NGY3OG8gdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/), and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas. All are welcome to join. Best regards, Akash, Deepak, Madhukar, Srivathsan ============================================================= Title: Insecurity problem for assertions Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: Security protocols underpin most aspects of our digital lives nowadays, with finance, health, and even citizenship requiring some online interaction with remote servers over an insecure network, and involving exchange of sensitive private information. Formal verification of such protocols has a long history of more than 40 years (and applied on many fundamental protocols like TLS and the Signal messaging protocol, and various protocols for electronic voting, e-commerce, etc.). One of the central theoretical results [Rusinowitch-Turuani (2003)] is that the problem of deciding if there is a B-bounded attack on a given protocol is NP-complete, for a fixed number B. A B-bounded attack is one which involves at most B messages and in which a secret is leaked to the malicious attacker. The technical challenge is that although the number of messages is bounded in such attacks, the size of each message is not. In recent work [Ramanujam-Sundararajan-Suresh (2024)] we extended the above NP-completeness result to protocols that involve, in addition to "traditional" messages themselves, certificates or assertions of the form "the previous term that I sent is encrypted, and the term inside the encryption is a number between 1 to 10." In this talk, we describe the insecurity problem, and the solution by Rusinowitch-Turuani (RT03), and show how we can extend the analysis of RT03 to our setting. Bio: S P Suresh is a faculty member of Theoretical Computer Science at the Chennai Mathematical Institute. His research interests include logic in computer science, concurrency and distributed computing, and formal methods for security. His other interests include classical Indian logic and epistemology, Carnatic music, chess, and P G Wodehouse.