Computer scientist and software engineer specializing in formal modeling and reasoning. Recent work focuses on formal proofs of security and correctness for cryptographic constructions.
K. Ye, M. Green, N. Sanguansin, L. Beringer, A. Petcher, and A. Appel. Verified Correctness and Security of mbedTLS HMAC-DRBG. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, November 2017. [ pdf ]
L. Beringer, A. Petcher, K. Ye, and A. Appel. Verified Correctness and Security of OpenSSL HMAC. In 24th USENIX Security Symposium, August 2015. [ pdf ]
A. Petcher and G. Morrisett. A Mechanized Proof of Security for Searchable Symmetric Encryption. In 28th IEEE Computer Security Foundations Symposium (CSF), July 2015. [ pdf ]
A. Petcher and G. Morrisett. The Foundational Cryptography Framework. In 4th International Conference on Principles of Security and Trust (POST), April 2015. [ pdf ]
A. Petcher. A Foundational Proof Framework for Cryptography. Ph.D. Thesis, Harvard University. April 2015. [ pdf ]
A. Petcher and A. Stump. Deciding Joinability Modulo Ground Equations in Operational Type Theory. In Proof Search in Type Theories (PSTT), August 2009. [ pdf ]
A. Stump, M. Deters, A. Petcher, T. Schiller, and T. Simpson. Verified Programming in Guru. In Programming Languages meets Program Verification (PLPV), January 2009. [ pdf ]
A. Petcher. Deciding Joinability Modulo Ground Equations in Operational Type Theory. M.S. Thesis, Washington University in Saint Louis, May 2008. [ pdf ]
A Coq library for modeling and reasoning about cryptographic constructions in the computational model.