From 816a496de90ace8716e5b96baf182a26889ad024 Mon Sep 17 00:00:00 2001 From: Cristina Nita-Rotaru Date: Wed, 4 Dec 2024 12:43:17 -0500 Subject: [PATCH] removed duplicate text --- sections/proofs.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sections/proofs.tex b/sections/proofs.tex index 185b733..fcc13e1 100644 --- a/sections/proofs.tex +++ b/sections/proofs.tex @@ -1,6 +1,6 @@ \korg is an implementation of the theoretical attack synthesis framework proposed by \cite{Hippel2022_anonym}. This framework enjoys soundness and completeness guarantees for attacks discovered; that is, if there exists an attack, it is discovered, and if an attack is discovered, it is valid. However, the attack synthesis framework proposed by \cite{Hippel2022_anonym} reasons about an abstracted, theoretical process construct. Therefore, in order to correctly claim \korg is also sound and complete, it is necessary to demonstrate discovering an attack within the theoretical framework reduces to the semantics of \spin, the model checker \korg is built on top of. -There exists a semantic gap between the theoretical attack synthesis framework proposed by \cite{Hippel2022_anonym}, and the semantics of \korg. Therefore, in order to correctly claim \korg maintains the soundness and completeness of the theoretical framework it implements, it suffices to demonstrate finding an attack within the theoretical attack synthesis framework precisely reduces to the semantics of \spin. +%There exists a semantic gap between the theoretical attack synthesis framework proposed by \cite{Hippel2022_anonym}, and the semantics of \korg. Therefore, in order to correctly claim \korg maintains the soundness and completeness of the theoretical framework it implements, it suffices to demonstrate finding an attack within the theoretical attack synthesis framework precisely reduces to the semantics of \spin. %the model checker \korg is implemented on top of. \begin{definition}[\ba]