Abstract
A real-time process algebra, enhanced with specific constructs for handling cryptographic primitives, is proposed to model cryptographic protocols in a simple way.We show that some security properties, such as authentication and secrecy, can be re-formulated in this timed setting. Moreover, we show that they can be seen as suitable instances of a general information flow-like scheme, called tGN DC, parametric w.r.t. the observational semantics of interest.We show that, when considering timed trace semantics, there exists a most powerful hostile environment (or enemy) that can try to compromise the protocol. Moreover, we hint some compositionality results.
Work partially supported by MURST Progetto “Metodi Formali per la Sicurezza” (MEFISTO); IST-FET project “Design Environments for Global ApplicationS (DEGAS)”; Microsoft Research Europe; by CNR project “Tecniche e Strumenti Software per l’analisi della sicurezza delle comunicazioni in applicazioni telematiche di interesse economico e sociale” and by a CSP grant for the project “SeTAPS II”.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Boreale and D. Gorla. on Compositional Reasoning in the Spi-calculus In proc. of FOSSACS’ 02, LNCS 2303, 2002.
P. Broadfoot and G. Lowe. Analysing a StreamAuthentication Protocol using Model Checking In Procs. ESORICS’02, LNCS, Springer, 2002.
N. De Francesco and M. Petrocchi. Authenticity in a Reliable Protocol for Mobile Computing. Accepted at 18th ACM Symposium on Applied Computing (SAC03). U.S., March 2003.
R. Focardi and R. Gorrieri. A classification of security properties. Journal of Computer Security, 3(1):5–33, 1995.
R. Focardi, R. Gorrieri and F. Martinelli. A comparison of three authentication properties. To appear on Theoretical Computer Science.
R. Focardi, R. Gorrieri and F. Martinelli. Secrecy in Security Protocols as Non Interference. Electronic Notes in Theoretical Computer Science, 32. (2000)
R. Focardi, R. Gorrieri and F. Martinelli. Non-interference for the analysis of cryptographic protocols. In Procs. Int.l Colloquium on Automata, Languages and Programming (ICALP’00), LNCS 1853, 354–372, Springer, 2000.
R. Focardi, R. Gorrieri and F. Martinelli. Real-time Information Flow Analysis Journal of Selected Areas of Communications, IEEE Press, 2002, to appear.
R. Focardi and F. Martinelli. A uniform approach for the definition of security properties. In Proceedings of World Congress on Formal Methods (FM’99), pages 794–813. Springer, LNCS 1708, 1999.
R. Gennaro and P. Rohatgi. How to Sign Digital Streams. Information and Computation 165(1), pp.100–116 (2001).
R. Gorrieri, F. Martinelli, M. Petrocchi and A. Vaccarelli. Using compositional reasoning and Non-interference for verifying integrity in digital stream protocols. Technical Report IIT, 2003. Submitted for publication.
J. F. Groote. Transition system specifications with negative premises. Theoretical Computer Science, 118:263–299, 1993.
J. Guttman and F. J. Thayer. Protocol Independence through Disjoint Encryption. In Proc. CSFW’00. IEEE Press, 2000.
G. Lowe. A Hiearchy of Autentication Specifications. In Proc. CSFW’97, pp. 31–43, IEEE Press.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
S. Schneider. Analysing Time-Dependent Security Properties in CSP using PVS. In Procs. ESORICS, LNCS 1895, 2000.
I. Ulidowski and S. Yuen. Extending process languages with time. In Proceedings of AMAST, LNCS 1349, pages 524–538, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gorrieri, R., Locatelli, E., Martinelli, F. (2003). A Simple Language for Real-Time Cryptographic Protocol Analysis. In: Degano, P. (eds) Programming Languages and Systems. ESOP 2003. Lecture Notes in Computer Science, vol 2618. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36575-3_9
Download citation
DOI: https://doi.org/10.1007/3-540-36575-3_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00886-6
Online ISBN: 978-3-540-36575-4
eBook Packages: Springer Book Archive