Mathematical Foundations and Analysis Techniques for Protocol Indistinguishability

Investigator: José Meseguer

This project proposes to make advances in protocol indistinguishability research by accomplishing the following main research goals:

1.  Develop the mathematical foundations of indistinguishability in the Doleve-Yao model modulo algebraic properties.

2. Develop formal verification techniques to automate proofs of indistinguishability properties.

3. Demonstrate the usefulness of such proof techniques on a wide range of protocols, including various kinds of privacy-preserving protocols.

4. Develop substantial case studies which further validate these advances and help in transmitting them to the research community.

Hard Problem Addressed


  1. Santiago Escobar, Catherine Meadows, José Meseguer and Sonia Santiago, “Sequential Protocol Composition in Maude-NPA”, 15th European Conference on Research in Computer Security (ESORICS 2010), Athens, Greece, September 20-22, 2010. [full text]
  2. Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, José Meseguer, Paliath Narendran, Sonia Santiago and Ralf Sasse, “Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis”, 24th International Conference on Automated Deduction (CADE 2013), Lake Placid, NY, June 9-14, 2013. [full text]
  3. Santiago Escobar, Catherine Meadows, José Meseguer and Sonia Santiago, “A Rewriting-based Forward Semantics for Maude-NPA”, Symposium and Bootcamp on the Science of Security (HotSoS 2014), Raleigh, NC, April 8-9 2014.  [full text]
  4. Fan Yang, Santiago Escobar, Catherine Meadows, José Meseguer, Paliath Narendran, “Theories for Homomorphic Encryption, Unification and the Finite Variant Property”, 16th International Symposium on Principles and Practice of Declarative Programming (PPDP 2014), Canterbury, United Kingdom, September 8-10, 2014. [full text]
  5. Sonia Santiago, Santiago Escobar, Catherine Meadows, and José Meseguer, “A Formal Definition of Protocol Indistinguishability and its Verification Using Maude-NPA”, 10th International Workshop on Security and Trust Management (STM 2014), Wroclaw, Poland, September 10-11, 2014. [full text]