Abstract
Below we present an information-theoretic method for proving the amount of information leaked by programs formalized using the HOL4 theorem-prover. The advantages of this approach are that the analysis is quantitative, and therefore capable of expressing partial leakage, and that proofs are performed using the HOL4 theorem-prover, and are therefore guaranteed to be logically and mathematically consistent with the formalization. The applicability of this methodology to proving privacy properties of Privacy Enhancing Technologies is demonstrated by proving the anonymity of the Dining Cryptographers protocol. To the best of the author’s knowledge, this is the first machine-verified proof of privacy of the Dining Cryptographers protocol for an unbounded number of participants and a quantitative metric for privacy.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bhargava, M., Palamidessi, C.: Probabilistic Anonymity, vol. 3653 (2005)
Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy, pp. 140–154 (May 2006)
Chatzikokolakis, K.: Probabilistic and Information-Theoretic Approaches to Anonymity. PhD thesis, Laboratoire d’Informatique (LIX), École Polytechnique, Paris (October 2007)
Chaum, D.: The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology 1(1), 65–75 (1988)
Clark, D., Hunt, S., Malacaria, P.: Quantitative analysis of the leakage of confidential data. Electr. Notes Theor. Comput. Sci. 59(3) (2001)
Clark, D., Hunt, S., Malacaria, P.: Quantitative information flow, relations and polymorphic types. J. Log. Comput. 15(2), 181–199 (2005)
Danezis, G., Dingledine, R., Mathewson, N.: Mixminion: design of a type III anonymous remailer protocol. pp. 2–15 (2003)
Deng, Y., Palamidessi, C., Pang, J.: Weak probabilistic anonymity. In: Proceedings of SECCO 2005. Electronic Notes in Theoretical Computer Science (2005)
Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976)
Denning, D.E.: Cryptography and Data Security. Addison-Wesley, Reading (1982)
Dewdney, A.K.: Computer recreations: Of worms, viruses, and core war. Scientific American, 110 (March 1989)
Díaz, C., Seys, S., Claessens, J., Preneel, B.: Towards Measuring Anonymity, vol. 2482 (2003)
Dingledine, R., Mathewson, N., Syverson, P.: Tor: The second-generation onion router. In: Proceedings of the 13th USENIX Security Symposium (August 2004)
Doob, J.L.: Measure Theory. Graduate Texts in Mathematics, vol. 143. Springer, Heidelberg (1991)
Goel, S., Robson, M., Polte, M., Sirer, E.G.: Herbivore: A Scalable and Efficient Protocol for Anonymous Communication. Technical Report 2003-1890, Cornell University, Ithaca, NY (February 2003)
Gordon, M.J.C.: From lcf to hol: a short history. In: Plotkin, G., Stirling, C.P., Tofte, M. (eds.) Proof, Language, and Interaction. MIT Press, Cambridge (2000)
Hasan, O., Tahar, S.: Verification of expectation properties for discrete random variables in hol. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 119–134. Springer, Heidelberg (2007)
Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge (2002)
Levine, B.N., Shields, C.: Hordes — A Multicast Based Protocol for Anonymity. Journal of Computer Security 10(3), 213–240 (2002)
Lowe, G.: Breaking and fixing the needham-schroder public-key protocol using fdr. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Malacaria, P.: Assessing security threats of looping constructs. In: POPL, pp. 225–235 (2007)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1-2), 85–128 (1998)
Reiter, M.K., Rubin, A.D.: Crowds: Anonymity for web transactions. Technical Report 97-15, DIMACS (1997)
Rennhard, M., Plattner, B.: Introducing MorphMix: Peer-to-Peer based Anonymous Internet Usage with Collusion Detection. In: Proceedings of the Workshop on Privacy in the Electronic Society (WPES 2002), Washington, DC, USA (November 2002)
Schneider, S., Sidiropoulos, A.: CSP and anonymity. In: Martella, G., Kurth, H., Montolivo, E., Bertino, E. (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 198–218. Springer, Heidelberg (1996)
Serjantov, A., Danezis, G.: Towards an information theoretic metric for anonymity. In: Dingledine, R., Syverson, P.F. (eds.) PET 2002. LNCS, vol. 2482. Springer, Heidelberg (2003)
Shannon, C.E.: A mathematical theory of communication. Bell System Technincal Journal (27), 379–423, 623–656 (1948)
Shmatikov, V.: Probabilistic model checking of an anonymity system. Schneider S.(ed.) Journal of Computer Security 12(3/4), 355–377 (2004)
Williams, D.: Probability with Martingales. Cambridge Mathematical Textbooks. Cambridge University Press, Cambridge (1991)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coble, A.R. (2008). Formalized Information-Theoretic Proofs of Privacy Using the HOL4 Theorem-Prover. In: Borisov, N., Goldberg, I. (eds) Privacy Enhancing Technologies. PETS 2008. Lecture Notes in Computer Science, vol 5134. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70630-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-70630-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70629-8
Online ISBN: 978-3-540-70630-4
eBook Packages: Computer ScienceComputer Science (R0)