In the formal analysis of security protocols, messages are treated as symbolic terms over an algebra rather than as bitstrings. This is typically not a free algebra -- there are equations that try to reflect the behaviour of the cryptographic operators. For example, dec(enc(x, pk), sk) = x is an equation that reflects that encrypting any message with a public key and decrypting using the coresponding secret key gives back the original message. Such (sets of) equations are called "intruder theories". It is typically the case that it makes sense to apply these equations in one direction only, so these are turned into rewrite rules or proof rules, and techniques from rewriting or proof normalization are used to study such intruder theories.
We present some interesting intruder theories and their analysis, and how it fits into the problem of verifying the security of protocols, with special attention to the XOR operation. This is joint work with R Ramanujam (Azim Premji University) and Vaishnavi Sundararajan (IIT Delhi).
In the first part of the talk, I will introduce certain algorithmic problems in group theory—namely, the Twisted Conjugacy Problem (TCP) and Orbit Decidability (OD)—which are closely related to the classical Conjugacy Problem (CP). I will then present some recent results addressing the CP in specific extensions of solvable Baumslag–Solitar (BS) groups, based on joint work with Mallika Roy and Enric Ventura.
In the second part, I will discuss some new algebraic and algorithmic results concerning fixed point subgroups of solvable BS groups. This part is based on ongoing joint work with Ramya Nair.