Abstract
We present G2C, a goal-driven specification language for distributed applications. This language offers support for the declarative specification of functionality goals and security properties. The former comprise the parties, their inputs, and the goal of the communication protocol. The latter comprise secrecy, access control, and anonymity requirements. A key feature of our language is that it abstracts away from how the intended functionality is achieved, but instead lets the system designer concentrate on which functional features and security properties should be achieved. Our framework provides a compilation method for transforming G2C specifications into symbolic cryptographic protocols, which are shown to be optimal. We provide a technique to automatically verify the correctness and security of these protocols using ProVerif, a state-of-the-art automated theorem-prover for cryptographic protocols. We have implemented a G2C compiler to demonstrate the feasibility of our approach.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Fournet, C.: Mobile Values, New Names, and Secure Communication. In: POPL 2001 (2001)
Abadi, M., Gordon, A.D.: A Calculus for Cryptographic Protocols: The Spi Calculus. In: CCS 1997. ACM, New York (1997)
Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Trans. Softw. Eng. 22(1) (1996)
Backes, M., Grochulla, M.P., Hriţcu, C., Maffei, M.: Achieving security despite compromise using zero-knowledge. In: CSF 2009. IEEE, Los Alamitos (2009)
Barth, A., Datta, A., Mitchell, J.C., Nissenbaum, H.: Privacy and Contextual Integrity: Framework and Applications. In: SP 2006. IEEE, Los Alamitos (2006)
Bhargavan, K., Corin, R., Deniélou, P.-M., Fournet, C., Leifer, J.J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: CSF 2009. IEEE, Los Alamitos (2009)
Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW 2001 (2001)
Bleichenbacher, D.: Chosen ciphertext attacks against protocols based on the RSA encryption standard PKCS. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol. 1462, pp. 1–12. Springer, Heidelberg (1998)
Boneh, D., Gentry, C., Waters, B.: Collusion resistant broadcast encryption with short ciphertexts and private keys. In: Shoup, V. (ed.) CRYPTO 2005. LNCS, vol. 3621, pp. 258–275. Springer, Heidelberg (2005)
Boneh, D., Waters, B.: A fully collusion resistant broadcast, trace, and revoke system. In: CCS 2006. ACM, New York (2006)
Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A., Walstad, C.: Formal analysis of Kerberos 5. Theoretical Computer Science, 367(1) (2006)
Chandran, N., Groth, J., Sahai, A.: Ring signatures of sub-linear size without random oracles. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 423–434. Springer, Heidelberg (2007)
Chen, W., Clarke, L., Kurose, J., Towsley, D.: Optimizing cost-sensitive trust-negotiation protocols. In: INFOCOM 2005, pp. 1431–1442. IEEE, Los Alamitos (2005)
Chong, S., Liu, J., Myers, A.C., Qi, X., Vikram, K., Zheng, L., Zheng, X.: Secure web applications via automatic partitioning. SIGOPS Operating System Review 41 (2007)
Ciriani, V., De Capitani di Vimercati, S., Foresti, S., Samarati, P.: k-Anonymity. Secure Data Management in Decentralized Systems 33 (2007)
Corin, R., Deniélou, P.-M.: A protocol compiler for secure sessions in ml. In: Barthe, G., Fournet, C. (eds.) TGC 2007. LNCS, vol. 4912, pp. 276–293. Springer, Heidelberg (2008)
Corin, R., Deniélou, P.-M., Fournet, C., Bhargavan, K., Leifer, J.: Secure implementations for typed session abstractions. In: CSF 2007 (2007)
Denning, D.E.: A Lattice Model of Secure Information Flow. Communications of the ACM 19(5) (1976)
Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Communications of the ACM 24(8) (1981)
Fiat, A., Naor, M.: Broadcast encryption. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol. 773, pp. 480–491. Springer, Heidelberg (1994)
Fisher, D.: Millions of .Net Passport accounts put at risk. eWeek (2003)
Fournet, C., Guernic, G.L., Rezk, T.: A security-preserving compiler for distributed programs: From information-flow policies to cryptographic mechanisms. In: CCS 2009. ACM, New York (2009)
G2C website (2011), http://www.infsec.cs.uni-saarland.de/~reischuk/g2c/
Gecode: generic constraint development environment (2011), http://www.gecode.org
Ghallab, M., Nau, D., Traverso, P.: Automated Planning: Theory and Practice. Morgan Kaufmann, San Francisco (2004)
Herranz, J.: Identity-based ring signatures from RSA. Theoretical Computer Science 389 (2007)
Jia, L., Vaughan, J.A., Mazurak, K., Zhao, J., Zarko, L., Schorr, J., Zdancewic, S.: AURA: A Programming Language for Authorization and Audit. In: ICFP 2008, ACM, New York (2008)
Liu, J., George, M.D., Vikram, K., Qi, X., Waye, L., Myers, A.C.: Fabric: A platform for secure distributed computation and storage. In: SOSP 2009. ACM, New York (2009)
Loo, B.T., Condie, T., Garofalakis, M., Gay, D.E., Hellerstein, J.M., Maniatis, P., Ramakrishnan, R., Roscoe, T., Stoica, I.: Declarative Networking: Language, Execution and Optimization. In: SIGMOD 2006. ACM, New York (2006)
Loo, B.T., Condie, T., Hellerstein, J.M., Maniatis, P., Roscoe, T., Stoica, I.: Implementing Declarative Overlays. In: Herbert, A., Birman, K.P. (eds.) SOSP 2005. ACM, New York (2005)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Milner, R.: Communicating and Mobile Systems: The Pi-Calculus. Cambridge University Press, Cambridge (1999)
Myers, A., Liskov, B.: Protecting privacy using the decentralized label model. ACM Transactions on Software Engineering and Methodology (2000)
Navarro, J.A., Rybalchenko, A.: Operational semantics for declarative networking. In: Gill, A., Swift, T. (eds.) PADL 2009. LNCS, vol. 5418, pp. 76–90. Springer, Heidelberg (2008)
Necula, G.C.: Translation validation for an optimizing compiler. ACM SIGPLAN Notices 35(5) (2000)
Ocenasek, P., Sveda, M.: An approach to automated design of security protocols. In: ICMLS 2006 (2006)
Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998)
Rivest, R.L., Shamir, A., Tauman, Y.: How to leak a secret. Communications of the ACM 22(22) (2001)
Sabelfeld, A., Myers, A.C.: Language-Based Information Flow Security. IEEE Journal on Selected Area in Communications 21(1) (2003)
Sprenger, C., Basin, D.: Developing security protocols by refinement. In: CCS 2010. ACM, New York (2010)
Sweeney, L.: k-anonymity: a model for protecting privacy. International Journal on Uncertainty, Fuzziness and Knowledge-based Systems 10(5) (2002)
Tristan, J.-B., Leroy, X.: Formal verification of translation validators: A case study on instruction scheduling optimizations. In: POPL 1908. ACM, New York (2008)
US Depart. of Health & Human Services. The Health Insurance Portability and Accountability Act of 1996 Privacy Rule (2009), http://www.hhs.gov/ocr/privacy
Vaughan, J.A.: A confidentiality extension to the Aura programming language. In: TLDI 2011. ACM, New York (2011)
Volpano, D., Smith, G., Irvine, C.: A Sound Type System for Secure Flow Analysis. Journal of Computer Security 4(2-3) (1996)
Wagner, D., Schneier, B.: Analysis of the SSL 3.0 protocol. In: EC 1996 (1996)
Xue, H., Zhang, H., Qing, S.: A schema of automated design security protocols. In: CISW 2007 (2007)
Zhou, W., Mao, Y., Loo, B.T., Abadi, M.: Unified Declarative Platform for Secure Networked Information Systems. In: ICDE 2009. IEEE, Los Alamitos (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Backes, M., Maffei, M., Pecina, K., Reischuk, R.M. (2012). G2C: Cryptographic Protocols from Goal-Driven Specifications. In: Mödersheim, S., Palamidessi, C. (eds) Theory of Security and Applications. TOSCA 2011. Lecture Notes in Computer Science, vol 6993. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27375-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-27375-9_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27374-2
Online ISBN: 978-3-642-27375-9
eBook Packages: Computer ScienceComputer Science (R0)