Trace equivalence and epistemic logic to express security properties. (English) Zbl 1511.68185
Gotsman, Alexey (ed.) et al., Formal techniques for distributed objects, components, and systems. 40th IFIP WG 6.1 international conference, FORTE 2020, held as part of the 15th international federated conference on distributed computing techniques, DisCoTec 2020, Valletta, Malta, June 15–19, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12136, 115-132 (2020).
Summary: In process algebra, we can express security properties using an equivalence on processes. However, it is not clear which equivalence is the most suitable for the purpose. Indeed, several definitions of some properties are proposed. For example, the definition of privacy is not unique. This situation means that we are not certain how to express an intuitive security notion. Namely, there is a gap between an intuitive security notion and the formulation. Proper formalization is essential for verification, and our purpose is to bridge this gap.
In the case of the applied pi calculus, an outputted message is not explicitly expressed. This feature suggests that trace equivalence appropriately expresses indistinguishability for attackers in the applied pi calculus. By chasing interchanging bound names and scope extrusions, we prove that trace equivalence is a congruence. Therefore, a security property expressed using trace equivalence is preserved by application of contexts.
Moreover, we construct an epistemic logic for the applied pi calculus. We show that its logical equivalence agrees with trace equivalence. It means that trace equivalence is suitable in the presence of a non-adaptive attacker. Besides, we define several security properties to use our epistemic logic.
For the entire collection see [Zbl 1496.68021].
In the case of the applied pi calculus, an outputted message is not explicitly expressed. This feature suggests that trace equivalence appropriately expresses indistinguishability for attackers in the applied pi calculus. By chasing interchanging bound names and scope extrusions, we prove that trace equivalence is a congruence. Therefore, a security property expressed using trace equivalence is preserved by application of contexts.
Moreover, we construct an epistemic logic for the applied pi calculus. We show that its logical equivalence agrees with trace equivalence. It means that trace equivalence is suitable in the presence of a non-adaptive attacker. Besides, we define several security properties to use our epistemic logic.
For the entire collection see [Zbl 1496.68021].
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 03B42 | Logics of knowledge and belief (including belief change) |
| 03B70 | Logic in computer science |
Software:
Modal_Logics_for_NTSReferences:
| [1] | Abadi, M., Blanchet, B., Fournet, C.: The applied pi calculus: mobile values, new names, and secure communication. J. ACM 65(1), 1-41 (2017). https://doi.org/10.1145/3127586 · Zbl 1426.68037 · doi:10.1145/3127586 |
| [2] | Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367(1-2), 2-32 (2006). https://doi.org/10.1016/j.tcs.2006.08.032 · Zbl 1153.94339 · doi:10.1016/j.tcs.2006.08.032 |
| [3] | Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. Inf. Comput. 148(1), 1-70 (1999). https://doi.org/10.1006/inco.1998.2740 · Zbl 0924.68073 · doi:10.1006/inco.1998.2740 |
| [4] | Alvim, M.S., Andrés, M.E., Palamidessi, C., van Rossum, P.: Safe equivalences for security properties. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IAICT, vol. 323, pp. 55-70. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15240-5_5 · Zbl 1202.68217 · doi:10.1007/978-3-642-15240-5_5 |
| [5] | Bernardo, M., De Nicola, R., Loreti, M.: Revisiting trace and testing equivalences for nondeterministic and probabilistic processes. Log. Methods Comput. Sci. 10(1) (2014). https://doi.org/10.2168/LMCS-10(1:16)2014 · Zbl 1325.68159 |
| [6] | Canetti, R., Cheung, L., Kaynar, D., Liskov, M., Lynch, N., Pereira, O., Segala, R.: Task-structured probabilistic i/o automata. J. Comput. Syst. Sci. 94, 63-97 (2018). https://doi.org/10.1016/j.jcss.2017.09.007 · Zbl 1390.68382 · doi:10.1016/j.jcss.2017.09.007 |
| [7] | Chadha, R., Delaune, S., Kremer, S.: Epistemic logic for the applied pi calculus. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS/FORTE -2009. LNCS, vol. 5522, pp. 182-197. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02138-1_12 · doi:10.1007/978-3-642-02138-1_12 |
| [8] | Chatzikokolakis, K., Palamidessi, C.: Making random choices invisible to the scheduler. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 42-58. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74407-8_4 · Zbl 1151.68517 · doi:10.1007/978-3-540-74407-8_4 |
| [9] | Cheval, V., Kremer, S., Rakotonirina, I.: DEEPSEC: deciding equivalence properties in security protocols theory and practice. In: SP 2018, pp. 529-546 (2018). https://doi.org/10.1109/SP.2018.00033 |
| [10] | Cheval, V., Cortier, V., Delaune, S.: Deciding equivalence-based properties using constraint solving. Theor. Comput. Sci. 492, 1-39 (2013). https://doi.org/10.1016/j.tcs.2013.04.016 · Zbl 1294.68111 · doi:10.1016/j.tcs.2013.04.016 |
| [11] | Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265-284. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54792-8_15 · doi:10.1007/978-3-642-54792-8_15 |
| [12] | Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157-1210 (2010). https://doi.org/10.3233/JCS-2009-0393 · doi:10.3233/JCS-2009-0393 |
| [13] | Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435-487 (2009). https://doi.org/10.3233/JCS-2009-0340 · Zbl 1284.68243 · doi:10.3233/JCS-2009-0340 |
| [14] | Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198-208 (1983). https://doi.org/10.1109/TIT.1983.1056650 · Zbl 0502.94005 · doi:10.1109/TIT.1983.1056650 |
| [15] | Eisentraut, C., Godskesen, J.C., Hermanns, H., Song, L., Zhang, L.: Probabilistic bisimulation for realistic schedulers. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 248-264. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19249-9_16 · Zbl 1427.68193 · doi:10.1007/978-3-319-19249-9_16 |
| [16] | Fiore, M., Abadi, M.: Computing symbolic models for verifying cryptographic protocols. In: CSFW-14, pp. 160-173 (2001). https://doi.org/10.1109/CSFW.2001.930144 |
| [17] | Giro, S., D’Argenio, P.: On the expressive power of schedulers in distributed probabilistic systems. Electron. Notes Theor. Comput. Sci. 253(3), 45-71 (2009). https://doi.org/10.1016/j.entcs.2009.10.005 · doi:10.1016/j.entcs.2009.10.005 |
| [18] | Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278-297. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039066 · doi:10.1007/BFb0039066 |
| [19] | 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). https://doi.org/10.1007/978-3-540-76637-7_12 · Zbl 1137.68448 · doi:10.1007/978-3-540-76637-7_12 |
| [20] | Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 299-309. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10003-2_79 · Zbl 0441.68018 · doi:10.1007/3-540-10003-2_79 |
| [21] | Horne, R.: A bisimilarity congruence for the applied pi-calculus sufficiently coarse to verify privacy properties. arXiv:1811.02536 (2018) |
| [22] | Knight, S., Mardare, R., Panangaden, P.: Combining epistemic logic and hennessy-milner logic. In: Constable, R.L., Silva, A. (eds.) Logic and Program Semantics. LNCS, vol. 7230, pp. 219-243. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29485-3_14 · Zbl 1354.68255 · doi:10.1007/978-3-642-29485-3_14 |
| [23] | Knight, S., Palamidessi, C., Panangaden, P., Valencia, F.D.: Spatial and epistemic modalities in constraint-based process calculi. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 317-332. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32940-1_23 · Zbl 1364.68290 · doi:10.1007/978-3-642-32940-1_23 |
| [24] | Mano, K.: Formal specification and verification of anonymity and privacy. Ph.D. thesis, Nagoya University (2013) |
| [25] | Mano, K., Kawabe, Y., Sakurada, H., Tsukada, Y.: Role interchange for anonymity and privacy of voting. J. Logic Comput. 20(6), 1251-1288 (2010). https://doi.org/10.1093/logcom/exq013 · Zbl 1213.68639 · doi:10.1093/logcom/exq013 |
| [26] | Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I. Inf. Comput. 100(1), 1-40 (1992). https://doi.org/10.1016/0890-5401(92)90008-4 · Zbl 0752.68036 · doi:10.1016/0890-5401(92)90008-4 |
| [27] | Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, II. Inf. Comput. 100(1), 41-77 (1992). https://doi.org/10.1016/0890-5401(92)90009-5 · Zbl 0752.68037 · doi:10.1016/0890-5401(92)90009-5 |
| [28] | Minami, K.: Trace equivalence and epistemic logic to express security properties. arXiv:1903.03719 (2019) |
| [29] | Parrow, J., Borgström, J., Eriksson, L.H., Gutkovas, R., Weber, T.: Modal logics for nominal transition systems. In: CONCUR 2015. LIPIcs, vol. 42, pp. 198-211. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015). https://doi.org/10.4230/LIPIcs.CONCUR.2015.198 · Zbl 1374.68339 |
| [30] | Segala, R.: A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 234-248. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60218-6_17 · doi:10.1007/3-540-60218-6_17 |
| [31] | Toninho, B., Caires, L.: A spatial-epistemic logic for reasoning about security protocols. In: SecCo 2010. EPTCS, vol. 51, pp. 1-15. Open Publishing Association (2011). https://doi.org/10.4204/EPTCS.51.1 |
| [32] | Tsukada, Y., Sakurada, H., Mano, K., Manabe, Y.: On compositional reasoning about anonymity and privacy in epistemic logic. Ann. Math. Artif. Intell. 78(2), 101-129 (2016). https://doi.org/10.1007/s10472-016-9516-8 · Zbl 1403.03051 · doi:10.1007/s10472-016-9516-8 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
