Document Open Access Logo

Compositional Weak Metrics for Group Key Update

Authors Ruggero Lanotte, Massimo Merro, Simone Tini

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2017.72.pdf
  • Filesize: 0.87 MB
  • 16 pages

Document Identifiers

Author Details

Ruggero Lanotte
Massimo Merro
Simone Tini

Cite As Get BibTex

Ruggero Lanotte, Massimo Merro, and Simone Tini. Compositional Weak Metrics for Group Key Update. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 72:1-72:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.MFCS.2017.72

Abstract

We investigate the compositionality of both weak bisimilarity metric and weak similarity quasi- metric semantics with respect to a variety of standard operators, in the context of probabilistic process algebra. We show how compositionality with respect to nondeterministic and probabilistic choice requires to resort to rooted semantics. As a main application, we demonstrate how our results can be successfully used to conduct compositional reasonings to estimate the performances of group key update protocols in a multicast setting.

Subject Classification

Keywords
  • Behavioural metric
  • compositional reasoning
  • group key update

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Luca Aceto, Bard Bloom, and Fritz W. Vaandrager. Turning SOS Rules into Equations. Information &Computation, 111(1):1-52, 1994. URL: http://dx.doi.org/10.1006/inco.1994.1040.
  2. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Computing Behavioral Distances, Compositionally. In 38th International Symposium on Mathematical Foundations of Computer Science, volume 8087 of LNCS, pages 74-85. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40313-2_9.
  3. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Converging from Branching to Linear Metrics on Markov Chains. In 12th International Colloquium on Theoretical Aspects of Computing, volume 9399 of LNCS, pages 349-367. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-25150-9_21.
  4. Christel Baier, Holger Hermanns, and Joost-Pieter Katoen. Probabilistic Weak Simulation is Decidable in Polynomial Time. Information Processing Letters, 89(3):123-130, 2004. URL: http://dx.doi.org/10.1016/j.ipl.2003.10.001.
  5. Christel Baier, Joost-Pieter Katoen, Holger Hermanns, and Boudewijn R. Haverkort. Simulation for Continuous-Time Markov Chains. In 13th International Conf. on Concurrency Theory, volume 2421 of LNCS, pages 338-354, 2002. URL: http://dx.doi.org/10.1007/3-540-45694-5_23.
  6. Falk Bartels. On Generalised Coinduction and Probabilistic Specification Formats. PhD thesis, VU University Amsterdam, 2004. Google Scholar
  7. Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation Can't Be Traced. Journal of the ACM, 42:232-268, 1995. URL: http://dx.doi.org/10.1145/200836.200876.
  8. Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, and Tatjana Petrov. Linear Distances between Markov Chains. In 27th International Conference on Concurrency Theory, LIPIcs, pages 20:1-20:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.20.
  9. Pedro R. D'Argenio, Daniel Gebler, and Matias D. Lee. Axiomatizing Bisimulation Equivalences and Metrics from Probabilistic SOS Rules. In 17th International Conference on Foundations of Software Science and Computation Structures, volume 8412 of LNCS, pages 289-303. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54830-7_19.
  10. Pedro R. D'Argenio, Daniel Gebler, and Matias D. Lee. A General SOS Theory for the Specification of Probabilistic Transition Systems. Information &Computation, 249:76-109, 2016. URL: http://dx.doi.org/10.1016/j.ic.2016.03.009.
  11. Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and Branching System Metrics. IEEE Trans. Software Eng., 35(2):258-273, 2009. URL: http://dx.doi.org/10.1109/TSE.2008.106.
  12. Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Discounting the Future in Systems Theory. In 30th Int. Colloquium on Automata, Languages and Programming, volume 2719 of LNCS, pages 1022-1037. Springer, 2003. URL: http://dx.doi.org/10.1007/3-540-45061-0_79.
  13. Luca de Alfaro, Rupak Majumdar, Vishwanath Raman, and Mariëlle Stoelinga. Game Relations and Metrics. In 22nd IEEE Symposium on Logic in Computer Science, pages 99-108. IEEE Computer Society, 2007. URL: http://dx.doi.org/10.1109/LICS.2007.22.
  14. Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang. Metrics for Action-labelled Quantitative Transition Systems. ENTCS, 153(2):79-96, 2006. URL: http://dx.doi.org/10.1016/j.entcs.2005.10.033.
  15. Yuxin Deng and Wenjie Du. The Kantorovich Metric in Computer Science: A Brief Survey. ENTCS, 253(3):73-82, 2009. URL: http://dx.doi.org/10.1016/j.entcs.2009.10.006.
  16. Yuxin Deng, Rob J. van Glabbeek, Matthew Hennessy, and Carroll Morgan. Characterising Testing Preorders for Finite Probabilistic Processes. Logical Methods in Computer Science, 4(4), 2008. URL: http://dx.doi.org/10.2168/LMCS-4(4:4)2008.
  17. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for Labelled Markov Processes. Theoretical Computer Science, 318(3):323-354, 2004. URL: http://dx.doi.org/10.1016/j.tcs.2003.09.013.
  18. Josée Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden. The Metric Analogue of Weak Bisimulation for Probabilistic Processes. In 17th IEEE Symposium on Logic in Computer Science, pages 413-422. IEEE Computer Society, 2002. URL: http://dx.doi.org/10.1109/LICS.2002.1029849.
  19. Uli Fahrenberg and Axel Legay. The Quantitative Linear-time-branching-time Spectrum. Theoretical Computer Science, 538:54-69, 2014. URL: http://dx.doi.org/10.1016/j.tcs.2013.07.030.
  20. Daniel Gebler, Kim G. Larsen, and Simone Tini. Compositional Bisimulation Metric Reasoning with Probabilistic Process Calculi. Logical Methods in Computer Science, 12(4), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(4:12)2016.
  21. Daniel Gebler and Simone Tini. Fixed-point Characterization of Compositionality Properties of Probabilistic Processes Combinators. In Combined 21th International Workshop on Expressiveness in Concurrency and 11th Workshop on Structural Operational Semantics, volume 160 of EPTCS, pages 63-78. OPA, 2014. URL: http://dx.doi.org/10.4204/EPTCS.160.7.
  22. Daniel Gebler and Simone Tini. SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators. In 26th Conference on Concurrency Theory, volume 42 of LIPIcs, pages 155-168. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  23. Hans Hansson and Bengt Jonsson. A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing, 6(5):512-535, 1994. URL: http://dx.doi.org/10.1007/BF01211866.
  24. Bengt Jonsson, Kim G. Larsen, and Wang Yi. Probabilistic Extensions of Process Algebras. In Handbook of Process Algebra, pages 685-710. Elsevier, 2001. Google Scholar
  25. Leonid V. Kantorovich. On the transfer of masses. Doklady Akademii Nauk, 37(2):227-229, 1942. Original article in Russian, translation in Management Science, 5: 1-4 (1959). Google Scholar
  26. Robert M. Keller. Formal Verification of Parallel Programs. Communications of the ACM, 19(7):371-384, 1976. URL: http://dx.doi.org/10.1145/360248.360251.
  27. Ruggero Lanotte, Andrea Maggiolo-Schettini, and Angelo Troina. Time and Probability-based Information Flow Analysis. IEEE Transactions on Software Engineering, 36(5):719-734, 2010. URL: http://dx.doi.org/10.1109/TSE.2010.4.
  28. Ruggero Lanotte, Andrea Maggiolo-Schettini, and Angelo Troina. Weak bisimulation for Probabilistic Timed Automata. Theoretical Computer Science, 411(50):4291-4322, 2010. URL: http://dx.doi.org/10.1016/j.tcs.2010.09.003.
  29. Ruggero Lanotte and Massimo Merro. Semantic Analysis of Gossip Protocols for Wireless Sensor Networks. In 22nd International Conference on Concurrency Theory, volume 6901 of LNCS, pages 156-170. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-23217-6_11.
  30. Ruggero Lanotte, Massimo Merro, and Simone Tini. Weak Simulation Quasimetric in a Gossip Scenario. In 37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, volume 10321 of LNCS, pages 139-155. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-319-60225-7_10.
  31. Matteo Mio. Upper-Expectation Bisimilarity and Łukasiewicz μ-Calculus. In 17th International Conference on Foundations of Software Science and Computation Structures, volume 8412 of LNCS, pages 335-350. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54830-7_22.
  32. Sandro Rafaeli and David Hutchison. A Survey of Key Management for Secure Group Communication. ACM Comput. Surv., 35(3):309-329, 2003. URL: http://dx.doi.org/10.1145/937503.937506.
  33. Roberto Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, 1995. Google Scholar
  34. William J. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1994. Google Scholar
  35. Frank van Breugel and J. Worrell. A Behavioural Pseudometric for Probabilistic Transition Systems. Theor. Comput. Sci., 331(1):115-142, 2005. URL: http://dx.doi.org/10.1016/j.tcs.2006.05.021.
  36. Rob J. van Glabbeek and Peter W. Weijland. Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM, 43(3):555-600, 1996. URL: http://dx.doi.org/10.1145/233551.233556.
  37. Cédric Villani. Optimal Transport: Old and New. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-540-71050-9.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact