Compositional refinement in agent-based security protocols
Tóm tắt
A truly secure protocol is one which never violates its security requirements, no matter how bizarre the circumstances, provided those circumstances are within its terms of reference. Such cast-iron guarantees, as far as they are possible, require formal, rigorous techniques: proof or model-checking. Informally, they are difficult or impossible to achieve. Our rigorous technique is refinement, until recently not much applied to security. We argue its benefits by using refinement-based program algebra to develop several security case studies. That is one of our contributions here. The soundness of the technique follows from its compositional semantics, one which we defined (elsewhere) to support a specialisation of standard refinement by enriching standard semantics with information that tracks correlations between hidden state and visible behaviour. A further contribution is to extend the basic theory of secure refinement (Morgan in Mathematics of program construction, Springer, Berlin, vol. 4014, pp. 359–378, 2006) with special features required by our case studies, namely agent-based systems with complementary security requirements, and looping programs.
Tài liệu tham khảo
Amtoft T, Banerjee A (2004) Information flow analysis in logical form. In: Proceedings of the static analysis symposium. LNCS, vol 3148. Springer, Berlin (awarded Best Paper)
Alur R, Černý P, Zdancewic S (2006) Preserving secrecy under refinement. In: ICALP ’06: proceedings (part II) of the 33rd international colloquium on automata, languages and programming. Springer, Berlin, pp 107–118
Abramsky S, Jung A (1994) Domain theory. In: Abramsky S, Gabbay DM, Maibaum TSE (eds) Handbook of logic and computer science, vol 3. Oxford Science Publications, Oxford, pp 1–168
Bogetoft P, Christensen DL, Damgård I, Geisler M, Jakobsen T, Krøigaard M, Nielsen JD, Nielsen JB, Nielsen K, Pagter J, Schwartzbach M, Toft T (2010) Secure multiparty computation goes live. http://eprint.iacr.org/2008/068
Bossi A, Focardi R, Piazza C, Rossi S (2003) Refinement operators and information flow security. In: SEFM, IEEE, pp 44–53
Cerny P (2009) Private communication
Coble A (2008) Formalized information-theoretic proofs of privacy using the HOL-4 theorem-prover. In: Privacy enhancing technologies symposium (to appear)
Dijkstra EW (1976) A discipline of programming. Prentice-Hall, Englewood Cliffs
Engelhardt K, van der Meyden R, Moses Y (2001) A refinement theory that supports reasoning about knowledge and time. In: Nieuwenhuis R, Voronkov A (eds) LPAR. Lecture notes in computer science, vol 2250. Springer, Berlin, pp 125–141
Gordon AD, Abadi M (1997) A calculus for cryptographic protocols: the Spi calculus. In: Proceedings of the ACM conference on computer and communications security
Goguen JA, Meseguer J (1984) Unwinding and inference control. In: Proceedings of the IEEE symposium on security and privacy. IEEE Computer Society, pp 75–86
Hoare CAR (1985) A couple of novelties in the propositional calculus. Z Math Logik Grundlagen Math 31(2): 173–178
Leino KRM, Joshi R (2000) A semantic approach to secure information flow. Sci Comput Program 37(1–3): 113–138
Mantel H (2001) Preserving information flow properties under refinement. In: Proceedings of the IEEE symposium on security and privacy, pp 78–91
McIver AK, Cohen E, Morgan C, Gonzalia C (2008) Using probabilistic Kleene algebra pKA for protocol verification. J Logic Algebr Program 76(1): 90–111
Murray T, Lowe G (2009) On refinement-closed security properties and nondeterminism. In: Proceedings of the AVoCS. ENTCS 250(2):49–68
McIver AK, Morgan CC (2008) A calculus of revelations. Presented at VSTTE theories workshop. http://www.cs.york.ac.uk/vstte08/
McIver AK, Morgan CC (2009) Sums and lovers: case studies in security, compositionality and refinement. In: Cavalcanti A, Dams D (eds) Proceedings of the FM ’09. LNCS, vol 5850. Springer, Berlin
McIver AK, Morgan CC (2010) The thousand-and-one cryptographers. In: Jones CB, Roscoe AW, Wood KR (eds) Reflections on the work of C.A.R. Hoare. Springer, Berlin
McIver AK, Meinicke LA, Morgan CC (2010) Compositional closure for Bayes risk in probabilistic noninterference. In: Abramsky S, Gavoille C, Kirchner C, auf der Heide FM, Spiraki PG (eds) Proceedings of the ICALP 2010. LNCS, vol 6199, pp 223–235 (extended abstract)
Malkhi D, Nisan N, Pinkas B, Sella Y (2004) Fairplay—a secure two-party computation system. In: Proceedings of the 13th conference on USENIX security symposium. USENIX Association
Morgan CC (1994) Programming from specifications, 2nd edn. Prentice-Hall, Englewood Cliffs. http://web.comlab.ox.ac.uk/oucl/publications/books/PfS/
Morgan CC (2006) The shadow knows: refinement of ignorance in sequential programs. In: Uustalu T (ed) Mathematics of program construction, vol 4014. Springer, Berlin, pp 359–378
Morgan CC (2009) The shadow knows: refinement of ignorance in sequential programs. Sci Comput Program 74(8): 629–653
Naumann DA, Banerjee A, Rosenberg S (2007) Towards a logical account of declassification. In: Proceedings of the workshop on programming languages and analysis for security, pp 61–66
Paulson LC (1998) The inductive approach to verifying cryptographic protocols. J Comput Secur 6: 85–128
Pironti A, Sisto R (2008) Formally sound refinement of Spi calculus protocol specifications into Java code. In: IEEE high assurance systems engineering symposium
Rabin MO (1981) How to exchange secrets by oblivious transfer. Technical Report TR-81, Harvard University. eprint.iacr.org/2005/187
Rivest R (1999) Unconditionally secure commitment and oblivious transfer schemes using private channels and a trusted initialiser. Technical report, M.I.T. http://theory.lcs.mit.edu/~rivest/Rivest-commitment.pdf
Ryan P, Schneider S, Goldsmith M, Lowe G, Roscoe B (2000) Modelling and analysis of security protocols. Addison-Wesley, Reading
Schoenmakers B (2010) Cryptography lecture notes. http://www.win.tue.nl/~berry/2WC13/LectureNotes.pdf
Smyth MB (1978) Power domains. J Comput Syst Sci 16: 23–36
Sabelfeld A, Sands D (2001) A PER model of secure information flow. High Order Symb Comput 14(1): 59–91
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