Externally Verifiable Oblivious RAM. - Joshua Gancher; Adam Groce; Alex Ledger (Proc. Priv. Enhancing Technol., 2017)

Symbolic Proofs for Lattice-Based Cryptography. - Gilles Barthe; Xiong Fan; Joshua Gancher; Benjamin Grégoire; Charlie Jacomme; Elaine Shi (IACR Cryptol. ePrint Arch., 2018)

IPDL: A Probabilistic Dataflow Logic for Cryptography. - Xiong Fan; Joshua Gancher; Greg Morrisett; Elaine Shi; Kristina Sojakova (IACR Cryptol. ePrint Arch., 2019)

Viaduct: an extensible, optimizing compiler for secure distributed programs. - Cosku Acay; Rolph Recto; Joshua Gancher; Andrew C. Myers; Elaine Shi (PLDI, 2021)

Viaduct: An Extensible, Optimizing Compiler for Secure Distributed Programs (Technical Report). - Cosku Acay; Rolph Recto; Joshua Gancher; Andrew C. Myers; Elaine Shi (IACR Cryptol. ePrint Arch., 2021)

IPDL: A Simple Framework for Formally Verifying Distributed Cryptographic Protocols. - Greg Morrisett; Elaine Shi; Kristina Sojakova; Xiong Fan; Joshua Gancher (IACR Cryptol. ePrint Arch., 2021)

Equational Reasoning for Verified Cryptographic Security. - Joshua Gancher (2021)

WaveCert: Formal Compiler Validation for Asynchronous Dataflow Programs. - Zhengyao Lin; Joshua Gancher; Bryan Parno (CoRR, 2023)

Owl: Compositional Verification of Security Protocols via an Information-Flow Type System. - Joshua Gancher; Sydney Gibson; Pratap Singh; Samvid Dharanikota; Bryan Parno (IACR Cryptol. ePrint Arch., 2023)

A Core Calculus for Equational Proofs of Cryptographic Protocols. - Joshua Gancher; Kristina Sojakova; Xiong Fan; Elaine Shi; Greg Morrisett (Proc. ACM Program. Lang., 2023)

Secure Synthesis of Distributed Cryptographic Applications. - Cosku Acay; Joshua Gancher; Rolph Recto; Andrew C. Myers (CSF, 2024)

Secure Synthesis of Distributed Cryptographic Applications (Technical Report). - Cosku Acay; Joshua Gancher; Rolph Recto; Andrew C. Myers (CoRR, 2024)

FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions. - Zhengyao Lin; Joshua Gancher; Bryan Parno (Proc. ACM Program. Lang., 2024)

OwlC: Compiling Security Protocols to Verified, Secure, High-Performance Libraries. - Pratap Singh; Joshua Gancher; Bryan Parno (IACR Cryptol. ePrint Arch., 2025)

Concrete Security Bounds for Simulation-Based Proofs of Multi-Party Computation Protocols. - Kristina Sojakova; Mihai Codescu; Joshua Gancher (CoRR, 2025)