@article{LP15,
  author        = {Y. Li and J. Pang},
  title         = {Formalizing provable anonymity in {Isabelle/HOL}},
  journal       = {Formal Aspects of Computing},
  year          = {2015},
  volume        = {27},
  number        = {2},
  pages         = {255-282}
}