A model-based approach to analysis of authentication protocols

  • Janusz Górski
  • Marcin Olszewski
Conference paper


The paper presents the OF-APSAF integrated framework for authention protocol analysis. The framework is built on top of a well-established formal method CSP and its supporting tools: Casper and FDR. The integral part of OF-APSAF is the object-oriented semi-formal approach to modelling of cryptographic protocols, their application context and security requirements. The modelling is based on UML and a catalogue of specialised analytical patterns. Object-orientation helps to cope with the complexity inherent to the domain of security protocols verification and formal methods in general.


security protocols formal methods object-oriented modelling 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

7 References

  1. [1]
    Burrows M., Abadi M. 1989. ‘A logic of authentication'. Technical Report 39, Digital Systems Research Center.Google Scholar
  2. [2]
    Roscoe A.W. 1998. ‘The Theory and Practice of Concurrency'. Prentice-Hall, International Series in Computer Science, ISBN 0-13-674409-5.Google Scholar
  3. [3]
    Ryan P.Y.A, Schneider S.A., Goldsmith M.H., Lowe G., Roscoe A.W. 2001. ‘The Modelling and Analysis of Security Protocols: the CSP Approach'. Addison-Wesley, ISBN 0-201-67471-8.Google Scholar
  4. [4]
    Lowe G. 1998, ‘Casper: A Compiler for the Analysis of Security Protocols'. Journal of Computer Security, Volume 6, pp. 53–84.Google Scholar
  5. [5]
    Object Management Group 2000. ‘OMG Unified Modelling Language Specification ver. 1.3’Google Scholar
  6. [6]
    Simoes P., Alves P., Rogado J., Ferreira P. 2000. ‘An Authentication Protocol for Mobile Devices'. Advance Program for International Workshop on Internet 2000.Google Scholar
  7. [7]
    Yamaguchi S., Okayama K., Miyahara H. 1991. ‘The design and implementation of an authentication system for the wide area distributed environment'. IEICE Transactions on Information and Systems. E74(11):3902–3909.Google Scholar
  8. [8]
    Hwang T., Yung-Hsiang Chen 1995. ‘On the security of splice/as: The authentication system in wide internet'. Information Processing Letters 53:97–101.CrossRefGoogle Scholar
  9. [9]
    Górski J., Jarzębowicz A., Leszczyna R., Miler J., Olszewski M. 2003. ‘An Approach to Trust Case Development'. Lecture Notes in Computer Science 2788. Springer-Verlag. pp. 193–206.Google Scholar
  10. [10], IST-DRIVE project's official website.Google Scholar

Copyright information

© Springer Science+Business Media, Inc. 2005

Authors and Affiliations

  • Janusz Górski
    • 1
  • Marcin Olszewski
    • 1
  1. 1.Gdańsk University of TechnologyGdańskPoland

Personalised recommendations