Advertisement

Prolog-Based Formal Reasoning for Security Protocols

  • Rongrong Jiang
  • Chuanbin Wang
  • Jiejie Xu
  • Jiangfen Yu
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 137)

Abstract

This paper introduces a security reachability analysis model based on the strand space theory and the constraint elimination method. A prolog-based automatic reasoning scheme is then proposed. At last, the reasoning implementation utilizing the Java interface of XSB (a prolog interpreter ) is described.

Keywords

Formal method Security protocols Prolog Automatic reasoning 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Burrows, M., Abadi, M., Needham, R.: A logic of authentication. Proceedings of the Royal Society of London A 426, 233–271 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Qin, S.: Twenty years development of security protocols research. Journal of Software 14(10), 2036–2044 (2003)Google Scholar
  3. 3.
    Fábrega, F., Herzog, J., Guttman, J.: Strand spaces: Proving security protocols correct. Journal of Computer Security 7(2,3), 191–230 (1999)CrossRefGoogle Scholar
  4. 4.
    Jonathan, M., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: 8th ACM Conference on Computer and Communications Security, pp. 166–175. ACM Press, Philadelphia (2001)Google Scholar
  5. 5.
    Amadio, R.M., Vincent, V., et al.: On the symbolic reduction of processes with cry-ptographic functions. Theory of Computer Science 290(1), 695–740 (2003)CrossRefzbMATHGoogle Scholar
  6. 6.
    Chen, T., Cai, J.: Research on visual analysis and design of security protocols. Journal of Communication and Computer 2(12), 27–31 (2005)MathSciNetGoogle Scholar
  7. 7.
    Amadio, R.M., Lugiez, D.: On the reachability problem in cryptographic protocols. In: Proceedings of the 11th International Conference, August 2000. Springer, Heidelberg (2000)Google Scholar
  8. 8.
    Lowe, G.: Breaking and Fixing the Needham-Sc-hroeder Public-Key Protocol Using FDR. In: Proceedings of the Second International Workshop, March 1996. Springer, Heidelberg (1996)Google Scholar
  9. 9.
    Song, D.X.: A New Efficient Automatic Checker for Security Protocol Analysis. In: IEEE Computer Security Foundations Workshop 1999. IEEE Computer Society, Los Alamitos (1999)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Rongrong Jiang
    • 1
    • 2
  • Chuanbin Wang
    • 2
  • Jiejie Xu
    • 2
  • Jiangfen Yu
    • 1
  1. 1.College of Inforamtion and EngineeringZhejiang Radio & Television UniversityHangzhouChina
  2. 2.Zhejiang Key Laboratory of Inforamtion SecurityHangzhouChina

Personalised recommendations