Home Research Projects Teaching Events Contact

Andrew M. Marshall

Associate Professor of Computer Science
University of Mary Washington


Research Interests

  • Broad Interests: Computational Logic, Algebra in Computation, Automated Reasoning, Security.
  • Theoretical: Unification Theory, Combination Methods in Automated Reasoning, Term-Rewriting, Algebraic Complexity.
  • Applied: Formal Verification of Cryptographic Protocols and Algorithms, Software Verification, Automated Reasoning in Security.


Papers, Publications, and Other Research (ORCID, DBLP)


  • Unification modulo the theory of map
    (With Paliath Narendran and Bingqiao Zhou)
    Tech Report

Current Funded Research Project

Unification in Symbolic Methods for the Verification of Automatically Synthesized Cryptosystems


The objective of this project is to develop new symbolic analysis techniques that can be applied to the automated synthesis of cryptographic algorithms. Instead of focusing on specific problems and particular methods for those problems, we will focus on classes of problems and the symbolic methods themselves. We will be particularly interested in general techniques that can be applied to wide classes of problems, and thus will be of maximal usefulness.

Most of the symbolic characterizations are expressed in terms of the existence or non-existence of solutions to systems of equations. Thus, we intend to make unification, the process of finding solutions to systems of equations in a symbolic algebra, the main focus of our approach. However, the unification algorithms we develop may need to obey certain constraints. For example the solutions we construct may need to be computable by a probabilistic polynomial-time adversary without access to certain terms (e.g. some cryptographic keys), or a solution may require that certain terms not be identical, adding a disunification constraint, or an authentication algorithms may require that authentication checks (which usually involve checking an inequality) succeed for correctly authenticated data and fail for all other cases.

We expect to develop a collection of constrained unification problems of demonstrated relevance to deciding security of cryptographic algorithms, to advance the complexity analyses of the symbolic problems, and to develop implementations of the algorithms that will be made available to the research community.

Project Collaboratoring Institutions

Code Repo:

You can find the current public release of the tool code here: CryptoSolve

The UMW Team


  • University of Mary Washington
    • CPSC 110 - Introduction to Computer Science (Fall 2020, Spring 2021)
    • CPSC 326 - Theoretical Foundations of Computing (Fall 2016, Spring 2017, Fall 2017, Fall 2018, Spring 2019, Fall 2019, Fall 2021)
    • CPSC 340 - Data Structures and Algorithms (Spring 2016)
    • CPSC 405 - Operating Systems and Programming (Fall 2015, Fall 2016, Fall 2017, Spring 2018, Fall 2018, Fall 2021)
    • CPSC 414 - Network Principles and Applications (Spring 2015, Spring 2016, Spring 2017)
    • CPSC 220 – Comp Programming and Problem Solving (Fall 2014, Spring 2015)
    • CPSC 345 – Intro to Computer Security (Fall 2014, Fall 2015, Spring 2018, Spring 2019)
    • CPSC 435 - Advanced Cybersecurity (Spring 2021)
    • CPSC 445 - Software Security (Fall 2017, Fall 2018, Fall 2019)
  • University at Albany

New Programs at UMW:


Older Events: