Specification of Security and Dependability Properties

  • Sigrid Gürgens
  • Gimena Pujol
Part of the Advances in Information Security book series (ADIS, volume 45)


SERENITY S&D Classes as well as S&D Patterns specify the security properties they provide. In order for a system designer to select the correct class and pattern, the security property specification must be both unambiguous and intuitive. Furthermore, in case no class or pattern can be found that provides the exact property desired by the system designer, classes and patterns providing stronger properties will also serve his/her needs. Hence there is the necessity to be able to find and prove relations between properties. In this chapter we introduce the SERENITY approach for the specification of S&D properties that are both intuitively understandable and based on a formal semantics that allows to prove relations between properties. In fact, we use two different languages: the Operational S&D Properties Language, and the Formal S&D Properties Language.


Formal Semantic Security Property Serenity Standard Epistemic Logic Proof Assistant 
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.
    Barras B, Boutin S, Cornes C, Courant J, Filliatre J, Giménez E, Herbelin H, Huet G, noz CM, Murthy C, Parent C, Paulin C, Saïbi A, Werner B (1997) The Coq Proof Assistant Reference Manual – Version V6.1. Tech. Rep. 0203, INRIAGoogle Scholar
  2. 2.
    Bellare M, Canetti R, Krawczyk H (1998) A modular approach to the design and analysis of authentication and key exchange protocols. In: 30th Annual Symposium on the Theory of Computing, ACMGoogle Scholar
  3. 3.
    Bossi A, Focardi R, Piazza C, Rossi S (2004) Verifying Persistent Security Properties. Computer Languages, Systems and Structures 30:231–258MATHCrossRefGoogle Scholar
  4. 4.
    Boyd C (1993) Security Architectures Using Formal Methods. IEEE Journal on Selected Areas in Communication 11(5)Google Scholar
  5. 5.
    Burrows M, Abadi M, Needham R (1990) A Logic of Authentication. ACM Transactions on Computer Systems 8Google Scholar
  6. 6.
    Cohen M, Dam M (2005) Logical Omniscience in the Semantics of BAN Logics. In: Foundations of Computer Security FCS'05, pp 121–132Google Scholar
  7. 7.
    Cortier V, Rusinowitch M, Zalinescu E (2005) Relating two standard notions of secrecy. In: Computer Science Logic, Szeged (Hungary), pp 25–19Google Scholar
  8. 8.
    Dolinar K, Fuchs A, Gürgens S, Rudolph C (2008) SERENITY Project, A3 Deliverable – A3.D2.2 S&D requirements for networks and devices. EU IST IP 6th Framework Programme SERENITY 27587Google Scholar
  9. 9.
    Eilenberg S (1974) Automata, Languages and Machines. Academic Press, New YorkMATHGoogle Scholar
  10. 10.
    Evans N (2001) A practical introduction to using CSP and PVS to prove authentication properties of security protocols. In: Proceedings of Verify 2001, Lecture Notes in Computer ScienceGoogle Scholar
  11. 11.
    Focardi R (1996) Comparing Two Information Flow Security Properties. In: Proceedings of the 9 Computer Security Foundations Workshop, IEEE Computer SocietyGoogle Scholar
  12. 12.
    Focardi R, Gorrieri R (2001) Classification of Security Properties. Part I: Information Flow. In Foundations of Security Analysis and Design (RFocardi, RGorrieri eds) LNCS 2171:331–396Google Scholar
  13. 13.
    Focardi R, Gorrieri R, Panini V (1995) The Security Checker: a Semantics-based Tool for the Verification of Security Properties. In: Ed LG (ed) Proceedings of Eighth IEEE Computer Security Foundations Workshop (CSFW'95), IEEE Press, Kenmare (Ireland), pp 60–69CrossRefGoogle Scholar
  14. 14.
    Focardi R, Gorrieri R, Martinelli F (2003) A Comparison of Three Authentication Properties. Theoretical Computer Science 291(3):219–388CrossRefMathSciNetGoogle Scholar
  15. 15.
    Focardi R, Gorrieri R, Martinelli F (2004) Classification of Security Properties (Part II: Network Security). Lecture notes in computer scienceGoogle Scholar
  16. 16.
    Gürgens S, Ochsenschläger P, Rudolph C (2005) On a formal framework for security properties. International Computer Standards & Interface Journal (CSI), Special issue on formal methods, techniques and tools for secure and reliable applications 27(5):457–466Google Scholar
  17. 17.
    Hoare C (1985) Communicating Sequential Process. London: Prentice-Hall International, UK, LTD.Google Scholar
  18. 18.
    ISO/IEC (1996) ISO/IEC 14977 Information technology – Syntactic metalanguage – Extended BNFGoogle Scholar
  19. 19.
    Jacob J (1988) Security Specifications. In: Proceedings of the 1988 IEEE Symposium on Research in Security arid Privacy, IEEE PressGoogle Scholar
  20. 20.
    Lowe G (1997) A hierarchy of authentication specifications. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop (CSFW'97), IEEE Society Press, pp 31–43Google Scholar
  21. 21.
    Mantel H (2000) Possibilistic Definitions of Security – an Assembly Kit. In: Proceedings of the IEEE Computer Security Foundations Workshop, pp 185–199Google Scholar
  22. 22.
    McLean J (1994) A General Theory of Composition for Trace Sets Closed under Selective Interleaving Functions. In: Proceedings of the 1994 IEEE Symposium on Security and Privacy, IEEE PressGoogle Scholar
  23. 23.
    Menezes A, van Oorschot P, Vanstone S (1996) Handbook of Applied Cryptography. CRC PressGoogle Scholar
  24. 24.
    Pujol G, et al (2008) SERENITY Project, A5 Deliverable – A5.D3.2 Security Properties Specification Language (final version) and Property Reasoning Mechanisms. EU IST IP 6th Framework Programme SERENITY 27587Google Scholar
  25. 25.
    Schneider S (1996) Security properties and CSP. In: Proceedings of the 1996 IEEE Symposium on Security and Privacy, IEEE PressGoogle Scholar
  26. 26.
    Zakinthinos A, Lee E (1997) A General Theory of Security Properties. In: Proceedings of the 18th IEEE Computer Society Symposium on Research in Security and PrivacyGoogle Scholar

Copyright information

© Springer-Verlag US 2009

Authors and Affiliations

  1. 1.Fraunhofer Institute for Secure Information TechnologyDarmstadtGermany
  2. 2.Campus de TeatinosUniversity of MalagaMalagaSpain

Personalised recommendations