Project Type
Poster
Publication Date
4-15-2022
Department or Program
Computer Science
College
College of Arts and Sciences
Faculty Mentor #1
Marshall, Andrew
Abstract
The primary motivator of this research is attempting to extend the ability of cryptographic protocol analysis tool and prove security questions about a wider set of cryptographic systems. Many systems already work for “subterm-convergent” presentations. Many also work for specific examples of protocols that are beyond subterm-convergent. However, there is no syntactic definition of this “beyond subterm” or no classification of what systems. The resulting question is: Can we define a new form of beyond subterm-convergent Term Rewrite System (TRS) and prove it can be used to extend the ability of existing cryptographic protocol analysis methods? We begin finding our solution by first using notions of graph theory develop a new definition of graph-embedded relation on terms. Then, we extend the graph embedded notion on terms to term-rewrite systems. Next, we prove that these new “graph-embedded TRS” encompass the required properties of the cryptographic analysis systems. Finally, we prove that the protocol analysis systems work on the classes of graph-embedded TRS, namely that they have the local stability property. As a result of this research, we have developed a new form of graph-embedded term rewrite system. Additionally, we have proven several properties such as termination and that they differ from homeomorphic embedded systems. These properties were then used to show how graph-embedded term rewrite systems can be used to analyze cryptographic protocols, for example, by using local stability. In future work, we would like to explore more applications for graph-embedded term rewrite systems, as well as investigating if additional embedding properties such as topological embeddings are useful.