Reasoning about Algorithms
Reasoning about Algorithms, such as cryptographic protocols, is necessary to guarantee confidential and authenticated communication over a public network. Many proposed protocols have been found to contain deep and subtle flaws, and several formalisms proposed for reasoning about such protocols are likewise flawed. We focus on the question on how to make formal proofs easier to conduct, by enhancing tool support and devising novel proof tactics.
Contact Jeremy Jacob for more information.