Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
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 3576
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, LNCS
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, ACM
AVANTSSAR (2008) The AVANTSSAR Project. www.avantssar.eu/
AVISPA (2007) The AVISPA Project. www.avispa-project.org/
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–104
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–45
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–96
Bundesamt für Sicherheit in der Informationstechnik (BSI) (2008) Itgrundschutz-kataloge. URL: http://www.bsi.de/gshb/deutsch/index.htm
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 http://dx.doi.org/10.1016/j.ic.2007.05.005
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)
Cremers C (2006) Scyther – semantics and verification of security protocols. Ph.D. dissertation, Eindhoven University of Technology
Dierks T, Allen C (1999) RFC 2246: The TLS Protocol Version 1.0. IETF – Standard Track
Dolev D, Yao A (1983) On the Security of Public-Key Protocols. IEEE Transactions on Information Theory 2(29)
Google (2008) Web-based reference implementation of SAML-based SSO for Google Apps. http : //code.google.com/apis/apps/sso/samlreferenceimplementationweb.html
Gürgens S, Rudolph C (2004) Security Analysis of (Un-) Fair Non-repudiation Protocols. Formal aspects of computing
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, IEEE
Jürjens J (2005) Secure Systems Development with UML. Springer Verlag
OASIS (2005) Security Assertion Markup Language (SAML) v2.0. Available at http ://www.oasis – open.org/committees/tchome.php?wgabbrev = security
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–24
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–459
Paulson L (1996) Proving Properties of Security Protocols by Induction. Tech. Rep. 409, Computer Laboratory, University of Cambridg
Polk WT, Dodson DF, Burr WE (2007) NIST Special Publication 800-78-1, Cryptographic Algorithms and Key Sizes for PIV. http://csrc.nist.gov/publications/nistpubs/800-78-1/SP-800-78-1_final2.pdf
The AVISPA Project (2007) Analysis of the tls protocol. www.avispa-project.org/library/TLS.html
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag US
About this chapter
Cite this chapter
Rudolph, C., Compagna, L., Carbone, R., Muñoz, A., Repp, J. (2009). Verification of S&D Solutions for Network Communications and Devices. In: Kokolakis, S., Gómez, A., Spanoudakis, G. (eds) Security and Dependability for Ambient Intelligence. Advances in Information Security, vol 45. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-88775-3_9
Download citation
DOI: https://doi.org/10.1007/978-0-387-88775-3_9
Published:
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-88774-6
Online ISBN: 978-0-387-88775-3
eBook Packages: Computer ScienceComputer Science (R0)