Probabilistic annotations for protocol models. Dedicated to Joshua Guttman

DOI10.1007/978-3-030-91631-2_18MaRDI QIDQ2154019zbMATH OpenOpenAlexFDO

Authors Dusko Pavlovic

Publication date 13 July 2022

Full work available at URL https://arxiv.org/abs/2108.03901

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer security (68M25) Cryptography (94A60)

Abstract: 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.

Recommendations

• Automata, Languages and Programming
• A logical approach to multilevel security of probabilistic systems
• scientific article; zbMATH DE number 4191559
• On quantitative analysis of probabilistic protocols
• scientific article; zbMATH DE number 1692932

Cites work

• EasyCrypt: a tutorial
• How probabilities came to be objective and subjective
• On the security of public key protocols
• State and progress in strand spaces: proving fair exchange

Cited in

(8)

• Formalizing and analyzing security ceremonies with heterogeneous devices in ANP and PDL
• Exogenous probabilistic computation tree logic
• Probabilistic relational Hoare logics for computer-aided security proofs
• Elementary probability theory in the Eindhoven style
• scientific article; zbMATH DE number 4191559 (Why is no real title available?)
• A logical approach to multilevel security of probabilistic systems
• A quantitative doxastic logic for probabilistic processes and applications to information-hiding
• Automata, Languages and Programming

This page was built for publication: Probabilistic annotations for protocol models. Dedicated to Joshua Guttman

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2154019)