diff options
| author | Florian Dold <florian.dold@gmail.com> | 2018-09-30 17:55:08 +0200 |
|---|---|---|
| committer | Florian Dold <florian.dold@gmail.com> | 2018-09-30 17:55:08 +0200 |
| commit | e8fb73afda059976c0bc3199452b1dcb2e017f68 (patch) | |
| tree | 2d3463c00d967566ab9ff6c653b73b2a3e3c0be7 /conclusions.tex | |
| parent | 82ef4f5dccffa4c51c4ae35ef032a1c0ca030503 (diff) | |
| download | dold-thesis-phd-e8fb73afda059976c0bc3199452b1dcb2e017f68.tar.gz dold-thesis-phd-e8fb73afda059976c0bc3199452b1dcb2e017f68.tar.bz2 dold-thesis-phd-e8fb73afda059976c0bc3199452b1dcb2e017f68.zip | |
sync
Diffstat (limited to 'conclusions.tex')
| -rw-r--r-- | conclusions.tex | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/conclusions.tex b/conclusions.tex index aaf506c..18ef14f 100644 --- a/conclusions.tex +++ b/conclusions.tex @@ -48,7 +48,10 @@ challenge of allocating the total available balance to individual devices in a way that fits the customer's spending pattern, and only require synchronous communication at fixed intervals or when really necessary to re-allocate coins. -\subsection*{Formal Verification of Proofs} +% FIXME: reference PIR literature? + + +\subsection*{Machine-Verified Proofs} We currently model only a subset of the GNU Taler protocol formally, and proofs are handwritten and verified by humans. A tool such as CryptoVerif \cite{blanchet2007cryptoverif} can allow a higher coverage and computer-checked |