Top

Published in:

2017 | Supplement | Chapter

Modular Verification of Protocol Equivalence in the Presence of Randomness

Authors : Matthew S. Bauer, Rohit Chadha, Mahesh Viswanathan

Published in: Computer Security – ESORICS 2017

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Security protocols that provide privacy and anonymity guarantees are growing increasingly prevalent in the online world. The highly intricate nature of these protocols makes them vulnerable to subtle design flaws. Formal methods have been successfully deployed to detect these errors, where protocol correctness is formulated as a notion of equivalence (indistinguishably). The high overhead for verifying such equivalence properties, in conjunction with the fact that protocols are never run in isolation, has created a need for modular verification techniques. Existing approaches in formal modeling and (compositional) verification of protocols for privacy have abstracted away a fundamental ingredient in the effectiveness of these protocols, randomness. We present the first composition results for equivalence properties of protocols that are explicitly able to toss coins. Our results hold even when protocols share data (such as long term keys) provided that protocol messages are tagged with the information of which protocol they belong to.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter MTD CBITS: Moving Target Defense for Cloud-Based IT Systems

next chapter Non-interactive Provably Secure Attestations for Arbitrary RSA Prime Generation Algorithms

Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. ACM SIGPLAN Not. 36(3), 104–115 (2001)CrossRefMATH

Andova, S., Cremers, C.J.F., Gjøsteen, K., Mauw, S., Mjølsnes, S.F., Radomirovic, S.: A framework for compositional verification of security protocols. Inf. Comput. 206(2–4), 425–459 (2008)MathSciNetCrossRefMATH

Arapinis, M., Cheval, V., Delaune, S.: Verifying privacy-type properties in a modular way. In: CSF, pp. 95–109 (2012)

Arapinis, M., Cheval, V., Delaune, S.: Composing security protocols: from confidentiality to privacy. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 324–343. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46666-7_17

Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: CSF, pp. 107–121 (2010)

Arapinis, M., Delaune, S., Kremer, S.: From one session to many: dynamic tags for security protocols. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 128–142. Springer, Heidelberg (2008). doi:10.1007/978-3-540-89439-1_9 CrossRef

Basin, D., Dreier, J., Sasse, R.: Automated symbolic proofs of observational equivalence. In: CCS, pp. 1144–1155 (2015)

Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: CCS, pp. 16–25 (2005)

Bauer, M.S., Chadha, R., Viswanathan, M.: Modular verification of protocol equivalence in the presence of randomness. http://hdl.handle.net/2142/96261

10.

Bauer, M.S., Chadha, R., Viswanathan, M.: Composing protocols with randomized actions. In: Piessens, F., Viganò, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 189–210. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49635-0_10 CrossRef

11.

Ben-Or, M., Goldreich, O., Micali, S., Rivest, R.L.: A fair protocol for signing contracts. IEEE Trans. Inf. Theor. 36(1), 40–46 (1990)MathSciNetCrossRef

12.

Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: LICS, pp. 331–340 (2005)

13.

Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: FOCS, pp. 136–145 (2001)

14.

Canetti, R., Cheung, L., Kaynar, D., Liskov, M., Lynch, N., Pereira, P., Segala, R.: Task-structured probabilistic I/O automata. In: Workshop on Discrete Event Systems (2006)

15.

Canetti, R., Herzog, J.: Universally composable symbolic analysis of mutual authentication and key-exchange protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 380–403. Springer, Heidelberg (2006). doi:10.1007/11681878_20 CrossRef

16.

Chadha, R., Sistla, A., Viswanathan, M.: Model checking concurrent programs with nondeterminism and randomization. In: FSTTCS, pp. 364–375 (2010)

17.

Chadha, R., Sistla, A.P., Viswanathan, M.: Verification of randomized security protocols. In: LICS (2017)

18.

Chatzikokolakis, K., Palamidessi, C.: Making random choices invisible to the scheduler. Inf. Comput. 208, 694–715 (2010)MathSciNetCrossRefMATH

19.

Chaum, D.: The dining cryptographers problem: unconditional sender and recipient untraceability. J. Cryptology 1(1), 65–75 (1988)MathSciNetCrossRefMATH

20.

Chaum, D.L.: Untraceable electronic mail, return addresses, and digital pseudonyms. Commun. ACM 24(2), 84–90 (1981)CrossRef

21.

Cheung, L.: Reconciling nondeterministic and probabilistic choices. Ph.D. thesis, Radboud University of Nijmegen (2006)

22.

Chevalier, C., Delaune, S., Kremer, S.: Transforming password protocols to compose. In: FSTTCS, pp. 204–216 (2011)

23.

Chevalier, Y., Rusinowitch, M.: Decidability of equivalence of symbolic derivations. J. Autom. Reasoning 48, 263–292 (2010)MathSciNetCrossRefMATH

24.

Cortier, V., Delaitre, J., Delaune, S.: Safely composing security protocols. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 352–363. Springer, Heidelberg (2007). doi:10.1007/978-3-540-77050-3_29 CrossRef

25.

Cortier, V., Delaune, S.: A method for proving observational equivalence. In: CSF, pp. 266–276 (2009)

26.

Cortier, V., Delaune, S.: Safely composing security protocols. Formal Methods Syst. Des. 34(1), 1–36 (2009)CrossRefMATH

27.

Ciobâcă, Ş., Cortier, V.: Protocol composition for arbitrary primitives. In: CSF, pp. 322–336 (2010)

28.

Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositional logic for security protocols. J. Comput. Secur. 13(3), 423–482 (2005)CrossRef

29.

de Alfaro, L.: The verification of probabilistic systems under memoryless partial information policies is hard. In: PROBMIV (1999)

30.

Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435–487 (2009)CrossRefMATH

31.

Delaune, S., Kremer, S., Ryan, M.D.: Composition of password-based protocols. In: CSF, pp. 239–251 (2008)

32.

Dingledine, R., Mathewson, N., Syverson, P.: Tor: the second-generation onion router. Technical report, DTIC Document (2004)

33.

Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theor. 29(2), 198–208 (1983)MathSciNetCrossRefMATH

34.

Dreier, J., Duménil, C., Kremer, S., Sasse, R.: Beyond subterm-convergent equational theories in automated verification of stateful protocols. In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 117–140. Springer, Heidelberg (2017). doi:10.1007/978-3-662-54455-6_6 CrossRef

35.

Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties, pp. 1–50 (2009)

36.

Even, S., Goldreich, O., Lempel, A.: A randomized protocol for signing contracts. Commun. ACM 28(6), 637–647 (1985)MathSciNetCrossRefMATH

37.

Garcia, F., van Rossum, P., Sokolova, A.: Probabilistic Anonymity and Admissible Schedulers. CoRR, abs/0706.1019 (2007)

38.

Goldschlag, D.M., Reed, M.G., Syverson, P.F.: Hiding routing information. In: Anderson, R. (ed.) IH 1996. LNCS, vol. 1174, pp. 137–150. Springer, Heidelberg (1996). doi:10.1007/3-540-61996-8_37 CrossRef

39.

Goubault-Larrecq, J., Palamidessi, C., Troina, A.: A probabilistic applied Pi–calculus. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 175–190. Springer, Heidelberg (2007). doi:10.1007/978-3-540-76637-7_12 CrossRef

40.

Gunter, C.A., Khanna, S., Tan, K., Venkatesh, S.S.: Dos protection for reliably authenticated broadcast. In: NDSS (2004)

41.

Guttman, J.D.: Authentication tests and disjoint encryption: a design method for security protocols. J. Comput. Secur. 12(3–4), 409–433 (2004)CrossRef

42.

Guttman, J.D.: Cryptographic protocol composition via the authentication tests. In: Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 303–317. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00596-1_22 CrossRef

43.

He, C., Sundararajan, M., Datta, A., Derek, A., Mitchell, J.C.: A modular correctness proof of IEEE 802.11i and TLS. In: CCS, pp. 2–15 (2005)

44.

Hirschi, L., Baelde, D., Delaune, S.: A method for verifying privacy-type properties: the unbounded case. In: SP, pp. 564–581 (2016)

45.

Hoare, C.A.R.: Communicating Sequential Processes, vol. 178 (1985)

46.

Kwiatkowska, M., Norman, G., Parker, D.: Prism: probabilistic symbolic model checker. In: International Conference on Modelling Techniques and Tools for Computer Performance Evaluation, pp. 200–204 (2002)

47.

Meadows, C.: Formal methods for cryptographic protocol analysis: emerging issues and trends. IEEE J. Sel. Areas Commun. 21(1), 44–54 (2003)CrossRef

48.

Meadows, C.: Emerging issues and trends in formal methods in cryptographic protocol analysis: twelve years later. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 475–492. Springer, Cham (2015). doi:10.1007/978-3-319-23165-5_22 CrossRef

49.

Mödersheim, S., Viganò, L.: Sufficient conditions for vertical composition of security protocols. In: CCS, pp. 435–446 (2014)

50.

Pfitzmann, B., Pfitzmann, A.: How to break the direct RSA-implementation of mixes. In: Quisquater, J.-J., Vandewalle, J. (eds.) EUROCRYPT 1989. LNCS, vol. 434, pp. 373–381. Springer, Heidelberg (1990). doi:10.1007/3-540-46885-4_37 CrossRef

51.

Reiter, M.K., Rubin, A.D.: Crowds: anonymity for web transactions. TISSEC 1(1), 66–92 (1998)CrossRef

52.

Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: CSFW, pp. 174–190 (2001)

53.

Ryan, P.Y.A., Bismark, D., Heather, J., Schneider, S., Xia, Z.: Prêt à voter: a voter-verifiable voting system. IEEE Trans. Inf. Forensics Secur. 4(4), 662–673 (2009)CrossRef

54.

Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of diffie-hellman protocols and advanced security properties. In: CSF, pp. 78–94 (2012)

55.

Schneider, S., Sidiropoulos, A.: CSP and anonymity. In: Bertino, E., Kurth, H., Martella, G., Montolivo, E. (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 198–218. Springer, Heidelberg (1996). doi:10.1007/3-540-61770-1_38 CrossRef

56.

Shmatikov, V.: Probabilistic analysis of an anonymity system. J. Comput. Secur. 12(3–4), 355–377 (2004)CrossRefMATH

Title: Modular Verification of Protocol Equivalence in the Presence of Randomness
Authors: Matthew S. Bauer
Rohit Chadha
Mahesh Viswanathan
Publisher: Springer International Publishing
Book: Computer Security – ESORICS 2017
Print ISBN: 978-3-319-66401-9

Electronic ISBN: 978-3-319-66402-6

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-66402-6_12

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner