Abstract
Bounding the number of agents is a current practice when modeling a protocol. In 2003, it has been shown that one honest agent and one dishonest agent are indeed sufficient to find all possible attacks, for secrecy properties. This is no longer the case for equivalence properties, crucial to express many properties such as vote privacy or untraceability.
In this paper, we show that it is sufficient to consider two honest agents and two dishonest agents for equivalence properties, for deterministic processes with standard primitives and without else branches. More generally, we show how to bound the number of agents for arbitrary constructor theories and for protocols with simple else branches. We show that our hypotheses are tight, providing counter-examples for non action-deterministic processes, non constructor theories, or protocols with complex else branches.
The research leading to these results has received funding from the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007-2013)/ERC grant agreement \(n^{\circ }\) 258865, project ProSecure, the ANR project JCJC VIP n\(^o\) 11 JS02 006 01, and the DGA.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of the 28th Symposium on Principles of Programming Languages (POPL 2001). ACM Press (2001)
Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: Proceedings of the 23rd Computer Security Foundations Symposium (CSF 2010), pp. 107–121. IEEE Computer Society Press (2010)
Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: Proceedings of 29th IEEE Symposium on Security and Privacy, May 2008
Baelde, D., Delaune, S., Hirschi, L.: Partial order reduction for security protocols. In: Aceto, L., de Frutos-Escrig, D. (eds.) CONCUR 2015. Leibniz International Proceedings in Informatics, vol. 42, pp. 497–510. Leibniz-Zentrum für Informatik, Madrid (2015)
Blanchet, B.: Proverif 1.91. As downloaded on October 1st. See files in directory (2015). http://prosecco.gforge.inria.fr/personal/bblanche/examples/pitype/choice/
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of the 14th Computer Security Foundations Workshop (CSFW 2001). IEEE Computer Society Press, June 2001
Blanchet, B.: An automatic security protocol verifier based on resolution theorem proving (invited tutorial). In: Proceedings of the 20th International Conference on Automated Deduction (CADE-20), Tallinn, July 2005
Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. J. Logic Algebr. Program. 75(1), 3–51 (2008)
Chadha, R., Ciobâcă, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 108–127. Springer, Heidelberg (2012)
Cheval, V., Cortier, V., Delaune, S.: Deciding equivalence-based properties using constraint solving. Theor. Comput. Sci. 492, 1–39 (2013)
Chothia, T., Smirnov, V.: A traceability attack against e-passports. In: Proceedings of the 14th International Conference on Financial Cryptography and Data Security (FC) (2010)
Chrétien, R., Cortier, V., Delaune, S.: From security protocols to pushdown automata. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 137–149. Springer, Heidelberg (2013)
Chrétien, R., Cortier, V., Delaune, S.: Checking trace equivalence: how to get rid of nonces? In: Pernul, G., Ryan, P.Y.A., Weippl, E. (eds.) ESORICS 2015. LNCS, vol. 9327, pp. 230–251. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24177-7_12
Comon-Lundh, H., Cortier, V.: Security properties: two agents are sufficient. Sci. Comput. Program. 50(1–3), 51–71 (2004)
Comon-Lundh, H., Cortier, V.: Computational soundness of observational equivalence. In: Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS 2008), pp. 109–118. ACM Press, Alexandria, October 2008
Cortier, V., Dallon, A., Delaune, S.: Bounding the number of agents, for equivalence too. Research report LSV-16-01, Laboratoire Spécification et Vérification, ENS Cachan, p. 37, January 2016
Cremers, C.J.F.: The scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008)
Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 4, 435–487 (2008)
Denning, D., Sacco, G.: Timestamps in key distributed protocols. Commun. ACM 24(8), 533–535 (1981)
Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Chong, S. (ed.) Proceedings of the 25th IEEE Computer Security Foundations Symposium, CSF 2012, IEEE, Cambridge, pp. 78–94, 25–27 June 2012
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cortier, V., Dallon, A., Delaune, S. (2016). Bounding the Number of Agents, for Equivalence Too. In: Piessens, F., Viganò, L. (eds) Principles of Security and Trust. POST 2016. Lecture Notes in Computer Science(), vol 9635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-49635-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-662-49635-0_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-49634-3
Online ISBN: 978-3-662-49635-0
eBook Packages: Computer ScienceComputer Science (R0)
