Abstract
Abstraction based approaches like ProVerif are very efficient in protocol verification, but have a limitation in dealing with stateful protocols. A number of extensions have been proposed to allow for a limited amount of state information while not destroying the advantages of the abstraction method. However, the extensions proposed so far can only deal with a finite amount of state information. This can in many cases make it impossible to formulate a verification problem for an unbounded number of agents (and one has to rather specify a fixed set of agents). Our work shows how to overcome this limitation by abstracting state into countable families of sets. We can then formalize a problem with unbounded agents, where each agent maintains its own set of keys. Still, our method does not loose the benefits of the abstraction approach, in particular, it translates a verification problem to a set of first-order Horn clauses that can then be efficiently verified with tools like ProVerif.
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
Notes
- 1.
If one would rather like to model that servers cannot see which keys the other servers consider as valid or revoked, one runs indeed into the boundaries of AIF-\(\omega \) here. This is because in this case one must accept that at least a dishonest agent can register the same key at two different servers, violating the uniqueness invariant. If one wants to model such systems, one must resort to finitely many servers.
- 2.
In fact, we are here over-careful as the case \(\sigma (A)=a\) in the second rule would still be fine; but a precise solution in general would require inequalities—which we leave for future work.
References
Arapinis, M., Phillips, J., Ritter, E., Ryan, M.D.: Statverif: verification of stateful processes. J. Comput. Secur. 22(5), 743–821 (2014)
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Computer Security Foundations Workshop (2001)
Bruni, A., Modersheim, S.: The AIF-\(\omega \) Compiler and Examples. http://www.compute.dtu.dk/~samo/aifom.html
Bruni, A., Mödersheim, S., Nielson, F., Nielson, H.R.: Set-pi: set membership p-calculus. In: IEEE 28th Computer Security Foundations Symposium, CSF 2015 (2015)
Comon-Lundh, H., Cortier, V.: Security properties: two agents are sufficient. Sci. Comput. Program. 50(1–3), 51–71 (2004)
Fröschle, S., Steel, G.: Analysing PKCS#11 key management apis with unbounded fresh data. In: Degano, P., Viganò, L. (eds.) ARSPA-WITS 2009. LNCS, vol. 5511, pp. 92–106. Springer, Heidelberg (2009)
Kremer, S., Künnemann, R.: Automated analysis of security protocols with global state. In: Security and Privacy (2014)
Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013)
Ye, M.: Design and analysis of PKCS#11 key management with AIF. Master’s thesis, DTU Compute (2014). www2.compute.dtu.dk/~samo
Mödersheim, S.: Abstraction by set-membership: verifying security protocols and web services with databases. In: Computer and Communications Security (2010)
Mödersheim, S., Modesti, P.: Verifying sevecom using set-based abstraction. In: Proceedings of the 7th International Wireless Communications and Mobile Computing Conference, IWCMC 2011, Istanbul, Turkey, 4–8 July 2011 (2011)
Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 314–328. Springer, Heidelberg (1999)
Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009)
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
Mödersheim, S., Bruni, A. (2016). AIF-\(\omega \): Set-Based Protocol Abstraction with Countable Families. 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_12
Download citation
DOI: https://doi.org/10.1007/978-3-662-49635-0_12
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)
