Skip to main content

2017 | Supplement | Buchkapitel

Modular Verification of Protocol Equivalence in the Presence of Randomness

verfasst von : Matthew S. Bauer, Rohit Chadha, Mahesh Viswanathan

Erschienen in: Computer Security – ESORICS 2017

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

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!

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!

Literatur
1.
Zurück zum Zitat Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. ACM SIGPLAN Not. 36(3), 104–115 (2001)CrossRefMATH Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. ACM SIGPLAN Not. 36(3), 104–115 (2001)CrossRefMATH
2.
Zurück zum Zitat 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 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
3.
Zurück zum Zitat 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.: Verifying privacy-type properties in a modular way. In: CSF, pp. 95–109 (2012)
4.
Zurück zum Zitat 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., 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
5.
Zurück zum Zitat 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., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: CSF, pp. 107–121 (2010)
6.
Zurück zum Zitat 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 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
7.
Zurück zum Zitat Basin, D., Dreier, J., Sasse, R.: Automated symbolic proofs of observational equivalence. In: CCS, pp. 1144–1155 (2015) Basin, D., Dreier, J., Sasse, R.: Automated symbolic proofs of observational equivalence. In: CCS, pp. 1144–1155 (2015)
8.
Zurück zum Zitat Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: CCS, pp. 16–25 (2005) Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: CCS, pp. 16–25 (2005)
10.
Zurück zum Zitat 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 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.
Zurück zum Zitat 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 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.
Zurück zum Zitat Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: LICS, pp. 331–340 (2005) Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: LICS, pp. 331–340 (2005)
13.
Zurück zum Zitat Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: FOCS, pp. 136–145 (2001) Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: FOCS, pp. 136–145 (2001)
14.
Zurück zum Zitat 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) 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.
Zurück zum Zitat 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 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.
Zurück zum Zitat Chadha, R., Sistla, A., Viswanathan, M.: Model checking concurrent programs with nondeterminism and randomization. In: FSTTCS, pp. 364–375 (2010) Chadha, R., Sistla, A., Viswanathan, M.: Model checking concurrent programs with nondeterminism and randomization. In: FSTTCS, pp. 364–375 (2010)
17.
Zurück zum Zitat Chadha, R., Sistla, A.P., Viswanathan, M.: Verification of randomized security protocols. In: LICS (2017) Chadha, R., Sistla, A.P., Viswanathan, M.: Verification of randomized security protocols. In: LICS (2017)
18.
19.
Zurück zum Zitat Chaum, D.: The dining cryptographers problem: unconditional sender and recipient untraceability. J. Cryptology 1(1), 65–75 (1988)MathSciNetCrossRefMATH Chaum, D.: The dining cryptographers problem: unconditional sender and recipient untraceability. J. Cryptology 1(1), 65–75 (1988)MathSciNetCrossRefMATH
20.
Zurück zum Zitat Chaum, D.L.: Untraceable electronic mail, return addresses, and digital pseudonyms. Commun. ACM 24(2), 84–90 (1981)CrossRef Chaum, D.L.: Untraceable electronic mail, return addresses, and digital pseudonyms. Commun. ACM 24(2), 84–90 (1981)CrossRef
21.
Zurück zum Zitat Cheung, L.: Reconciling nondeterministic and probabilistic choices. Ph.D. thesis, Radboud University of Nijmegen (2006) Cheung, L.: Reconciling nondeterministic and probabilistic choices. Ph.D. thesis, Radboud University of Nijmegen (2006)
22.
Zurück zum Zitat Chevalier, C., Delaune, S., Kremer, S.: Transforming password protocols to compose. In: FSTTCS, pp. 204–216 (2011) Chevalier, C., Delaune, S., Kremer, S.: Transforming password protocols to compose. In: FSTTCS, pp. 204–216 (2011)
23.
Zurück zum Zitat Chevalier, Y., Rusinowitch, M.: Decidability of equivalence of symbolic derivations. J. Autom. Reasoning 48, 263–292 (2010)MathSciNetCrossRefMATH Chevalier, Y., Rusinowitch, M.: Decidability of equivalence of symbolic derivations. J. Autom. Reasoning 48, 263–292 (2010)MathSciNetCrossRefMATH
24.
25.
Zurück zum Zitat Cortier, V., Delaune, S.: A method for proving observational equivalence. In: CSF, pp. 266–276 (2009) Cortier, V., Delaune, S.: A method for proving observational equivalence. In: CSF, pp. 266–276 (2009)
26.
Zurück zum Zitat Cortier, V., Delaune, S.: Safely composing security protocols. Formal Methods Syst. Des. 34(1), 1–36 (2009)CrossRefMATH Cortier, V., Delaune, S.: Safely composing security protocols. Formal Methods Syst. Des. 34(1), 1–36 (2009)CrossRefMATH
27.
Zurück zum Zitat Ciobâcă, Ş., Cortier, V.: Protocol composition for arbitrary primitives. In: CSF, pp. 322–336 (2010) Ciobâcă, Ş., Cortier, V.: Protocol composition for arbitrary primitives. In: CSF, pp. 322–336 (2010)
28.
Zurück zum Zitat 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 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.
Zurück zum Zitat de Alfaro, L.: The verification of probabilistic systems under memoryless partial information policies is hard. In: PROBMIV (1999) de Alfaro, L.: The verification of probabilistic systems under memoryless partial information policies is hard. In: PROBMIV (1999)
30.
Zurück zum Zitat Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435–487 (2009)CrossRefMATH Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435–487 (2009)CrossRefMATH
31.
Zurück zum Zitat Delaune, S., Kremer, S., Ryan, M.D.: Composition of password-based protocols. In: CSF, pp. 239–251 (2008) Delaune, S., Kremer, S., Ryan, M.D.: Composition of password-based protocols. In: CSF, pp. 239–251 (2008)
32.
Zurück zum Zitat Dingledine, R., Mathewson, N., Syverson, P.: Tor: the second-generation onion router. Technical report, DTIC Document (2004) Dingledine, R., Mathewson, N., Syverson, P.: Tor: the second-generation onion router. Technical report, DTIC Document (2004)
34.
Zurück zum Zitat 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 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.
Zurück zum Zitat Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties, pp. 1–50 (2009) Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties, pp. 1–50 (2009)
36.
37.
Zurück zum Zitat Garcia, F., van Rossum, P., Sokolova, A.: Probabilistic Anonymity and Admissible Schedulers. CoRR, abs/0706.1019 (2007) Garcia, F., van Rossum, P., Sokolova, A.: Probabilistic Anonymity and Admissible Schedulers. CoRR, abs/0706.1019 (2007)
38.
39.
40.
Zurück zum Zitat Gunter, C.A., Khanna, S., Tan, K., Venkatesh, S.S.: Dos protection for reliably authenticated broadcast. In: NDSS (2004) Gunter, C.A., Khanna, S., Tan, K., Venkatesh, S.S.: Dos protection for reliably authenticated broadcast. In: NDSS (2004)
41.
Zurück zum Zitat Guttman, J.D.: Authentication tests and disjoint encryption: a design method for security protocols. J. Comput. Secur. 12(3–4), 409–433 (2004)CrossRef Guttman, J.D.: Authentication tests and disjoint encryption: a design method for security protocols. J. Comput. Secur. 12(3–4), 409–433 (2004)CrossRef
43.
Zurück zum Zitat 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) 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.
Zurück zum Zitat Hirschi, L., Baelde, D., Delaune, S.: A method for verifying privacy-type properties: the unbounded case. In: SP, pp. 564–581 (2016) Hirschi, L., Baelde, D., Delaune, S.: A method for verifying privacy-type properties: the unbounded case. In: SP, pp. 564–581 (2016)
45.
Zurück zum Zitat Hoare, C.A.R.: Communicating Sequential Processes, vol. 178 (1985) Hoare, C.A.R.: Communicating Sequential Processes, vol. 178 (1985)
46.
Zurück zum Zitat 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) 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.
Zurück zum Zitat Meadows, C.: Formal methods for cryptographic protocol analysis: emerging issues and trends. IEEE J. Sel. Areas Commun. 21(1), 44–54 (2003)CrossRef Meadows, C.: Formal methods for cryptographic protocol analysis: emerging issues and trends. IEEE J. Sel. Areas Commun. 21(1), 44–54 (2003)CrossRef
48.
Zurück zum Zitat 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 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.
Zurück zum Zitat Mödersheim, S., Viganò, L.: Sufficient conditions for vertical composition of security protocols. In: CCS, pp. 435–446 (2014) Mödersheim, S., Viganò, L.: Sufficient conditions for vertical composition of security protocols. In: CCS, pp. 435–446 (2014)
50.
Zurück zum Zitat 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 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.
Zurück zum Zitat Reiter, M.K., Rubin, A.D.: Crowds: anonymity for web transactions. TISSEC 1(1), 66–92 (1998)CrossRef Reiter, M.K., Rubin, A.D.: Crowds: anonymity for web transactions. TISSEC 1(1), 66–92 (1998)CrossRef
52.
Zurück zum Zitat Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: CSFW, pp. 174–190 (2001) Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: CSFW, pp. 174–190 (2001)
53.
Zurück zum Zitat 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 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.
Zurück zum Zitat Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of diffie-hellman protocols and advanced security properties. In: CSF, pp. 78–94 (2012) 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.
Zurück zum Zitat 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 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.
Zurück zum Zitat Shmatikov, V.: Probabilistic analysis of an anonymity system. J. Comput. Secur. 12(3–4), 355–377 (2004)CrossRefMATH Shmatikov, V.: Probabilistic analysis of an anonymity system. J. Comput. Secur. 12(3–4), 355–377 (2004)CrossRefMATH
Metadaten
Titel
Modular Verification of Protocol Equivalence in the Presence of Randomness
verfasst von
Matthew S. Bauer
Rohit Chadha
Mahesh Viswanathan
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-66402-6_12