Title: Insecurity problem for assertions

Speaker: S P Suresh    (bio) (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.

When: Tuesday, 07 January 2024 at 1900 hrs (IST)  

Meeting Details: Zoom link, 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.