# Manual

Use

``tamarin-prover  --heuristic=O    --prove  --oraclename=gcm.spthy.oracle gcm.spthy``

and

``tamarin-prover  --heuristic=O    --prove  --oraclename=siv.spthy.oracle siv.spthy``

to recompute the proofs. Note that gcm.spthy.oracle and siv.spthy.oracle are
identical.
>tested in tamarin-prover version 1.5.1

___________


This directory contains the tamarin files for the paper "How to wrap it up - A formally verified proposal for the use of authenticated wrapping in PKCS#11" presented at CSF 2019.
