Abstract
Two styles of definitions are usually considered to express that a security protocol preserves the confidentiality of a data s. Reachability-based secrecy means that s should never be disclosed while equivalence-based secrecy states that two executions of a protocol with distinct instances for s should be indistinguishable to an attacker. Although the second formulation ensures a higher level of security and is closer to cryptographic notions of secrecy, decidability results and automatic tools have mainly focused on the first definition so far.
This paper initiates a systematic investigation of situations where syntactic secrecy entails strong secrecy. We show that in the passive case, reachability-based secrecy actually implies equivalence-based secrecy for signatures, symmetric and asymmetric encryption provided that the primitives are probabilistic. For active adversaries in the case of symmetric encryption, we provide sufficient (and rather tight) conditions on the protocol for this implication to hold.
This work has been partially supported by the ACI-SI Satin and the ACI Jeunes Chercheurs JC9005.
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
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: 28th Symp. on Principles of Programming Languages (POPL 2001). ACM Press, New York (2001)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. In: 4th Conf. on Computer and Communications Security (CCS 1997), pp. 36–47. ACM Press, New York (1997)
Amadio, R., Lugiez, D.: On the reachability problem in cryptographic protocols. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877. Springer, Heidelberg (2000)
The AVISPA Project, http://www.avispa-project.org/
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Computer Security Foundations Workshop (CSFW 2001), pp. 82–96. IEEE Computer Society Press, Los Alamitos (2001)
Blanchet, B.: Automatic Proof of Strong Secrecy for Security Protocols. In: IEEE Symposium on Security and Privacy (SP 2004), pp. 86–100 (2004)
Blanchet, B., Podelski, A.: Verification of cryptographic protocols: Tagging enforces termination. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 136–152. Springer, Heidelberg (2003)
Borgström, J., Briais, S., Nestmann, U.: Symbolic bisimulation in the SPI calculus. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 161–176. Springer, Heidelberg (2004)
Bozga, L., Lakhnech, Y., Périn, M.: HERMES: An automatic tool for verification of secrecy in security protocols. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 219–222. Springer, Heidelberg (2003)
Comon-Lundh, H., Cortier, V.: New decidability results for fragments of first-order logic and application to cryptographic protocols. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 148–164. Springer, Heidelberg (2003)
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)
Denker, G., Millen, J., Rueß, H.: The CAPSL Integrated Protocol Environment. Technical Report SRI-CSL-2000-02, SRI International, Menlo Park, CA (2000)
Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Workshop on Formal Methods and Security Protocols (1999)
Hüttel, H.: Deciding framed bisimilarity. In: INFINITY 2002 (August 2002)
Paulson, L.C.: Relations between secrets: Two formal analyses of the Yahalom protocol. Journal of Computer Security 9(3), 197–216 (2001)
Ramanujam, R., Suresh, S.P.: Tagging makes secrecy decidable with unbounded nonces as well. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 363–374. Springer, Heidelberg (2003)
Rusinowitch, M., Turuani, M.: Protocol Insecurity with Finite Number of Sessions and Composed Keys is NP-complete. Theoretical Computer Science 299, 451–475 (2003)
Zalinescu, E., Cortier, V., Rusinowitch, M.: Relating two standard notions of secrecy. Research Report 5908, INRIA (April 2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cortier, V., Rusinowitch, M., Zălinescu, E. (2006). Relating Two Standard Notions of Secrecy. In: Ésik, Z. (eds) Computer Science Logic. CSL 2006. Lecture Notes in Computer Science, vol 4207. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11874683_20
Download citation
DOI: https://doi.org/10.1007/11874683_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-45458-8
Online ISBN: 978-3-540-45459-5
eBook Packages: Computer ScienceComputer Science (R0)