synchronous/korg-paper
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

removed duplicate text

Browse Source
This commit is contained in:
Cristina Nita-Rotaru
2024-12-04 12:43:17 -05:00
parent 44df855bf8
commit 816a496de9
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
sections/proofs.tex
View File

@@ -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. \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. %the model checker \korg is implemented on top of.
\begin{definition}[\ba] \begin{definition}[\ba]