–
Room P3.10, Mathematics Building
Handling algebraic equations in the symbolic analysis of securityprotocols
Several security protocols make use of the algebraic properties of cryptographic operators, e.g. associativity of XOR or commutativity of exponents in modular exponentiation. Handling algebraic equations in the symbolic analysis of security protocols is however difficult as it requires extending the underlying unification algorithm as well as the protocol and intruder model. A number of approaches have been proposed, but they are complex and specialized to particular equational theories. In this talk, I will survey these approaches and present a general, uniform method to handle algebraic properties in symbolic protocol analysis, based on a restriction on the depth of message terms. As a case study, we have integrated our method into OFMC, a state-of-the-art protocol analysis tool based on symbolic techniques, thereby extending the scope of OFMC to encompass a large number of practically relevant protocols.