Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Techniques for Distributed Objects, Components, and Systems

FORTE 2017: Formal Techniques for Distributed Objects, Components, and Systems pp 156–170Cite as

Reasoning About Distributed Secrets

  • Conference paper
  • First Online:

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

Abstract

In 1977 Tore Dalenius described how partial disclosure about one secret can impact the confidentiality of other correlated secrets, and indeed this phenomenon is well-known in privacy of databases. The aim here is to study this issue in a context of programs with distributed secrets. Moreover, we do not assume that secrets never change, in fact we investigate what happens when they do: we explore how updates to some (but not all) secrets can affect confidentiality elsewhere in the system.

We provide methods to compute robust upper bounds on the impact of such information leakages with respect to all distributed secrets. Finally we illustrate our results on a defence against side channels.

This is a preview of subscription content, 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 EPUB and 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

Learn about institutional subscriptions

Notes

  1. 1.

    We write dot for function application, left associative, so that function g applied to argument w is g.w and then g.w.x is (g.w) applied to x, that is using the Currying technique of functional programming.

  2. 2.

    Although the matrices \(C^{2}\) and \(M^{S1}\) look the same, they are describing different aspects of the system.

  3. 3.

    We have overloaded matrix multiplication, to mean that the summation is always over the shared state in \(M^1\cdot M^2\).

  4. 4.

    Notice that the exact value \(y^*\) is not important for refinement comparisons.

  5. 5.

    Definition 2 defines a pre-order on HMM’s, but it can be made into a partial order on “abstract HMM’s”, introduced elsewhere [21].

References

  1. Alvim, M.S., Chatzikokolakis, K., McIver, A., Morgan, C., Palamidessi, C., Smith, G.: Additive and multiplicative notions of leakage, and their capacities. In: CSF, pp. 308–322. IEEE (2014)

    Google Scholar 

  2. Alvim, M.S., Scedrov, A., Schneider, F.B.: When not all bits are equal: worth-based information flow. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 120–139. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54792-8_7

    Chapter  Google Scholar 

  3. Bordenabe, N., McIver, A., Morgan, C., Rabehaja, T.: Compositional security and collateral leakage (2016). arXiv:1604.04983

  4. Bordenabe, N.E., Smith, G.: Correlated secrets in quantitative information flow. In: IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, 27 June - 1 July 2016, pp. 93–104 (2016)

    Google Scholar 

  5. Chatzikokolakis, K., Palamidessi, C., Panangaden, P.: Anonymity protocols as noisy channels. Inf. Comput. 206(2–4), 378–401 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  6. Clark, D., Hunt, S., Malacaria, P.: Quantitative analysis of the leakage of confidential data. Electron. Notes Theoret. Comput. Sci. 59(3), 238–251 (2001)

    Article  Google Scholar 

  7. Clark, D., Hunt, S., Malacaria, P.: Quantified interference for a while language. Electron. Notes Theoret. Comput. Sci. 112, 149–166 (2005)

    Article  MATH  Google Scholar 

  8. Clarkson, M.R., Myers, A.C., Schneider, F.B.: Belief in information flow. In: 18th IEEE Computer Security Foundations Workshop, (CSFW-18 2005), 20–22 June 2005, Aix-en-Provence, France, pp. 31–45 (2005)

    Google Scholar 

  9. Dalenius, T.: Towards a methodology for statistical disclosure control. Statistik Tidskrift 15, 429–444 (1977)

    Google Scholar 

  10. Doychev, G., Köpf, B.: Rational protection against timing attacks. In: IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13–17 July 2015, pp. 526–536 (2015)

    Google Scholar 

  11. Dwork, C.: Differential privacy. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 1–12. Springer, Heidelberg (2006). doi:10.1007/11787006_1

    Chapter  Google Scholar 

  12. Espinoza, B., Smith, G.: Min-entropy as a resource. Inf. Comput. 226, 57–75 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  13. Green, P.J., Noad, R., Smart, N.P.: Further hidden Markov model cryptanalysis. In: Rao, J.R., Sunar, B. (eds.) CHES 2005. LNCS, vol. 3659, pp. 61–74. Springer, Heidelberg (2005). doi:10.1007/11545262_5

    Chapter  Google Scholar 

  14. Karlof, C., Wagner, D.: Hidden Markov model cryptanalysis. In: Walter, C.D., Koç, Ç.K., Paar, C. (eds.) CHES 2003. LNCS, vol. 2779, pp. 17–34. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45238-6_3

    Chapter  Google Scholar 

  15. Kawamoto, Y., Chatzikokolakis, K., Palamidessi, C.: Compositionality results for quantitative information flow. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 368–383. Springer, Cham (2014). doi:10.1007/978-3-319-10696-0_28

    Google Scholar 

  16. Lenstra, A.K., Hughes, J.P., Augier, M., Kleinjung, T., Wachter, C.: Ron was wrong, Whit is right. Technical report, EPFL IC LACAL, Station 14, CH-1015 Lausanne, Switzerland (2012)

    Google Scholar 

  17. Mardziel, P., Alvim, M.S., Hicks, M.W., Clarkson, M.R.: Quantifying information flow for dynamic secrets. In: 2014 IEEE Symposium on Security and Privacy, SP 2014, Berkeley, CA, USA, 18–21 May 2014, pp. 540–555 (2014)

    Google Scholar 

  18. McIver, A., Meinicke, L., Morgan, C.: Compositional closure for bayes risk in probabilistic noninterference. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 223–235. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14162-1_19

    Chapter  Google Scholar 

  19. McIver, A., Meinicke, L., Morgan, C.: Hidden-Markov program algebra with iteration. Math. Struct. Comput. Sci. 25, 320–360 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  20. McIver, A., Morgan, C., Rabehaja, T.: Abstract Hidden Markov Models: a monadic account of quantitative information flow. In: Proceedings of LICS 2015 (2015)

    Google Scholar 

  21. McIver, A., Morgan, C., Smith, G., Espinoza, B., Meinicke, L.: Abstract channels and their robust information-leakage ordering. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 83–102. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54792-8_5

    Chapter  Google Scholar 

  22. Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Upper Saddle River (1994). http://www.cs.ox.ac.uk/publications/books/PfS/

    MATH  Google Scholar 

  23. Smith, G.: On the foundations of quantitative information flow. In: Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 288–302. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00596-1_21

    Chapter  Google Scholar 

  24. Walter, C.D.: MIST: an efficient, randomized exponentiation algorithm for resisting power analysis. In: Preneel, B. (ed.) CT-RSA 2002. LNCS, vol. 2271, pp. 53–66. Springer, Heidelberg (2002). doi:10.1007/3-540-45760-7_5

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, Macquarie University, Sydney, Australia

    Nicolás Bordenabe, Annabelle McIver & Tahiry Rabehaja

  2. DATA61 and University of New South Wales, Sydney, Australia

    Carroll Morgan

Authors
  1. Nicolás Bordenabe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Annabelle McIver
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Carroll Morgan
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Tahiry Rabehaja
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Annabelle McIver .

Editor information

Editors and Affiliations

  1. University Paris Diderot, Paris, France

    Ahmed Bouajjani

  2. University College London, London, United Kingdom

    Alexandra Silva

Rights and permissions

Reprints and permissions

Copyright information

© 2017 IFIP International Federation for Information Processing

About this paper

Cite this paper

Bordenabe, N., McIver, A., Morgan, C., Rabehaja, T. (2017). Reasoning About Distributed Secrets. In: Bouajjani, A., Silva, A. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2017. Lecture Notes in Computer Science(), vol 10321. Springer, Cham. https://doi.org/10.1007/978-3-319-60225-7_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-60225-7_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-60224-0

  • Online ISBN: 978-3-319-60225-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Societies and partnerships

Search

Navigation