  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.
