Abstract
This paper presents an approach to the analysis of real-time properties of security protocols, based on the Strand Space formalism for describing the behaviour of the participants in the protocol. The approach is compared with a trace-based analysis introduced by Pilegaard et al. [14]. Interval Logic with durations is used to express and reason about temporal phenomena. Strand Spaces were chosen as the starting point for our approach, since the causalities between important events in protocols are revealed in an illustrative manner by this formalism. The advantage of the trace-based approach is that it supports inductive reasoning in connection with the analysis of untimed properties. Interval Logic is chosen as the real-time formalism, as timing requirements and timing properties of security protocols are often expressible as interval properties. As an example, the Kerberos authentication protocol, which is based on concepts like timestamps and lifetimes, and which requires freshness of certain messages, is analysed.
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
Barua, R., Roy, S., Chaochen, Z.: Completeness of neighbourhood logic. Journal of Logic and Computation 10(2), 271–295 (2000)
Bellovin, S.M., Merritt, M.: Limitations of the Kerberos authentication system. In: Proc. of the USENIX Conference, pp. 253–267. USENIX Assoc. (1991)
Chan, P., Hung, D.V.: Duration calculus specification of scheduling for tasks with shared resources. In: Kanchanasut, K., Levy, J.-J. (eds.) Algorithms, Concurrency and Knowledge. LNCS, vol. 1023, pp. 365–380. Springer, Heidelberg (1995)
Halpern, J., Moszkowski, B., Manna, Z.: A hardware semantics based on temporal intervals. In: Díaz, J. (ed.) Automata, Languages and Programming. LNCS, vol. 154, pp. 278–291. Springer, Heidelberg (1983)
Hansen, M.R., Chaochen, Z.: Duration Calculus: Logical foundations. Formal Aspects of Computing 9(3), 283–330 (1997)
Kohl, J., Neuman, C.: RFC1510: The Kerberos network authentication service (V5). IETF (September 1993)
Lowe, G.: Some new attacks upon security protocols. In: Proc. of the 9th IEEE Security Foundations Workshop, pp. 162–169. IEEE Computer Society Press, Los Alamitos (1996)
Meadows, C.: A cost-based framework for analysis of denial-of-service in networks. Journal of Computer Security 9(1/2), 143–164 (2001)
Mørk, S., Godskesen, J.C., Hansen, M.R., Sharp, R.: A timed semantics for SDL. In: Formal Description Techniques IX: Theory, application and tools, pp. 295–309. Chapman & Hall, Sydney, Australia (1996)
Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. IEEE Computer 18(2), 10–19 (1985)
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6, 85–128 (1998)
Pilegaard, H.: Modelling properties of security protocols. Master’s thesis, Informatics and Mathematical Modelling, Technical University of Denmark (October 2002)
Pilegaard, H., Hansen, M.R., Sharp, R.: An approach to analyzing availability properties of security protocols. Nordic Journal of Computing 10(4), 337–373 (2003)
Rasmussen, T.M.: Automated proof support for interval logics. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 317–326. Springer, Heidelberg (2001)
Rasmussen, T.M.: Interval Logic – Proof Theory and Theorem Proving. PhD thesis, Informatics and Mathematical Modelling, Technical University of Denmark (2002)
Ravn, A.P., Rischel, H., Hansen, K.M.: Specifying and verifying requirements of real-time systems. IEEE Trans. on Software Engineering 19(1), 41–55 (1993)
Roscoe, A.W.: Modelling and verifying key-exchange protocols using CSP and FDR. In: Proc. of the 8th IEEE Security Foundations Workshop, IEEE Comp. Soc. Press, Los Alamitos (1995)
Thayer Fábrega, F.J., Herzog, J.C., Guttman, J.D.: Strand Spaces: Proving security protocols correct. Journal of Computer Security 7, 191–230 (1999)
Yu, C.-F., Gligor, V.D.: A formal specification and verification method for the prevention of denial of service. In: 1988 IEEE Symposium on Security and Privacy, pp. 187–202. IEEE Comp. Soc. Press, Los Alamitos (1988)
Yuhua, Z., Chaochen, Z.: A formal proof of the deadline driven scheduler. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 863, pp. 756–775. Springer, Heidelberg (1994)
Chaochen, Z., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. Monographs in Theoretical Computer Science. Springer, Heidelberg (2004)
Chaochen, Z., Hansen, M.R.: An adequate first order interval logic. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 581–608. Springer, Heidelberg (1998)
Chaochen, Z., Hansen, M.R., Ravn, A.P., Rischel, H.: Duration specifications for shared processors. In: Vytopil, J. (ed.) Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, vol. 571, pp. 21–32. Springer, Heidelberg (1991)
Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sharp, R., Hansen, M.R. (2007). Timed Traces and Strand Spaces. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds) Computer Science – Theory and Applications. CSR 2007. Lecture Notes in Computer Science, vol 4649. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74510-5_38
Download citation
DOI: https://doi.org/10.1007/978-3-540-74510-5_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74509-9
Online ISBN: 978-3-540-74510-5
eBook Packages: Computer ScienceComputer Science (R0)