×

zbMATH — the first resource for mathematics

A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols. (English) Zbl 1359.68023
Summary: Cryptographic protocols aim at securing communications over insecure networks such as the Internet, where dishonest users may listen to communications and interfere with them. A secure communication has a different meaning depending on the underlying application. It ranges from the confidentiality of a data to e.g. verifiability in electronic voting systems. Another example of a security notion is privacy.
Formal symbolic models have proved their usefulness for analysing the security of protocols. Until quite recently, most results focused on trace properties like confidentiality or authentication. There are however several security properties, which cannot be defined (or cannot be naturally defined) as trace properties and require a notion of behavioural equivalence. Typical examples are anonymity, and privacy related properties. During the last decade, several results and verification tools have been developed to analyse equivalence-based security properties.
We propose here a synthesis of decidability and undecidability results for equivalence-based security properties. Moreover, we give an overview of existing verification tools that may be used to verify equivalence-based security properties.
MSC:
68M12 Network protocols
94A60 Cryptography
Software:
Akiss; Apte; FAST; LALBLC; TAMARIN; YAPA
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Dolev, D.; Yao, A. C., On the security of public key protocols, (Proc. 22nd Symposium on Foundations of Computer Science, FCS’81, (1981), IEEE Computer Society Press), 350-357
[2] Blanchet, B., A computationally sound mechanized prover for security protocols, (Proc. Symposium on Security and Privacy, S&P’06, (2006), IEEE Computer Society Press), 140-154
[3] Abadi, M.; Rogaway, P., Reconciling two views of cryptography (the computational soundness of formal encryption), (Proc. International Conference on Theoretical Computer Science, (2000)), 3-22 · Zbl 1008.68048
[4] Cortier, V.; Kremer, S.; Warinschi, B., A survey of symbolic methods in computational analysis of cryptographic systems, J. Autom. Reason., 46, 3-4, 225-259, (2011) · Zbl 1213.94093
[5] Bana, G.; Comon-Lundh, H., Towards unconditional soundness: computationally complete symbolic attacker, (Proc. 1st International Conference on Principles of Security and Trust, POST’12, (2012), Springer), 189-208 · Zbl 1353.68018
[6] Bana, G.; Comon-Lundh, H., A computationally complete symbolic attacker for equivalence properties, (Proc. 21st Conference on Computer and Communications Security, CCS’14, (2014), ACM), 609-620
[7] Cortier, V.; Eigner, F.; Kremer, S.; Maffei, M.; Wiedling, C., Type-based verification of electronic voting protocols, (Proc. 4th Conference on Principles of Security and Trust, POST’15, (2015), Springer), 303-323
[8] Barthe, G.; Fournet, C.; Grégoire, B.; Strub, P.-Y.; Swamy, N.; Zanella-Béguelin, S., Probabilistic relational verification for cryptographic implementations, (Proc. 41st Symposium on Principles of Programming Languages, vol. 49, POPL’14, (2014), ACM), 193-206 · Zbl 1284.68380
[9] Diffie, W.; Hellman, M., New directions in cryptography, Trans. Inf. Soc., 22, 6, 644-654, (1976) · Zbl 0435.94018
[10] Rivest, R.; Shamir, A.; Adleman, L., A method for obtaining digital signatures and public-key cryptosystems, Commun. ACM, 21, 2, 120-126, (1978) · Zbl 0368.94005
[11] PKI for machine readable travel documents offering ICC Read-only access, (2004), International Civil Aviation Organization, Tech. rep.
[12] Arapinis, M.; Chothia, T.; Ritter, E.; Ryan, M., Analysing unlinkability and anonymity using the applied pi calculus, (Proc. 23rd Computer Security Foundations Symposium, CSF’10, (2010), IEEE Computer Society Press), 107-121
[13] Lowe, G., A hierarchy of authentication specifications, (Proc. 10th Computer Security Foundations Workshop, CSFW’97, (1997), IEEE Computer Society Press), 18-30
[14] Abadi, M., Secrecy by typing in security protocols, (Theoretical Aspects of Computer Software, (1997), Springer), 611-638
[15] Blanchet, B., Automatic proof of strong secrecy for security protocols, (Proc. 2004 Symposium on Security and Privacy, (2004), IEEE Computer Society Press), 86-100
[16] Abadi, M.; Gordon, A. D., A calculus for cryptographic protocols: the spi calculus, (Proc. of the 4th ACM Conference on Computer and Communications Security, (1997), ACM), 36-47
[17] Arapinis, M.; Chothia, T.; Ritter, E.; Ryan, M., Untraceability in the applied pi-calculus, (Proc. International Conference for Internet Technology and Secured Transactions, ICITST’09, (2009), IEEE Computer Society Press), 1-6
[18] Schneider, S.; Sidiropoulos, A., CSP and anonymity, (Proc. International Conference on Computer Security, ESORICS’96, (1996), Springer), 198-218
[19] Chothia, T., Analysing the mute anonymous file-sharing system using the pi-calculus, (Formal Techniques for Networked and Distributed Systems - FORTE 2006, (2006), Springer), 115-130 · Zbl 1225.68038
[20] Kremer, S.; Ryan, M. D., Analysis of an electronic voting protocol in the applied pi-calculus, (Proc. 14th European Symposium on Programming, ESOP’05, Lect. Notes Comput. Sci., vol. 3444, (2005), Springer-Verlag), 186-200 · Zbl 1108.68462
[21] Delaune, S.; Kremer, S.; Ryan, M. D., Verifying privacy-type properties of electronic voting protocols, J. Comput. Secur., 17, 4, 435-487, (2008)
[22] Benaloh, J.; Tuinstra, D., Receipt-free secret-ballot elections (extended abstract), (Proc. 26th Symposium on Theory of Computing, STOC’94, (1994), ACM Press), 544-553 · Zbl 1344.68029
[23] Delaune, S.; Kremer, S.; Ryan, M. D., Coercion-resistance and receipt-freeness in electronic voting, (Proc. 19th Computer Security Foundations Workshop, CSFW’06, (2006), IEEE Computer Society Press), 28-39
[24] Backes, M.; Hritcu, C.; Maffei, M., Automated verification of remote electronic voting protocols in the applied pi-calculus, (Proc. 21st Computer Security Foundations Symposium, CSF’08, (2008), IEEE Computer Society Press), 195-209
[25] Arapinis, M.; Cortier, V.; Kremer, S.; Ryan, M. D., Practical everlasting privacy, (Proc. 2nd Conference on Principles of Security and Trust, POST’13, Lect. Notes Comput. Sci., vol. 7796, (2013), Springer), 21-40 · Zbl 1390.68273
[26] Dong, N.; Jonker, H.; Pang, J., Analysis of a receipt-free auction protocol in the applied pi calculus, (Proceedings of the 7th International Workshop on Formal Aspects in Security and Trust, FAST’10, Lect. Notes Comput. Sci., vol. 6561, (2010), Springer), 223-238
[27] Dreier, J.; Lafourcade, P.; Lakhnech, Y., Formal verification of e-auction protocols, (Proc. 2nd Conferences on Principles of Security and Trust, POST’13, Lect. Notes Comput. Sci., vol. 7796, (2013), Springer), 247-266 · Zbl 1390.68078
[28] Brusó, M.; Chatzikokolakis, K.; Den Hartog, J., Formal verification of privacy for RFID systems, (Proc. 23rd Computer Security Foundations Symposium, CSF’10, (2010), IEEE Computer Society Press), 75-88
[29] Van Deursen, T.; Mauw, S.; Radomirović, S., Untraceability of RFID protocols, (Information Security Theory and Practices. Smart Devices, Convergence and Next Generation Networks, (2008), Springer), 1-15
[30] Brusó, M.; Chatzikokolakis, K.; Etalle, S.; Den Hartog, J., Linking unlinkability, (Trustworthy Global Computing, (2013), Springer), 129-144
[31] Canetti, R., Universally composable security: a new paradigm for cryptographic protocols, (Proc. 42nd Annual Symposium on Foundations of Computer Science, FOCS’01, (2001), IEEE Computer Society Press), 136-145
[32] Delaune, S.; Kremer, S.; Pereira, O., Simulation based security in the applied pi calculus, (Proc. 29th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’09, Leibniz Int. Proc. Inform., vol. 4, (2009), Leibniz-Zentrum für Informatik), 169-180 · Zbl 1250.94035
[33] Böhl, F.; Unruh, D., Symbolic universal composability, (Proc. 26th Computer Security Foundations Symposium, CSF’13, (2013), IEEE Computer Society Press), 257-271
[34] Abadi, M.; Fournet, C., Mobile values, new names, and secure communication, (Proc. 28th Symposium on Principles of Programming Languages, POPL’01, (2001), ACM Press), 104-115 · Zbl 1323.68398
[35] B. Blanchet, Proverif 1.91, http://prosecco.gforge.inria.fr/personal/bblanche/, as downloaded on October 1st, 2015. See files in directory /examples/pitype/choice/.
[36] Abadi, M.; Cortier, V., Deciding knowledge in security protocols under equational theories, (Proc. 31st International Colloquium on Automata, Languages, and Programming, ICALP’04, Lect. Notes Comput. Sci., vol. 3142, (2004), Springer-Verlag), 46-58 · Zbl 1099.94026
[37] Abadi, M.; Cortier, V., Deciding knowledge in security protocols under (many more) equational theories, (Proc. 18th Computer Security Foundations Workshop, CSFW’05, (2005), IEEE Computer Society Press), 62-76
[38] Cortier, V.; Delaune, S., Decidability and combination results for two notions of knowledge in security protocols, J. Autom. Reason., 48, 4, 441-487, (2012) · Zbl 1242.68099
[39] Ciobâcă, Ş.; Delaune, S.; Kremer, S., Computing knowledge in security protocols under convergent equational theories, J. Autom. Reason., 48, 2, 219-262, (2012) · Zbl 1242.68098
[40] Baudet, M.; Cortier, V.; Delaune, S., YAPA: a generic tool for computing intruder knowledge, ACM Trans. Comput. Log., 14, 1, (2013), article no. 4 · Zbl 1353.68019
[41] Conchinha, B.; Basin, D. A.; Caleiro, C., FAST: an efficient decision procedure for deduction and static equivalence, (Proc. 22nd International Conference on Rewriting Techniques and Applications, RTA’11, LIPIcs, vol. 10, (2011), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 11-20 · Zbl 1236.94073
[42] Abadi, M.; Gordon, A. D., A calculus for cryptographic protocols: the spi calculus, Inf. Comput., 148, 1, 1-70, (1999) · Zbl 0924.68073
[43] Cervesato, I.; Durgin, N.; Lincoln, P.; Mitchell, J.; Scedrov, A., A meta-notation for protocol analysis, (Proc. 12th Computer Security Foundations Workshop, CSFW’99, (1999), IEEE Computer Society Press), 55-69
[44] Thayer, F. J.; Herzog, J. C.; Guttman, J. D., Strand spaces: proving security protocols correct, J. Comput. Secur., 7, 1, 191-230, (1999)
[45] Milner, R.; Sangiorgi, D., Barbed bisimulation, (Kuich, W., Proc. 19th International Colloquium on Automata, Languages, and Programming, ICALP’92, Lect. Notes Comput. Sci., vol. 623, (1992), Springer Verlag), 685-695
[46] Abadi, M.; Gordon, A. D., A bisimulation method for cryptographic protocols, Nord. J. Comput., 5, 4, 267, (1998) · Zbl 0913.68062
[47] Boreale, M.; Nicola, R. D.; Pugliese, R., Proof techniques for cryptographic processes, SIAM J. Comput., 31, 3, 947-986, (2002) · Zbl 1017.68050
[48] Bengtson, J.; Johansson, M.; Parrow, J.; Victor, B., Psi-calculi: a framework for mobile processes with nominal data and logic, Log. Methods Comput. Sci., 7, 1, (2011) · Zbl 1213.68399
[49] Cheval, V.; Cortier, V.; Delaune, S., Deciding equivalence-based properties using constraint solving, Theor. Comput. Sci., 492, 1-39, (2013) · Zbl 1294.68111
[50] Hüttel, H., Deciding framed bisimilarity, Electron. Notes Theor. Comput. Sci., 68, 6, 1-18, (2003) · Zbl 1270.68216
[51] Chrétien, R.; Cortier, V.; Delaune, S., From security protocols to pushdown automata, ACM Trans. Comput. Log., 17, 1, (2015), article no. 3 · Zbl 1367.68186
[52] Delaune, S.; Kremer, S.; Ryan, M. D., Symbolic bisimulation for the applied pi calculus, J. Comput. Secur., 18, 2, 317-377, (2010)
[53] Durante, L.; Sisto, R.; Valenzano, A., Automatic testing equivalence verification of spi calculus specifications, ACM Trans. Softw. Eng. Methodol., 12, 2, 222-284, (2003)
[54] Borgström, J., A complete symbolic bisimilarity for an extended spi calculus, Electron. Notes Theor. Comput. Sci., 242, 3, 3-20, (2009) · Zbl 1294.68109
[55] Borgström, J.; Gutkovas, R.; Rodhe, I.; Victor, B., The psi-calculi workbench: a generic tool for applied process calculi, ACM Trans. Embed. Comput. Syst., 14, 1, 9:1-9:25, (2015)
[56] Baudet, M., Deciding security of protocols against off-line guessing attacks, (Proc. 12th ACM conference on Computer and Communications Security, CCS’05, (2005), ACM), 16-25
[57] Chevalier, Y.; Rusinowitch, M., Decidability of symbolic equivalence of derivations, J. Autom. Reason., 48, 2, 263-292, (2012) · Zbl 1242.68097
[58] Tiu, A.; Dawson, J., Automating open bisimulation checking for the spi calculus, (Proc. 23rd Computer Security Foundations Symposium, CSF’10, (2010), IEEE Computer Society Press), 307-321
[59] Tiu, A., A trace based bisimulation for the spi calculus, (Programming Languages and Systems, (2007), Springer), 367-382 · Zbl 1137.68455
[60] Cheval, V.; Comon-Lundh, H.; Delaune, S., Trace equivalence decision: negative tests and non-determinism, (Proc. 18th ACM Conference on Computer and Communications Security, CCS’11, (2011), ACM Press), 321-330
[61] Cheval, V.; Comon-Lundh, H.; Delaune, S., Automating security analysis: symbolic equivalence of constraint systems, (Proc. 5th International Joint Conference on Automated Reasoning, IJCAR’10, Lect. Notes Artif. Intell., vol. 6173, (2010), Springer-Verlag), 412-426 · Zbl 1291.94068
[62] Cheval, V., APTE: an algorithm for proving trace equivalence, (Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’14, Lect. Notes Comput. Sci., vol. 8413, (2014)), 587-592
[63] Cheval, V.; Cortier, V.; Plet, A., Lengths may break privacy - or how to check for equivalences with length, (Proc. 25th International Conference on Computer Aided Verification, CAV’13, Lect. Notes Comput. Sci., vol. 8044, (2013), Springer Berlin, Heidelberg), 708-723
[64] Cheval, V.; Cortier, V., Timing attacks in security protocols: symbolic framework and proof techniques, (Proc. 4th Conference on Principles of Security and Trust, POST’15, (2015), Springer), 280-299
[65] Chadha, R.; Ciobâcă, Ş.; Kremer, S., Automated verification of equivalence properties of cryptographic protocols, (Proc. European Symposium on Programming, ESOP’12, (2012), Springer), 108-127 · Zbl 1352.68148
[66] Comon-Lundh, H.; Delaune, S., The finite variant property: how to get rid of some algebraic properties, (Proc. International Conference on Rewriting Techniques and Applications, RTA’05, (2005), Springer), 294-307 · Zbl 1078.68059
[67] Chadha, R.; Cheval, V.; Ciobâcă, Ş.; Kremer, S., Automated verification of equivalence properties of cryptographic protocol, ACM Trans. Comput. Log., 17, 4, (2016), article no. 23 · Zbl 1367.68184
[68] Baelde, D.; Delaune, S.; Hirschi, L., Partial order reduction for security protocols, (Proc. 26th International Conference on Concurrency Theory, CONCUR’15, LIPIcs, vol. 42, (2015), Leibniz-Zentrum für Informatik), 497-510 · Zbl 1374.68318
[69] Baelde, D.; Delaune, S.; Hirschi, L., A reduced semantics for deciding trace equivalence using constraint systems, (Proc. 3rd Conference on Principles of Security and Trust, POST’14, (2014), Springer), 1-21
[70] Chrétien, R.; Cortier, V.; Delaune, S., From security protocols to pushdown automata, (Proc. 40th International Colloquium on Automata, Languages and Programming, ICALP’13, Lect. Notes Comput. Sci., vol. 7966, (2013), Springer), 137-149 · Zbl 1335.94040
[71] Comon-Lundh, H.; Cortier, V., New decidability results for fragments of first-order logic and application to cryptographic protocols, (14th Proc. International Conference on Rewriting Techniques and Applications, RTA’2003, Lect. Notes Comput. Sci., vol. 2706, (2003), Springer), 148-164 · Zbl 1038.03012
[72] Henry, P.; Sénizergues, G., LALBLC a program testing the equivalence of Dpda’s, (Proc. 18th International Conference on Implementation and Application of Automata, CIAA’13, Lect. Notes Comput. Sci., vol. 7982, (2013), Springer Halifax, NS, Canada), 169-180 · Zbl 1298.68139
[73] Chrétien, R.; Cortier, V.; Delaune, S., Typing messages for free in security protocols: the case of equivalence properties, (Proc. 25th International Conference on Concurrency Theory, CONCUR’14, Lect. Notes Comput. Sci., vol. 8704, (2014), Springer), 372-386 · Zbl 1417.68124
[74] Blanchet, B.; Podelski, A., Verification of cryptographic protocols: tagging enforces termination, (Proc. International Conference on Foundations of Software Science and Computation Structures, FoSSaCS’03, Lect. Notes Comput. Sci., vol. 2620, (2003)), 136-152 · Zbl 1029.94501
[75] Chrétien, R.; Cortier, V.; Delaune, S., Decidability of trace equivalence for protocols with nonces, (Proc. 28th Computer Security Foundations Symposium, CSF’15, (2015), IEEE Computer Society Press), 170-184
[76] Blanchet, B.; Abadi, M.; Fournet, C., Automated verification of selected equivalences for security protocols, (Proc. 20th Symposium on Logic in Computer Science, LICS’05, (2005), IEEE Computer Society Press), 331-340
[77] Basin, D.; Dreier, J.; Sasse, R., Automated symbolic proofs of observational equivalence, (Proc. 22nd Conference on Computer and Communications Security, CCS’15, (2015), ACM), 1144-1155
[78] Santiago, S.; Escobar, S.; Meadows, C.; Meseguer, J., A formal definition of protocol indistinguishability and its verification using maude-NPA, (Security and Trust Management, (2014), Springer), 162-177
[79] Blanchet, B.; Abadi, M.; Fournet, C., Automated verification of selected equivalences for security protocols, J. Log. Algebraic Program., 75, 1, 3-51, (2008) · Zbl 1135.68007
[80] Cheval, V.; Blanchet, B., Proving more observational equivalences with proverif, (Proc. 2nd Conference on Principles of Security and Trust, POST’13, Lect. Notes Comput. Sci., vol. 7796, (2013), Springer), 226-246 · Zbl 1391.94737
[81] Delaune, S.; Ryan, M. D.; Smyth, B., Automatic verification of privacy properties in the applied pi-calculus, (Proc. 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security, IFIPTM’08, IFIP Conf. Proc., vol. 263, (2008), Springer), 263-278
[82] Blanchet, B.; Smyth, B., Automated reasoning for equivalences in the applied pi calculus with barriers, (IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27-July 1, (2016)), 310-324
[83] Arapinis, M.; Bursuc, S.; Ryan, M. D., Reduction of equational theories for verification of trace equivalence: re-encryption, associativity and commutativity, (Proc. 1st International Conference on Principles of Security and Trust, POST’12, Lect. Notes Comput. Sci., vol. 7215, (2012), Springer), 169-188 · Zbl 1353.68069
[84] Meier, S.; Schmidt, B.; Cremers, C.; Basin, D., The TAMARIN prover for the symbolic analysis of security protocols, (Proc. International Conference on Computer Aided Verification, CAV’13, (2013), Springer), 696-701
[85] Schmidt, B.; Meier, S.; Cremers, C.; Basin, D., Automated analysis of diffie-hellman protocols and advanced security properties, (Proc. 25th Computer Security Foundations Symposium, CSF’12, (2012), IEEE Computer Society Press), 78-94
[86] Escobar, S.; Sasse, R.; Meseguer, J., Folding variant narrowing and optimal variant termination, (Rewriting Logic and Its Applications, (2010), Springer), 52-68 · Zbl 1306.68069
[87] Cortier, V.; Smyth, B., Attacking and fixing helios: an analysis of ballot secrecy, (Proc. 24th Computer Security Foundations Symposium, CSF’11, (2011), IEEE Computer Society Press), 297-311
[88] Cortier, V.; Wiedling, C., A formal analysis of the Norwegian e-voting protocol, (Proc. 2nd Conference on Principles of Security and Trust, (2012), Springer), 109-128
[89] Arapinis, M.; Mancini, L. I.; Ritter, E.; Ryan, M., Privacy through pseudonymity in mobile telephony systems, (Proc. Network and Distributed System Security Symposium, NDSS’14, (2014))
[90] Hirschi, L.; Baelde, D.; Delaune, S., A method for verifying privacy-type properties: the unbounded case, (IEEE Symposium on Security and Privacy, SP 2016, San Jose, CA, USA, May 22-26, (2016)), 564-581
[91] van Deursen, T.; Radomirović, S., Algebraic attacks on RFID protocols, (Information Security Theory and Practice. Smart Devices, Pervasive Systems, and Ubiquitous Networks, (2009), Springer), 38-51
[92] Delaune, S.; Kremer, S.; Pasailă, D., Security protocols, constraint systems, and group theories, (Proc. 6th International Joint Conference on Automated Reasoning, IJCAR’12, Lect. Notes Artif. Intell., vol. 7364, (2012), Springer-Verlag), 164-178 · Zbl 1358.68185
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.