Abstract
We present a symbolic decision procedure for time-sensitive cryptographic protocols with time-stamps. Our decision procedure deals with secrecy, authentication and any property that can be described as an invariance property.
This work has been partially suppoted by the projects ACI-SI ROSSIGNOL http://www.cmi.univ-mrs.fr/~lugiez/aci-rossignol.html and PROUVE-03V360.
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
Bella, G., Paulson, L.C.: Mechanizing BAN Kerberos by the inductive method. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 416–427. Springer, Heidelberg (1998)
Bozga, L., Ene, C., Lakhnech, Y.: On the existence of an effective and complete inference system for cryptographic protocols. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 42–57. Springer, Heidelberg (2004)
Clark, J., Joacob, J.: A survey on authentication protocol (1997), Available at the url: http://www.cs.york.ac.uk/jac/papers/drareviewps.ps
Cohen, E.: Taps: A first-order verifier for cryptographic protocols. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW 2000), p. 144. IEEE Computer Society, Los Alamitos (2000)
Comon, H.: Disunification: A survey. In: Computational Logic: Essays in Honor of Alan Robinson. MIT Press, Cambridge, MA (1991)
Delzanno, G., Ganty, P.: Automatic verification of time sensitive cryptographic protocols. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 342–356. Springer, Heidelberg (2004)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
Evans, N., Schneider, S.: Analyzing time dependent security properties in CSP using PVS. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol. 1895, pp. 222–237. Springer, Heidelberg (2000)
Fiore, M., Abadi, M.: Computing symbolic models for verifying cryptographic protocols. In: 14th IEEE Computer Security Foundations Workshop (CSFW 2001), Washington - Brussels - Tokyo, pp. 160–173. IEEE, Los Alamitos (2001)
Gong, L.: A security risk of depending on synchronized clocks. Operating Systems Review 26(1), 49–53 (1992)
Gorrieri, R., Martinelli, F.: A simple framework for real-time cryptographic protocol analysis with compositional proof rules. Science of Computer Programming 50(1-3), 23–49 (2004)
Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: A rule-based survey of unification. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson. MIT-Press, Cambridge (1991)
Lowe, G.: Breaking and fixing the Needham-Schroeder Public-Key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Lowe, G.: A hierarchy of authentication specifications. In: Proc. of The 10th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (1997)
Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: ACM Conference on Computer and Communications Security, pp. 166–175 (2001)
Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: IEEE Computer Security Foundations Workshop (2001)
Thayer, J., Herzog, J., Guttman, J.: Honest Ideals on Strand Spaces. In: IEEE Computer Security Foundations Workshop, pp. 66–78 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bozga, L., Ene, C., Lakhnech, Y. (2004). A Symbolic Decision Procedure for Cryptographic Protocols with Time Stamps . In: Gardner, P., Yoshida, N. (eds) CONCUR 2004 - Concurrency Theory. CONCUR 2004. Lecture Notes in Computer Science, vol 3170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-28644-8_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-28644-8_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22940-7
Online ISBN: 978-3-540-28644-8
eBook Packages: Springer Book Archive