Skip to main content
SpringerLink
Log in
Book cover

International Conference on the Theory and Application of Cryptology

ASIACRYPT 1991: Advances in Cryptology — ASIACRYPT '91 pp 412–426Cite as

Formal verification of probabilistic properties in cryptographic protocols

Extended abstract

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 739))

Abstract

We introduce an original method to verify probabilistic properties in cryptographic protocols. This method uses the representation of participants' knowledge that we presented at CRYPTO'91. The modelization is based on the assumption that the underlying cryptographic system is perfect and is an extension of the “Hidden Automorphism Model” introduced by Merritt.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Burrows, M. Abadi, and R. Needham. A Logic of Authentication. Technical Report 39, Digital — Systems Research Center (SRC), 1989.

    Google Scholar 

  2. P. Bieber. Aspects Epistémiques des Protocoles Cryptographiques. PhD thesis, Université Paul-Sabatier de Toulouse (Sciences), October 1989.

    Google Scholar 

  3. M. Blum and S. Micali. How to Generate Cryptographically Strong Sequences of Pseudo-Random Bits. SIAM Journal on Computing, 13(4):850–864, 1984.

    Article  Google Scholar 

  4. R. Berger, R. Peralta, and T. Tedrick. A Provably Secure Oblivious Transfer Protocol. In T. Beth, N. Cot, and I. Ingemarsson, editors, Lecture Notes in Computer Science. Advances in Cryptology, Proceedings of EUROCRYPT'84 #209, pages 379–386. Springer-Verlag, 1985.

    Google Scholar 

  5. S. Goldwasser, S. Micali, and C. Rackoff. The Knowledge Complexity of Interactive Proof-Systems. SIAM Journal on Computing, 18(1):186–208, 1989.

    Article  Google Scholar 

  6. L. Gong, R. Needham, and R. Yahalom. Reasoning about Belief in Cryptographic Protocols. In Proceedings of the 1990 IEEE Computer Society Symposium on Research in Security and Privacy, pages 234–248. IEEE Computer Society Press, 1990.

    Google Scholar 

  7. R. A. Kemmerer. Analyzing Encryption Protocols Using Formal Verification Techniques. IEEE Journal on Selected Areas in Communications, 7(4):448–457, 1989.

    Article  Google Scholar 

  8. J. K. Millen, S. C. Clark, and S. B. Freedman. The Interrogator: Protocol Security Analysis. IEEE Transactions on Software Engineering, 13(2):274–288, 1987.

    Google Scholar 

  9. C. Meadows. Representing Partial Knowledge in an Algebraic Security Model. In Proceedings of the Computer Security Foundations Workshop III, pages 23–31. IEEE Computer Society Press, 1990.

    Google Scholar 

  10. M. J. Merritt. Cryptographic Protocols. PhD thesis, Georgia Institute of Technology 1983.

    Google Scholar 

  11. M. Merritt and P. Wolper. States of Knowledge in Cryptographic Protocols (extended abstract). Unpublished Manuscript, 1985.

    Google Scholar 

  12. P. Syverson. The Use of Logic in the Analysis of Cryptographic Protocols. In Proceedings of the 1991 IEEE Symposium on Research in Security and Privacy, pages 156–170. IEEE Computer Society Press, 1991.

    Google Scholar 

  13. A. Thayse, P. Gribomont, G. Hulin, A. Pirotte, D. Roelants, D. Snyers, M. Vauclair, P. Gochet, P. Wolper, E. Grégoire, and P. Delsarte. Approche logique de l'intelligence artificielle — 2. De la logique modale à la logique des bases de données. Dunod, Bordas, Paris, 1989.

    Google Scholar 

  14. M-J. Toussaint. Reasoning about Probabilistic Properties of Cryptographic Protocols (extended abstract). Abstract of the talk at the F.N.R.S. day on Computer Security, May 1989.

    Google Scholar 

  15. M-J. Toussaint. Deriving the Complete Knowledge of Participants in Cryptographic Protocols (Extended Abstract). in the proceedings of CRYPTO'91, August. 1991.

    Google Scholar 

  16. M.-J. Toussaint. Verification of Cryptographic Protocols. PhD thesis, Université de Liège (Belgium), 1991.

    Google Scholar 

  17. M-J. Toussaint and P. Wolper. Reasoning about Cryptographic Protocols (Extended Abstract). In Joan Feigenbaum and Michael Merritt, editors, Distributed Computing and Cryptography (October 1989), pages 245–262. DIMACS — Series in Discrete Mathematics and Theoretical Computer Science (AMS — ACM), 1991. Volume 2.

    Google Scholar 

  18. V. Varadharajan. Verification of Network Security Protocols. Computers & Security, 8(8):693–708, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut Montefiore, Université de Liège, B28, Sart Tilman, B 4000, Liège, Belgium

    Marie-Jeanne Toussaint

Authors
  1. Marie-Jeanne Toussaint
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Hideki Imai Ronald L. Rivest Tsutomu Matsumoto

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Toussaint, MJ. (1993). Formal verification of probabilistic properties in cryptographic protocols. In: Imai, H., Rivest, R.L., Matsumoto, T. (eds) Advances in Cryptology — ASIACRYPT '91. ASIACRYPT 1991. Lecture Notes in Computer Science, vol 739. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57332-1_35

Download citation

  • DOI: https://doi.org/10.1007/3-540-57332-1_35

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57332-6

  • Online ISBN: 978-3-540-48066-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation