AttackerSynthesis

Tool (Korg), Models (TCP, etc.), and Documentation for Attacker Synthesis Project.

How to Read Docs

The documentation for this project consists of this README as well as all the files in docs/. They natively link to one another so that you can navigate without ever using the file system. These documents are written in Github Markdown and are best viewed online on Github pages, here. We use features of Github flavor Markdown such as emojis, automatic tables of contents, and HTML.

Repository Structure

This repository contains the tool Korg as well as various Promela models from our paper. The most important parts from the paper are marked with a :pushpin:.

:pushpin: The rest of the contents of the repository are exactly the code for the tool Korg.

How to run an example

From the top-level to run smallDemo1, run the command python3 Korg.py --name=smallDemo1 --dir='demo/smallDemo1/*'. The output of the demo will appear in out/smallDemo1. You can change what directory the results appear in by changing the name flag.

How to cite

In BibTeX:

@misc{hippel2020automated,
    title={Automated Attacker Synthesis for Distributed Protocols},
    author={Max von Hippel and Cole Vick and Stavros Tripakis and Cristina Nita-Rotaru},
    year={2020},
    eprint={2004.01220},
    archivePrefix={arXiv},
    primaryClass={cs.CR}
}

For more, view the article in Semantic Scholar.

ArXiV version with proofs.

Available here.

How to use the tool.

See docs/Korg.md.