ABOUT THE PROJECT:
This project is investigating the existence of decision procedures for two key properties at the heart of observational equivalence, assuming the protocol's algebraic properties satisfy the finite variant property (FVP), which is satisfied by most cryptographic functions. If time permits, extensions relaxing FVP will be developed. The first such property is deducibility, that is, determining whether an attacker who has seen a sequence of messages can deduce a given message from that sequence. The second is static equivalence, that is, the ability to decide whether two sequences of messages seen by an attacker are equivalent, in the sense that there is nothing that the attacker can distinguish from one of them and not from the other. Static equivalence is key to proving observational equivalence and trace equivalence. The research is trying to develop and prove correct inference systems for these two decision procedures under the FVP assumption or some more general condition.