A Framework for Automatically Checking Anonymity with μCRL

DOI10.1007/978-3-540-75336-0_19zbMATH1211.94027OpenAlexW2155570147MaRDI QIDQ3608464FDOQ3608464

Authors Tom Chothia, Simona Orzan, Jun Pang, Mohammad Torabi Dashti

Publication date 5 March 2009

Published in Trustworthy Global Computing (Search for Journal in Brave)

Full work available at URL https://research.tue.nl/nl/publications/a-framework-for-automatically-checking-anonymity-with--crl(db543cae-acaf-4654-9356-0f0fee7bb59e).html

Mathematics Subject Classification ID

Cryptography (94A60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Automatic verification of anonymity of protocols
• scientific article; zbMATH DE number 2088318
• Evaluation of anonymity and confidentiality protocols using theorem proving
• scientific article; zbMATH DE number 2090930

Cites work

• scientific article; zbMATH DE number 1690175 (Why is no real title available?)
• scientific article; zbMATH DE number 1949618 (Why is no real title available?)
• scientific article; zbMATH DE number 1796138 (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?)
• A Framework for Automatically Checking Anonymity with μCRL
• A formalization of anonymity and onion routing
• A practical secret voting scheme for large scale elections
• Algebra of communicating processes with abstraction
• Algebraic process verification.
• Analysing the BKE-security protocol with \(\mu\)CRL
• Analysing the MUTE Anonymous File-Sharing System Using the Pi-Calculus
• CONCUR 2005 – Concurrency Theory
• CSP and anonymity
• Programming Languages and Systems
• The dining cryptographers problem: Unconditional sender and recipient untraceability
• Weak probabilistic anonymity
• mcmas: A Model Checker for Multi-agent Systems

Cited in

(9)

• Keeping secrets in resource aware components
• Probabilistic anonymity via coalgebraic simulations
• Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap
• Automated verification of equivalence properties of cryptographic protocols
• Symbolic model checking the knowledge in Herbivore protocol
• A Framework for Automatically Checking Anonymity with μCRL
• Formalizing provable anonymity in Isabelle/HOL
• CSP and anonymity
• Automatic verification of anonymity of protocols

This page was built for publication: A Framework for Automatically Checking Anonymity with μCRL

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