Evaluation of anonymity and confidentiality protocols using theorem proving

DOI10.1007/S10703-015-0232-5MaRDI QIDQ5962971zbMATH OpenOpenAlexFDO

Authors Tarek Mhamdi, Osman Hasan, Sofiène Tahar

Publication date 25 February 2016

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-015-0232-5

zbMATH Keywords

confidentialitytheorem provinginformation leakageanonymitydependable systems and software

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Information theory (general) (94A15) Network protocols (68M12)

Recommendations

• A formalization of anonymity and onion routing
• Formalizing provable anonymity in Isabelle/HOL
• Formal analysis of the information leakage of the DC-nets and crowds anonymity protocols
• Modular verification of protocol equivalence in the presence of randomness
• Analyzing anonymity attacks through noisy channels

Cites work

• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 107482 (Why is no real title available?)
• scientific article; zbMATH DE number 3542687 (Why is no real title available?)
• scientific article; zbMATH DE number 2090929 (Why is no real title available?)
• scientific article; zbMATH DE number 2090930 (Why is no real title available?)
• scientific article; zbMATH DE number 958048 (Why is no real title available?)
• A theory of type polymorphism in programming
• An introduction to mathematical logic and type theory: To truth through proof.
• Anonymity Protocols as Noisy Channels
• Assessing security threats of looping constructs
• Formalization of entropy measures in HOL
• On the Foundations of Quantitative Information Flow
• On the formalization of the Lebesgue integration theory in HOL

Cited in

(3)

• A Framework for Automatically Checking Anonymity with μCRL
• Formalization of normal random variables in HOL
• scientific article; zbMATH DE number 1113950 (Why is no real title available?)

Describes a project that uses

Uses Software

• GitHub
• ETPS
• HOL
• ML

This page was built for publication: Evaluation of anonymity and confidentiality protocols using theorem proving

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