Verification of S&D Solutions for Network Communications and Devices

  • Carsten Rudolph
  • Luca Compagna
  • Roberto Carbone
  • Antonio Muñoz
  • Jürgen Repp
Part of the Advances in Information Security book series (ADIS, volume 45)


This chapter describes the tool-supported verification of S&D Solutions on the level of network communications and devices. First, the general goals and challenges of verification in the context of AmI systems are highlighted and the role of verification and validation within the SERENITY processes is explained.Then, SERENITY extensions to the SH VErification tool are explained using small examples. Finally, the applicability of existing verification tools is discussed in the context of the AVISPA toolset. The two different tools show that for the security analysis of network and devices S&D Patterns relevant complementary approachesexist and can be used.


State Component Security Protocol Transition Pattern Serenity Process Trusted Platform Module 
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.
    Armando A, Basin D, Boichut Y, Chevalier Y, Compagna L, Cuellar J, Drielsma PH, Heám P, Kouchnarenko O, Mantovani J, Mödersheim S, von Oheimb D, Rusinowitch M, Santiago J, Turuani M, Viganò L, Vigneron L (2005) The Avispa tool for the automated validation of internet security protocols and applications. In: Proceedings of CAV 2005, Computer Aided Verification, Springer Verlag, Lecture Notes in Computer Science, vol 3576Google Scholar
  2. 2.
    Armando A, Carbone R, Compagna L (2007) LTL Model Checking for Security Protocols. In: Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF20), July 6–8, 2007, Venice, Italy, Springer Verlag, LNCSGoogle Scholar
  3. 3.
    Armando A, Carbone R, Compagna L, Cuellar J, Tobarra L (2008) Formal analysis of saml 2.0 web browser single sign-on: Breaking the saml-based single sign-on for google apps. In: Proceedings of FMSE 2008, Formal Methods in Security Engineering, ACMGoogle Scholar
  4. 4.
    AVANTSSAR (2008) The AVANTSSAR Project.
  5. 5.
    AVISPA (2007) The AVISPA Project.
  6. 6.
    Bella G, Paulson L (2001) Mechanical proofs about a non-repudiation protocol. In: Proceedings of 14th International Conference on Theorem Proving in Higher Order Logic, Springer Verlag, Lecture Notes in Computer Science, vol 2152, pp 91–104Google Scholar
  7. 7.
    Bellare M, Desai A, Pointcheval D, Rogaway P (1998) Relations among notions of security for public-key encryption schemes. In: Krawczyk H (ed) Advances in Cryptology – Crypto 98, Springer Verlag, Lecture Notes in Computer Science, pp 26–45Google Scholar
  8. 8.
    Blanchet B (2001) An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14), IEEE Computer Society, Cape Breton, Nova Scotia, Canada, pp 82–96Google Scholar
  9. 9.
    Bundesamt für Sicherheit in der Informationstechnik (BSI) (2008) Itgrundschutz-kataloge. URL:
  10. 10.
    Cervesato I, Jaggard AD, Scedrov A, Tsay JK, Walstad C (2008) Breaking and fixing public-key kerberos. Inf Comput 206(2–4):402–424, DOI
  11. 11.
    Chevalier Y, Compagna L, Cuellar J, Hankes Drielsma P, Mantovani J, Mödersheim S, Vigneron L (2004) A high level protocol specification language for industrial security-sensitive protocols. In: Proceedings of Workshop on Specification and Automated Processing of Security Requirements (SAPS), Linz, Austria, (13 pages)Google Scholar
  12. 12.
    Cremers C (2006) Scyther – semantics and verification of security protocols. Ph.D. dissertation, Eindhoven University of TechnologyGoogle Scholar
  13. 13.
    Dierks T, Allen C (1999) RFC 2246: The TLS Protocol Version 1.0. IETF – Standard TrackGoogle Scholar
  14. 14.
    Dolev D, Yao A (1983) On the Security of Public-Key Protocols. IEEE Transactions on Information Theory 2(29)Google Scholar
  15. 15.
    Google (2008) Web-based reference implementation of SAML-based SSO for Google Apps. http : //
  16. 16.
    Gürgens S, Rudolph C (2004) Security Analysis of (Un-) Fair Non-repudiation Protocols. Formal aspects of computingGoogle Scholar
  17. 17.
    Gürgens S, Ochsenschläger P, Rudolph C (2002) Role based specification and security analysis of cryptographic protocols using asynchronous product automata. In: DEXA 2002 International Workshop on Trust and Privacy in Digital Business, IEEEGoogle Scholar
  18. 18.
    Jürjens J (2005) Secure Systems Development with UML. Springer VerlagGoogle Scholar
  19. 19.
    OASIS (2005) Security Assertion Markup Language (SAML) v2.0. Available at http ://www.oasis – = security
  20. 20.
    Ochsenschläger P, Repp J, Rieke R, Nitsche U (1999) The SH-Verification Tool – Abstraction-Based Verification of Co-operating Systems. Formal Aspects of Computing, The Int Journal of Formal Methods 11:1–24Google Scholar
  21. 21.
    Ochsenschläger P, Repp J, Rieke R (2000) Abstraction and composition – a verification method for co-operating systems. Journal of Experimental and Theoretical Artificial Intelligence 12:447–459MATHCrossRefGoogle Scholar
  22. 22.
    Paulson L (1996) Proving Properties of Security Protocols by Induction. Tech. Rep. 409, Computer Laboratory, University of CambridgGoogle Scholar
  23. 23.
    Polk WT, Dodson DF, Burr WE (2007) NIST Special Publication 800-78-1, Cryptographic Algorithms and Key Sizes for PIV.
  24. 24.
    The AVISPA Project (2007) Analysis of the tls protocol.

Copyright information

© Springer-Verlag US 2009

Authors and Affiliations

  • Carsten Rudolph
    • 1
  • Luca Compagna
    • 2
  • Roberto Carbone
    • 3
  • Antonio Muñoz
    • 4
  • Jürgen Repp
    • 5
  1. 1.Fraunhofer Institute of Secure Information TechnologyDarmstadtGermany
  2. 2.SAP ResearchSophia AntipolisFrance
  3. 3.University of GenovaGenovaItaly
  4. 4.University of MalagaMalagaSpain
  5. 5.Fraunhofer Institute of Secure Information TechnologyDarmstadtGermany

Personalised recommendations