Abstract
In recent years, many researches have been done to establish symbolic models of stateful protocols. Two works among them, the SAPIC tool and StatVerif tool, provide a high-level specification language and an automated analysis. Their language, the stateful applied \(\pi \) calculus, is extended from the applied \(\pi \) calculus by defining explicit state constructs. Symbolic abstractions of cryptography used in it make the analysis amenable to automation. However, this might overlook the attacks based on the algebraic properties of the cryptographic algorithms. In our paper, we establish the computational soundness results for stateful applied \(\pi \) calculus used in SAPIC tool and StatVerif tool.
In our approach, we build our results on the CoSP framework. For SAPIC, we embed the non-monotonic protocol states into the CoSP protocols, and prove that the resulting CoSP protocols are efficient. Through the embedding, we provide the computational soundness result for SAPIC (by TheoremĀ 1). For StatVerif, we encode the StatVerif process into a subset of SAPIC process, and obtain the computational soundness result for StatVerif (by TheoremĀ 2). Our encoding shows the differences between the semantics of the two languages. Our work inherits the modularity of CoSP, which allows for easily extending the proofs to specific cryptographic primitives. Thus we establish a computationally sound automated verification result for the input languages of SAPIC and StatVerif that use public-key encryption and signatures (by TheoremĀ 3).
Y. QināThe research presented in this paper is supported by the National Basic Research Program of China (No. 2013CB338003) and National Natural Science Foundation of China (No. 91118006, No. 61202414).
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.
Otherwise, the length of \(\pi \)-terms may grow exponentially by the iterated binding of variables. One example is the construct \(!([\text {Iter}(x)]-[]\rightarrow [\text {Iter}(fun(x,x))]\)).
- 2.
For a closed StatVerif process \(P_0\), we denote by \(Q_0\) and \(\wp \) the same meanings in Lemma 1. We say \(P_0\) computationally satisfies \(\wp \) iff \(Q_0\) computationally satisfies \(\wp \).
References
Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 2001 Proceedings of the 14th IEEE Computer Security Foundations Workshopp, pp. 82ā96 (2001)
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)
Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007/2008/2009. LNCS, vol. 5705, pp. 1ā50. Springer, Heidelberg (2009)
Dolev, D., Yao, A.C.: On the security of public key protocols. In: Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, SFCS 1981, pp. 350ā357. IEEE Computer Society, Washington, DC (1981)
Even, S., Goldreich, O.: On the security of multi-party ping-pong protocols. In: 24th Annual Symposium on Foundations of Computer Science, pp. 34ā39, November 1983
Abadi, M., Rogaway, P.: Reconciling two views of cryptography. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 3ā22. Springer, Heidelberg (2000)
Janvier, R., Lakhnech, Y., MazarĆ©, L.: Completing the picture: soundness of formal encryption in the presence of active adversaries. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 172ā185. Springer, Heidelberg (2005)
Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 133ā151. Springer, Heidelberg (2004)
Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 157ā171. Springer, Heidelberg (2005)
Cortier, V., Kremer, S., KĆ¼sters, R., Warinschi, B.: Computationally sound symbolic secrecy in the presence of hash functions. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 176ā187. Springer, Heidelberg (2006)
Backes, M., Hofheinz, D., Unruh, D.: CoSP: a general framework for computational soundness proofs. In: Proceedings of the 16th ACM Conference on Computer and Communications Security, CCS 2009, pp. 66ā78. ACM, New York (2009)
Backes, M., Bendun, F., Unruh, D.: Computational soundness of symbolic zero-knowledge proofs: weaker assumptions and mechanized verification. In: Basin, D., Mitchell, J.C. (eds.) POST 2013 (ETAPS 2013). LNCS, vol. 7796, pp. 206ā225. Springer, Heidelberg (2013)
Cortier, V., Warinschi, B.: A composable computational soundness notion. In: Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS 2011, pp. 63ā74. ACM, New York (2011)
Bƶhl, F., Cortier, V., Warinschi, B.: Deduction soundness: prove one, get five for free. In: Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security, CCS 2013, pp. 1261ā1272. ACM, New York (2013)
Backes, M., Malik, A., Unruh, D.: Computational soundness without protocol restrictions. In: Proceedings of the 2012 ACM Conference on Computer and Communications Security, CCS 2012, pp. 699ā711. ACM, New York (2012)
Arapinis, M., Liu, J., Ritter, E., Ryan, M.: Stateful applied Pi Calculus. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 22ā41. Springer, Heidelberg (2014)
Guttman, J.D.: State and progress in strand spaces: proving fair exchange. J. Autom. Reason. 48, 159ā195 (2012)
Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: 2012 IEEE 25th Computer Security Foundations Symposium (CSF), pp. 78ā94, June 2012
Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: Formal analysis of protocols based on TPM state registers. In: Proceedings of the 2011 IEEE 24th Computer Security Foundations Symposium, CSF 2011, pp. 66ā80. IEEE Computer Society, Washington, DC (2011)
Kremer, S., KĆ¼nnemann, R.: Automated analysis of security protocols with global state. In: Proceedings of the 35th IEEE Symposium on Security and Privacy, SP 2014. IEEE Computer Society, Washington (2014)
Arapinis, M., Ritter, E., Ryan, M.D.: StatVerif: verification of stateful processes. In: 2011 IEEE 24th Computer Security Foundations Symposium (CSF), pp. 33ā47, June 2011
Mƶdersheim, S.A.: Abstraction by set-membership: verifying security protocols and web services with databases. In: Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, pp. 351ā360. ACM, New York (2010)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol. 36, pp. 104ā115, January 2001
Backes, M., Mohammadi, E., Ruffing, T.: Computational soundness results for ProVerif: bridging the gap from trace properties to uniformity. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 42ā62. Springer, Heidelberg (2014)
Backes, M., Maffei, M., Unruh, D.: Computationally sound verification of source code. In: Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, pp. 387ā398. ACM, New York (2010)
Shao, J., Qin, Y., Feng, D.: Computational Soundness Results for Stateful Applied \(\pi \) Calculus. http://arxiv.org/abs/1601.00363
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
Shao, J., Qin, Y., Feng, D. (2016). Computational Soundness Results for Stateful Applied \(\pi \) Calculus. 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_13
Download citation
DOI: https://doi.org/10.1007/978-3-662-49635-0_13
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)
