Probabilistic annotations for protocol models
This work addresses security verification for cryptosystems and puzzles, but it is incremental as it applies an existing logic framework to new examples.
The paper tackles the problem of reasoning about security by applying a probabilistic Hoare logic with localities to analyze cryptosystems and puzzles, proving and disproving specific security properties as a proof-of-concept.
We describe how a probabilistic Hoare logic with localities can be used for reasoning about security. As a proof-of-concept, we analyze Vernam and El-Gamal cryptosystems, prove the security properties that they do satisfy and disprove those that they do not. We also consider a version of the Muddy Children puzzle, where children's trust and noise are taken into account.