[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
research-article
Open access

Abstractions of non-interference security: probabilistic versus possibilistic

Published: 01 January 2014 Publication History

Abstract

The Shadow Semantics (Morgan, Math Prog Construction, vol 4014, pp 359–378, 2006; Morgan, Sci Comput Program 74(8):629–653, 2009) is a possibilistic (qualitative) model for noninterference security. Subsequent work (McIver et al., Proceedings of the 37th international colloquium conference on Automata, languages and programming: Part II, 2010) presents a similar but more general quantitative model that treats probabilistic information flow. Whilst the latter provides a framework to reason about quantitative security risks, that extra detail entails a significant overhead in the verification effort needed to achieve it. Our first contribution in this paper is to study the relationship between those two models (qualitative and quantitative) in order to understand when qualitative Shadow proofs can be “promoted” to quantitative versions, i.e. in a probabilistic context. In particular we identify a subset of the Shadow’s refinement theorems that, when interpreted in the quantitative model, still remain valid even in a context where a passive adversary may perform probabilistic analysis. To illustrate our technique we show how a semantic analysis together with a syntactic restriction on the protocol description, can be used so that purely qualitative reasoning can nevertheless verify probabilistic refinements for an important class of security protocols. We demonstrate the semantic analysis by implementing the Shadow semantics in Rodin, using its special-purpose refinement provers to generate (and discharge) the required proof obligations (Abrial et al., STTT 12(6):447–466, 2010). We apply the technique to some small examples based on secure multi-party computations.

References

References

[1]
Abrial J-R, Butler M, Hallerstede S, Hoang TS, Mehta F, and Voisin L Rodin: an open toolset for modelling and reasoning in Event-B STTT 2010 12 6 447-466
[2]
Abrial J-R The B Book: assigning programs to meanings 1996 London Cambridge University Press
[3]
Andrés ME, Palamidessi C, Van Rossum P, Smith G (2010) Computing the leakage of information-hiding systems. In: Tools and algorithms for the construction and analysis of systems (TACAS). LNCS, vol 6015. Springer, Berlin, pp 373–389
[4]
Abadi M, Rogoway P (2000) Reconciling two views of cryptography (the computational soundness of formal encryption). In: Proceedings of IFIP International Conference on Theoretical Computer Science. LNCS, vol 1872. Springer, Berlin, pp 3–22
[5]
Beaver D Feigenbaum J Foundations of secure interactive computing CRYPTO ’91. LNCS, vol 576 1991 Berlin Springer 377-391
[6]
Bossi A, Focardi R, Piazza C, Rossi S (2003) Refinement operators and information flow security. In: SEFM. IEEE, Los Alamitos, pp 44–53
[7]
Bruno Blanchet (2001) An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), IEEE Computer Society, pp 82–96.
[8]
Backes M, Pfitzmann B (2002) Computational probabilistic non-interference. In: 7th European Symposium on Research in Computer Security. LNCS, vol 2502, pp 1–23
[9]
Backes M and Pfitzmann B Computational probabilistic noninterference Int J Inf Secur 2004 3 1 42-60
[10]
Bellare M, Rogoway P (1993) Random oracles are practical: a paradigm for designing efficient protocols. In: ACM Conference on Computer and Communications Security, pp 62–73
[11]
Back R-JR and von Wright J Refinement calculus: a systematic introduction 1998 Berlin Springer
[12]
Canetti R (2001) Universal composable security: a new paradigm for cryptographic protocols. In: Extended abstract appeared in proceedings of the 42nd Symposium on Foundations of Computer Science (FOCS), pp 136–145
[13]
Chor B, Goldreich O, Kushilevitz E, and Sudan M Private information retrieval J ACM 1999 45 6 965-982
[14]
Chaum D The dining cryptographers problem: unconditional sender and recipient untraceability J Cryptol 1988 1 1 65-75
[15]
Dolev D and Yao A On the security of public key protocols IEEE Trans Inf Theory 1983 29 2 198-208
[16]
Goldwasser S and Levin LA Menezes A and Vanstone SA Fair computation of general functions in presence of immoral majority CRYPTO ’90 1990 vol 537. Springer LNCS 77-93
[17]
Goguen JA, Meseguer J (1984) Unwinding and inference control. In: Proceedings of IEEE Symposium on Security and Privacy. IEEE Computer Society, pp 75–86
[18]
Goldwasser S (2002) Mathematical foundations of modern cryptography: computational complexity perspective. In: Proceedings of the ICM, Beijing, vol 1, pp 245–272
[19]
O Goldreich (2010) Studies in complexity and cryptography. In: Security preserving reductions—revised terminology. LNCS, vol 6650. Springer, Berlin
[20]
Probabilistic Systems Group. Collected publications. http://www.cse.unsw.edu.au/~carrollm/probs
[21]
Grimmett GR and Welsh D Probability: an introduction 1986 UK Oxford Science Publications
[22]
Heusser GR, Malacaria P (2010) Applied quantitative information flow and statistical databases. In: Formal aspects in security and trust. LNCS, vol 5983. Springer, Berlin, pp 96–110
[23]
Hutter D (2006) Possibilistic information flow control in MAKS and action refinement. In: Proceedings of the 2006 international conference on Emerging Trends in Information and Communication Security
[24]
Köpf B, Basin D (2007) An information-theoretic model for adaptive side-channel attacks. In: Proceedings of 14th ACM Conference on Computer and Communication Security
[25]
Leino KRM and Joshi R A semantic approach to secure information flow Sci Comput Program 2000 37 1–3 113-138
[26]
Mantel H (2001) Preserving information flow properties under refinement. In: Proceedings of IEEE Symposium on security and privacy, pp 78–91
[27]
McIver AK (2009) The secret art of computer programming. In: Proceedings of ICTAC 2009. LNCS, vol 5684, pp 61–78 (invited presentation)
[28]
McIver AK, Morgan CC (2009) The thousand-and-one cryptographers. At [Gro, McIver:10web]; includes appendices., April
[29]
McIver AK and Morgan CC Compositional refinement in agent-based security protocols Formal Aspects Comput 2011 23 6 711-737
[30]
McIver A, Meinicke L, Morgan C (2010) Compositional closure for Bayes Risk in probabilistic noninterference. In: Proceedings of the 37th international colloquium conference on Automata, languages and programming: Part II, ICALP’10. Springer, Berlin, pp 223–235
[31]
McIver A, Meinicke L, Morgan C (2011) Hidden-markov program algebra with iteration. Math Struct Comput Sci (to appear)
[32]
Morris JM A theoretical basis for stepwise refinement and the programming calculus Sci Comput Program 1987 9 3 287-306
[33]
Morgan CC (1994) Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs. http://web.comlab.ox.ac.uk/oucl/publications/books/PfS/
[34]
Morgan CC (2006) The Shadow Knows: refinement of ignorance in sequential programs. In: Uustalu T (ed), Math Prog Construction, vol 4014. Springer, Berlin, pages 359–378 (Treats Dining Cryptographers)
[35]
Morgan CC The Shadow Knows: refinement of ignorance in sequential programs Sci Comput Program 2009 74 8 629-653 (Treats Oblivious Transfer)
[36]
Micali S and Rogaway P Feigenbaum J Secure computation (abstract) CRYPTO ’91. LNCS, vol 576 1991 Berlin Springer 392-404
[37]
Paulson LC The inductive approach to verifying cryptographic protocols J Comput Secur 1998 6 85-128
[38]
Proverif: Cryptographic protocol verifier in the formal model. http://www.proverif.ens.fr/
[39]
Pfitzmann B, Waidner M (2001) A model for asynchronous reactive systems and its application to secure message transmission. In: IEEE Symposium on Security and Privacy. IEEE Computer Society, pp 184–200
[40]
Rabin MO (1981) How to exchange secrets by oblivious transfer. Technical Report TR-81, Harvard University. http://eprint.iacr.org/2005/187
[41]
Goldreich O, Canetti R, and Halevi S The random oracle methodology, revisited JACM 2004 51 4 557-594
[42]
Santen T Preservation of probabilistic information flow under refinement Inf Comput 2008 206 2–4 213-249
[43]
Shannon CE A mathematical theory of communication Bell Syst Tech J 1948 27 379-423
[44]
Sabelfeld A and Myers AC Language-based information-flow security IEEE J Sel Areas Commun 2003 21 1 5-19
[45]
Smith G (2007) Adversaries and information leaks (Tutorial). In: Barthe G, Fournet C (eds) Proceedings of 3rd Symposium on Trustworthy Global Computing. LNCS, vol 4912. Springer, Berlin, pp 383–400
[46]
Yao AC-C (1982) Protocols for secure computations (extended abstract). In: Annual Symposium on Foundations of Computer Science (FOCS 1982). IEEE Computer Society, pp 160–164

Cited By

View all
  • (2019)A cloud computing separation model based on information flowOpen Physics10.1515/phys-2019-001317:1(128-134)Online publication date: 11-Apr-2019
  • (2014)Sealed Containers in ZProceedings of the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 847710.1007/978-3-662-43652-3_12(136-141)Online publication date: 2-Jun-2014

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing
Formal Aspects of Computing  Volume 26, Issue 1
Jan 2014
192 pages
ISSN:0934-5043
EISSN:1433-299X
Issue’s Table of Contents

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 January 2014
Accepted: 20 April 2012
Revision received: 11 March 2012
Received: 14 October 2011
Published in FAC Volume 26, Issue 1

Author Tags

  1. Non-interference security
  2. Probabilistic non-interference
  3. Program semantics
  4. Program refinement

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)54
  • Downloads (Last 6 weeks)6
Reflects downloads up to 09 Jan 2025

Other Metrics

Citations

Cited By

View all
  • (2019)A cloud computing separation model based on information flowOpen Physics10.1515/phys-2019-001317:1(128-134)Online publication date: 11-Apr-2019
  • (2014)Sealed Containers in ZProceedings of the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 847710.1007/978-3-662-43652-3_12(136-141)Online publication date: 2-Jun-2014

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media