Formalization of provable anonymity in Isabelle

Yongjian Li

---

Case Studies

The Isabelle/HOL proof scripts in the papers are listed below:

o The general theory of provable anonymity library( thy files );

o The case study on the Crowds;

o The case study on Onion.

Some notes

• All the proof scripts have been checked in Isabelle2012.
• A paper has been prepared for submission: Formalizing Provable Anonymity in Isabelle/HOL

---

September 15, 2012