Skip to main content
SpringerLink
Log in

Architecting Security with Paradigm

  • Chapter
Architecting Dependable Systems VI

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5835))

Abstract

For large security systems a clear separation of concerns is achieved through architecting. Particularly the dynamic consistency between the architectural components should be addressed, in addition to individual component behaviour. In this paper, relevant dynamic consistency is specified through Paradigm, a coordination modeling language based on dynamic constraints. As it is argued, this fits well with security issues. A smaller example introduces the architectural approach towards implementing security policies. A larger casestudy illustrates the use of Paradigm in analyzing the FOO voting scheme. In addition, translating the Paradigm models into process algebra brings model checking within reach. Security properties of the examples discussed, are formally verified with the model checker mCRL2.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ahmed, T., Tripahti, A.R.: Specification and verification of security requirements in a programming model for decentralized CSCW systems. Transactions on Information and Systems Security 10, Article 7 (2007)

    Google Scholar 

  2. Anderson, R.: A Guide to Building Dependable Distributed Systems. Wiley, Chichester (2001)

    Google Scholar 

  3. Andova, S., Groenewegen, L., de Vink, E.: System evolution by migration coordination. In: Serebrenik, A. (ed.) Proc. BENEVOL 2008, pp. 18–21. Technische Universiteit Eindhoven, Eindhoven (2008)

    Google Scholar 

  4. Andova, S., Groenewegen, L.P.J., de Vink, E.P.: Dynamic consistency in process algebra: From Paradigm to ACP. In: Canal, C., Poizat, P., Sirjani, M. (eds.) Proc. FOCLASA 2008. ENTCS, p. 19 (2008) (extended version submitted) (to appear)

    Google Scholar 

  5. Andova, S., Groenewegen, L.P.J., de Vink, E.P.: Formalizing adaptation on-the-fly. In: Salaün, G., Sirjani, M. (eds.) Proc. FOCLASA 2009. ENTCS (to appear, 2009)

    Google Scholar 

  6. Basin, D., Doser, J., Lodderstedt, T.: Model driven security: UML models to access control infrastructures. Transactions on Software Engineering and Methodology 15, 39–91 (2006)

    Article  Google Scholar 

  7. Basin, D.A., Mödersheim, S., Viganò, L.: OFMC: A symbolic model checker for security protocols. Journal of Information Security 4, 181–208 (2005)

    Article  Google Scholar 

  8. Bhargava, M., Palamidessi, C.: Probabilistic anonymity. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 171–185. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proc. CSFW, Cape Breton, pp. 82–96. IEEE, Los Alamitos (2001)

    Google Scholar 

  10. Braghin, C., Gorla, D., Sassone, V.: Role-based access control for a distributed calculus. Journal of Computer Security 14, 113–155 (2006)

    Google Scholar 

  11. Bravetti, M., Busi, N., Gorrieri, R., Lucchi, R., Zavattaro, G.: Security issues in the tuple-space coordination model. In: Dimitrakos, T., Martinelli, F. (eds.) Proc. FAST 2004, p. 13. Kluwer, Dordrecht (2005)

    Google Scholar 

  12. Cremers, C.J.F.: Scyther: Semantics and Verification of Security Protocols. PhD thesis, Technische Universiteit Eindhoven (2006)

    Google Scholar 

  13. van Eijck, J., Orzan, S.: Epistemic verification of anonymity. In: ter Beek, M., Cadducci, F. (eds.) Proc. VODCA 2006. ENTCS, vol. 168, pp. 159–174 (2007)

    Google Scholar 

  14. Fujioka, A., Okamoto, T.: A practical secret voting scheme for large scale elections. In: Zheng, Y., Seberry, J. (eds.) AUSCRYPT 1992. LNCS, vol. 718, pp. 244–251. Springer, Heidelberg (1993)

    Google Scholar 

  15. Garcia, F.D., Hasuo, I., Pieters, W., van Rossum, P.: Provable anonymity. In: Atluri, V., Samarati, P., Küsters, R., Mitchell, J.C. (eds.) Proc. FMSE, Fairfax, pp. 63–72. ACM, New York (2005)

    Chapter  Google Scholar 

  16. Garlan, D.: Software architecture: a roadmap. In: Proc. ICSE 2000, Limerick, pp. 91–101. ACM, New York (2000)

    Chapter  Google Scholar 

  17. Groenewegen, L., de Vink, E.P.: Operational semantics for coordination in Paradigm. In: Arbab, F., Talcott, C. (eds.) COORDINATION 2002. LNCS, vol. 2315, pp. 191–206. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  18. Groenewegen, L., de Vink, E.: Evolution on-the-fly with Paradigm. In: Ciancarini, P., Wiklicky, H. (eds.) COORDINATION 2006. LNCS, vol. 4038, pp. 97–112. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Groenewegen, L.P.J., Stam, A.W., Toussaint, P.J., de Vink, E.P.: Paradigm as organization-oriented coordination language. In: van de Torre, L., Boella, G. (eds.) Proc. CoOrg 2005. ENTCS, vol. 150(3), pp. 93–113 (2005)

    Google Scholar 

  20. Groenewegen, L.P.J., de Vink, E.P.: Dynamic system adaptation by constraint orchestration. Technical Report CSR 08/29, Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, p.20, arXiv:0811.3492v1 (2008)

    Google Scholar 

  21. Groote, J.F., Mathijssen, A.H.J., Reniers, M.A., Usenko, Y.S., van Weerdenburg, M.J.: The formal specification language mCRL2. In: Brinksma, E., Harel, D., Mader, A., Stevens, P., Wieringa, R. (eds.) Methods for Modelling Software Systems, IBFI, Schloss Dagstuhl, 34 pages (2007)

    Google Scholar 

  22. Groote, J.F., Reniers, M.A.: Algebraic process verification. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 1151–1208. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  23. Groote, J.F., Willemse, T.: Parameterised boolean equation systems. Theoretical Computer Science 343, 332–369 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  24. Kramer, J., Magee, J., Uchitel, S.: Software architecture modeling & analysis: A rigorous approach. In: Bernardo, M., Inverardi, P. (eds.) SFM 2003. LNCS, vol. 2804, pp. 44–51. Springer, Heidelberg (2003)

    Google Scholar 

  25. Kremer, S., Ryan, M.: Analysis of an electronic voting protocol in the applied Pi calculus. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 186–200. Springer, Heidelberg (2005)

    Google Scholar 

  26. Krukow, K., Nielsen, M., Sassone, V.: A logical framework for history-based access control and reputation systems. Journal of Computer Security 16, 63–101 (2008)

    Google Scholar 

  27. Küster, J.: Consistency Management of Object-Oriented Behavioral Models. PhD thesis, University of Paderborn (2004)

    Google Scholar 

  28. Lankhorst, M. (ed.): Enterprise Architecture at Work: Modelling, Communication and Analysis. Springer, Heidelberg (2005)

    Google Scholar 

  29. Lomuscio, A., Raimondi, F.: MCMAS: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) Proc. TACAS. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)

    Google Scholar 

  30. Lopes, A., Wermelinger, M., Fiadeiro, J.L.: Higher-order architectural connectors. Transactions on Software Engineering and Methodology 12, 64–104 (2003)

    Article  Google Scholar 

  31. Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055. Springer, Heidelberg (1996)

    Google Scholar 

  32. Mauw, S., Verschuren, J., de Vink, E.P.: Data anonymity in the FOO voting scheme. In: ter Beek, M., Gadducci, F. (eds.) Proc. VODCA 2006. ENTCS, vol. 168, pp. 5–28 (2007)

    Google Scholar 

  33. Mauw, S., Verschuren, J., de Vink, E.P.: A formalization of anonymity and onion routing. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 109–124. Springer, Heidelberg (2004)

    Google Scholar 

  34. Mauw, S., Verschuren, J., de Vink, E.P.: Data anonymity in the FOO voting scheme. In: ter Beek, M., Gadducci, F. (eds.) Proc. VODCA 2006. ENTCS, vol. 168, pp. 5–28 (2007)

    Google Scholar 

  35. van der Meyden, R., Su, K.: Symbolic model checking the knowledge of the dining cryptographers. In: Proc. CSFW, Pacific Grove, pp. 280–291. IEEE, Los Alamitos (2004)

    Google Scholar 

  36. Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proc. CCS, Philadelphia, pp. 166–175. ACM, New York (2001)

    Google Scholar 

  37. Omicini, A.: Towards a notion of agent coordination context. In: Marinescu, D.C., Lee, C. (eds.) Process Coordination and Ubiquitous Computing, ch. 12, pp. 187–200. CRC Press, Boca Raton (2002)

    Google Scholar 

  38. Schneider, S., Sidiropoulos, A.: CSP and anonymity. In: Bertino, E., Kurth, H., Martella, G., Montolivo, E. (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 198–218. Springer, Heidelberg (1996)

    Google Scholar 

  39. Serjantov, A., Danezis, G.: Towards an information theoretic metric for anonymity. In: Dingledine, R., Syverson, P.F. (eds.) PET 2002. LNCS, vol. 2482, pp. 41–53. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  40. Shmatikov, V.: Probabilistic analysis of an anonymity system. Journal of Computer Security 12, 355–377 (2004)

    Google Scholar 

  41. Shmatikov, V., Talcott, C.L.: Reputation-based trust management. Journal of Computer Security 13, 167–190 (2005)

    Google Scholar 

  42. Song, D.X., Berezin, S., Perrig, A.: Athena: A novel approach to efficient automatic security protocol analysis. Journal of Computer Security 9, 47–74 (2001)

    Google Scholar 

  43. Stam, A.W.: Interaction Protocols in Paradigm. PhD thesis, LIACS, Leiden University (Forthcoming) (2009)

    Google Scholar 

  44. Vitek, J., Bryce, C., Oriol, M.: Coordinating processes with secure spaces. Science of Computer Programming 46, 163–193 (2003)

    Article  MATH  Google Scholar 

  45. Zhang, N., Ryan, M., Guelev, D.P.: Synthesising verified access control systems through model checking. Journal of Computer Security 16, 1–61 (2008)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, The Netherlands

    Suzana Andova & Erik P. de Vink

  2. LIACS, Leiden University, The Netherlands

    Luuk P. J. Groenewegen & Jan H. S. Verschuren

Authors
  1. Suzana Andova
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luuk P. J. Groenewegen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jan H. S. Verschuren
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Erik P. de Vink
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, Canterbury, University of Kent, CT2 7NF, Kent, UK

    Rogério de Lemos

  2. LAAS-CNRS, 7, avenue du Colonel Roche, 31077, Toulouse Cedex 4, France

    Jean-Charles Fabre

  3. School of Computing Science, Newcastle upon Tyne, University of Newcastle upon Tyne, NE1 7RU, UK

    Cristina Gacek

  4. Dipartimento di Informatica, Largo Pontecorvo 3c, Università di Pisa, 56127, Pisa, Italy

    Fabio Gadducci

  5. Istituto di Scienza e Tecnologie dell’Informazione (ISTI-CNR), Area della Ricerca di Pisa, Via G. Moruzzi 1, 56124, Pisa, Italy

    Maurice ter Beek

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Andova, S., Groenewegen, L.P.J., Verschuren, J.H.S., de Vink, E.P. (2009). Architecting Security with Paradigm. In: de Lemos, R., Fabre, JC., Gacek, C., Gadducci, F., ter Beek, M. (eds) Architecting Dependable Systems VI. Lecture Notes in Computer Science, vol 5835. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10248-6_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-10248-6_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-10247-9

  • Online ISBN: 978-3-642-10248-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation