README.md

# PKCS\#11SIV

My bachelor thesis, entitled ***To wrap it up:*** *A formally verified proposal for the use of
authenticated wrapping mechanisms in PKCS#11*.

It consists of
+ the thesis itself, [main.pdf](main.pdf)
+ [Tamarin](https://tamarin-prover.github.io/) models of the [PKCS\#11](https://www.oasis-open.org/committees/tc_home.php?wg_abbrev=pkcs11) API
  + a model using initialization vector-based [authenticated encryption](http://dx.doi.org/10.1145/586110.586125) schemes, [Model/gcm.spthy](Model/gcm.spthy)
  + a model using [synthetic initialization vector](http://web.cs.ucdavis.edu/~rogaway/papers/keywrap.html)-based schemes, [Model/siv.spthy](Model/siv.spthy)
  + an oracle needed for the automated proof of both models, [Model/oracle](Model/oracle)
+ [Pygments](https://pygments.org) extensions for source code highlighting
  + a lexer for the `spthy` format, [Pygments/spthy.py](Pygments/spthy.py)
  + a style tailored to fit the lexers output, [Pygments/spathi.py](Pygments/spathi.py)

## License
ISC-style license, see [LICENSE](LICENSE) for details.
Of course the license applies to my work, not to the work of others I used.
The excellent Masters/Doctoral thesis template, [main.tex](main.tex) and [MastersDoctoralThesisSplitTitle.cls](MastersDoctoralThesisSplitTitle.cls) which I adjusted slightly are a good example.

## Description
A symbolic model of a *Security API* supporting symmetric encryption and wrapping of keys.
Thought as a proposal for *PKCS\#11 v3.00*.
Automated proofs of security properties using Tamarin, a protocol verification tool.

## Initial setup
+ `git clone` the repository
+ `./init.sh` to prepare Makefiles

## Compiling the thesis
Prerequisites:
+ pdfLaTeX and latexmk
+ [Pygments](https://pygments.org)
  + affects code listings and inline code in `*.tex`
+ [Biber](http://biblatex-biber.sourceforge.net/)

Invoke `gmake`

## Using the models with Makefile
Prerequisites:
+ [Tamarin](https://tamarin-prover.github.io/)
+ adjusted [Model/Makefile](Model/Makefile) and [Model/Makefile.include](Model/Makefile.include)
+ current working directory is `Model`

+ open current model in interactive mode: `gmake`
+ automated proof of current model: `gmake proof`
+ well-formedness check of current model: `gmake check`
+ create a model from its components: e.g. `gmake gcm.spthy`
  + more or less concatenates the components
  + in most cases it will be easier to modify the models and not their components

## Using the models without Makefile
Prerequisites:
+ [Tamarin](https://tamarin-prover.github.io/)
+ current working directory is [Model](Model)

use `tamarin-prover --heuristic=O`, add parameters and model as needed

## Overview of the repository

+ [Chapters](Chapters): main chapters of the thesis
  + [motivation.tex](Chapters/motivation.tex): Introduction
  + [outline.tex](Chapters/outline.tex): Outline
  + [pkcs.tex](Chapters/pkcs.tex): PKCS\#11
  + [analysis.tex](Chapters/analysis.tex): Symbolic Analysis
  + [theory.tex](Chapters/theory.tex): Underlying Theory
  + [model.tex](Chapters/model.tex): Tamarin Model
  + [results.tex](Chapters/results.tex): Results
+ [Appendices](Appendices): appendix chapters of the thesis
  + [code.tex](Appendices/code.tex): code listings
  + [siv.tex](Appendices/siv.tex): SIV mode construction
+ [Figures](Figures): picture input, postscript at the moment
+ [Tikz](Tikz): graphics for the thesis
+ [Tables](Tables): tables for the thesis
+ [Presentation](Presentation): slides of the bachelor talk
+ [Model](Model): tamarin models
+ [Pygments](Pygments): classes needed for Pygments (used by minted)
+ [\_minted-main](_minted-main): precompiled minted files