Design and Verification of Anonymous Trust Protocols

  • Michael Backes
  • Matteo Maffei
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7028)


Over the last years, the Web has evolved into the premium forum for freely and anonymously disseminating and collecting information and opinions. However, the ability to anonymously exchange information, and hence the inability of users to identify the information providers and to determine their credibility, raises serious concerns about the reliability of exchanged information.

In this paper we propose a methodology for designing security protocols that enforce fine-grained trust policies while still ensuring the anonymity of the users. The fundamental idea of this methodology is to incorporate non-interactive zero-knowledge proofs: the trust level of users are certified using digital signatures, and users assert their trust level by proving in zero-knowledge the possession of such certificates. Since the proofs are zero-knowledge, they provably do not reveal any information about the users except for their trust levels; in particular, the proofs hide their identities.

We additionally propose a technique for verifying the security properties of these protocols in a fully automated manner. We specify protocols in the applied pi-calculus, formalize trust policies as authorization policies, and define anonymity properties in terms of observational equivalence relations. The verification of these properties is then conducted using an extension of recently proposed static analysis techniques for reasoning about symbolic abstractions of zero-knowledge proofs.


Security Protocol Trust Level Static Analysis Technique Authorization Policy 29th IEEE Symposium 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Lu, L., Han, J., Hu, L., Huai, J., Liu, Y., Ni, L.M.: Pseudo trust: Zero-knowledge based authentication in anonymous peer-to-peer protocols. In: Proc. 2007 IEEE International Parallel and Distributed Processing Symposium, p. 94. IEEE Computer Society Press (2007)Google Scholar
  2. 2.
    Goldreich, O., Micali, S., Wigderson, A.: Proofs that yield nothing but their validity or all languages in NP have zero-knowledge proof systems. Journal of the ACM 38(3), 690–728 (1991), MathSciNetCrossRefGoogle Scholar
  3. 3.
    Brickell, E., Camenisch, J., Chen, L.: Direct anonymous attestation. In: Proc. 11th ACM Conference on Computer and Communications Security, pp. 132–145. ACM Press (2004)Google Scholar
  4. 4.
    Juels, A., Catalano, D., Jakobsson, M.: Coercion-resistant electronic elections. In: Proc. 4th ACM Workshop on Privacy in the Electronic Society, WPES, pp. 61–70. ACM Press (2005)Google Scholar
  5. 5.
    Clarkson, M.R., Chong, S., Myers, A.C.: Civitas: A secure voting system. In: Proc. 29th IEEE Symposium on Security and Privacy, pp. 354–368. IEEE Computer Society Press (2008)Google Scholar
  6. 6.
    Abadi, M., Blanchet, B.: Secrecy Types for Asymmetric Communication. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 25–41. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Backes, M., Hriţcu, C., Maffei, M.: Type-checking zero-knowledge. In: 15th ACM Conference on Computer and Communications Security, CCS 2008, pp. 357–370. ACM Press (2008), Implementation available at
  8. 8.
    Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: Proc. 29th IEEE Symposium on Security and Privacy, pp. 202–215. IEEE Computer Society Press (2008)Google Scholar
  9. 9.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. 28th Symposium on Principles of Programming Languages, POPL, pp. 104–115. ACM Press (2001)Google Scholar
  10. 10.
    Abadi, M., Blanchet, B., Fournet, C.: Automated verification of selected equivalences for security protocols. In: Proc. 20th Annual IEEE Symposium on Logic in Computer Science, LICS, pp. 331–340. IEEE Computer Society Press (2005)Google Scholar
  11. 11.
    Jøsang, A.: An algebra for assessing trust in certification chains. In: Proceedings of the Network and Distributed Systems Security Symposium, NDSS 1999. The Internet Society (1999)Google Scholar
  12. 12.
    Xiong, L., Ling, L.: A reputation-based trust model for peer-to-peer ecommerce communities (extended abstract). In: Proceedings of the 4th ACM Conference on Electronic Commerce, EC 2003, pp. 228–229. ACM Press (2003)Google Scholar
  13. 13.
    Carbone, M., Nielsen, M., Sassone, V.: A formal model for trust in dynamic networks. In: International Conference on Software Engineering and Formal Methods, SEFM 2003, pp. 54–64 (2003)Google Scholar
  14. 14.
    Bangerter, E., Camenisch, J., Krenn, S., Sadeghi, A., Schneider, T.: Automatic generation of sound zero-knowledge protocols. IACR Cryptology ePrint Archive: Report 2008/471 (2008),

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Michael Backes
    • 1
    • 2
  • Matteo Maffei
    • 1
  1. 1.Saarland UniversitySaarbrückenGermany
  2. 2.Max Planck Institute for Software Systems (MPI-SWS)Germany

Personalised recommendations