Encoding First Order Proofs in SAT. - Todd Deshane; Wenjin Hu; Patty Jablonski; Hai Lin 005; Christopher Lynch; Ralph Eric McGregor (CADE, 2007)

Protocol Verification Via Rigid/Flexible Resolution. - Stéphanie Delaune; Hai Lin 005; Christopher Lynch (LPAR, 2007)

Encoding First Order Proofs in SMT. - Jeremy Bongio; Cyrus Katrak; Hai Lin 005; Christopher Lynch; Ralph Eric McGregor (SMT@CAV, 2007)

Unification modulo Homomorphic Encryption is Decidable. - Siva Anantharaman; Hai Lin 005; Christopher Lynch; Paliath Narendran; Michaël Rusinowitch (UNIF, 2008)

Cap unification: application to protocol security modulo homomorphic encryption. - Siva Anantharaman; Hai Lin 005; Christopher Lynch; Paliath Narendran; Michaël Rusinowitch (AsiaCCS, 2010)

Unification Modulo Homomorphic Encryption. - Siva Anantharaman; Hai Lin 005; Christopher Lynch; Paliath Narendran; Michaël Rusinowitch (J. Autom. Reason., 2012)

Local XOR Unification: Definitions, Algorithms and Application to Cryptography. - Hai Lin 005; Christopher Lynch (IACR Cryptol. ePrint Arch., 2020)

Formal Analysis of Symbolic Authenticity. - Hai Lin 005; Christopher Lynch (FroCoS, 2021)

Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems. - Hai Lin 005; Christopher Lynch; Andrew M. Marshall; Catherine A. Meadows; Paliath Narendran; Veena Ravishankar; Brandon Rozek (FroCoS, 2021)

CryptoSolve: Towards a Tool for the Symbolic Analysis of Cryptographic Algorithms. - Dalton Chichester; Wei Du; Raymond Kauffman; Hai Lin 005; Christopher Lynch; Andrew M. Marshall; Catherine A. Meadows; Paliath Narendran; Veena Ravishankar; Luis Rovira; Brandon Rozek (GandALF, 2022)