Formal Specification and Verification of Mobile Agent Data Integrity Properties: A Case Study

  • Xavier Hannotin
  • Paolo Maggi
  • Riccardo Sisto
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2240)


The aim of the work presented in this paper is to check cryptographic protocols for mobile agents against both network intruders and malicious hosts using formal methods. We focus attention on data integrity properties and show how the techniques used for classical message-based protocols such as authentication protocols can be applied to mobile agent systems as well. To illustrate our approach, we use a case study taken from the literature and show how it can be specified and verified using some currently available tools.


Model Check Mobile Agent Authentication Protocol Security Property Cryptographic Protocol 
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.
    Tschudin, C.: Mobile agent security. In Klusch, M., ed.: Intelligent Information Agents: Cooperative, Rational and Adaptive Information Gathering on the Internet. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany (1999) 431–446Google Scholar
  2. 2.
    Farmer, W., Guttman, J., Swarup, V.: Security for mobile agents: Issues and requirements. In: Proceedings of the 19th National Information Systems Security Conference, Baltimore, Md. (1996) 591–597Google Scholar
  3. 3.
    Yee, B.S.: A sanctuary for mobile agents. Technical Report CS97-537, UC San Diego, Department of Computer Science and Engineering (1997)Google Scholar
  4. 4.
    Vigna, G.: Cryptographic traces for mobile agents. In Vigna, G., ed.: Mobile Agent Security. Lecture Notes in Computer Science No. 1419. Springer-Verlag: Heidelberg, Germany (1998) 137–153CrossRefGoogle Scholar
  5. 5.
    Karjoth, G., Asokan, N., Gülcü, C.: Protecting the computation results of freeroaming agents. In Rothermel, K., Hohl, F., eds.: Proceedings of the 2nd International Workshop on Mobile Agents. Volume 1477 of Lecture Notes in Computer Science., Springer-Verlag: Heidelberg, Germany (1998) 195–207CrossRefGoogle Scholar
  6. 6.
    Corradi, A., Montanari, R., Stefanelli, C.: Mobile agents integrity in E-commerce applications. In: of the 19th IEEE International Conference on Distributed Computing Systems Workshop (ICDCS’99), Austin, Texas, IEEE Computer Society Press (1999) 59–64Google Scholar
  7. 7.
    Wang, X.F., Yi, X., Lam, K.Y., Okamoto, E.: Secure information gathering agent for internet trading. In Zhang, C., Lukose, D., eds.: Proceedings of the 4th Australian Workshop on Distributed Artificial Intelligence on Multi-Agent Systems: Theories, Languages, and Applications (DAI-98). Volume 1544 of LNAI., Berlin, Germany, Springer (1998) 183–193Google Scholar
  8. 8.
    Hoare, C.A.R.: Communications Sequential Processes. Prentice-Hall, Englewood Cliffs (NJ), USA (1985)Google Scholar
  9. 9.
    Ltd., F.S.E.: Failures-Divergence Refinement. FDR2 User Manual. Available at (3 May 2000)
  10. 10.
    Lowe, G.: Casper: A compiler for the analysis of security protocols. In: PCSFW: Proceedings of The 10th Computer Security Foundations Workshop, IEEE Computer Society Press (1997)Google Scholar
  11. 11.
    Lowe, G., Roscoe, B.: Using CSP to detect errors in the TMN protocol. IEEE Transactions on Software Engineering 23 (1997) 659–669CrossRefGoogle Scholar
  12. 12.
    Schneider, S.: Verifying authentication protocols with CSP. In: PCSFW: Proceedings of The 10th Computer Security Foundations Workshop, IEEE Computer Society Press (1997)Google Scholar
  13. 13.
    Roscoe, A.W.: Modelling and verifying key-exchange protocols using CSP and FDR. In: Proceedings of the Eighth Computer Security Foundations Workshop (CSFW’ 95), Washington-Brussels-Tokyo, IEEE (1995) 98–107Google Scholar
  14. 14.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spicalculus. Research Report 149, Digital Equipment Corporation Systems Research Center (1998) A shortened version of this report appeared in Information and Computation 148(1999):1–70.MathSciNetGoogle Scholar
  15. 15.
    Clarke, E.M., Jha, S., Marrero, W.: Verifying security protocols with Brutus. ACM Transactions on Software Engineering and Methodology 9 (2000) 443–487CrossRefGoogle Scholar
  16. 16.
    Song, D.: Athena: A new efficient automatic checker for security protocol analysis. In: Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW’ 99), Washington-Brussels-Tokyo, IEEE (1999) 192–202Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Xavier Hannotin
    • 1
  • Paolo Maggi
    • 1
  • Riccardo Sisto
    • 1
  1. 1.Dip. di Automatica e InformaticaPolitecnico di TorinoTorinoITALY

Personalised recommendations