Abstract
Causal reasoning is a powerful tool in analysing security protocols, as seen in the popularity of the strand space model. However, for protocols that branch, more subtle models are called for to capture the ways in which they can interact with a possibly malign environment. We study a model for security protocols encompassing causal reasoning and interaction, developing a semantics for a simple security protocol language based on concurrent games played on event structures. We show how it supports causal reasoning about a protocol for secure digital signature exchange. The semantics paves the way for the application of more sophisticated forms of concurrent game, for example including symmetry and probability, to the analysis of security protocols.
The support of the ERC through the Advanced Grant ECSYM is gratefully acknowledged.
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
Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. Journal of Computer Security 7(1), 191–230 (1999)
Paulson, L.C.: Proving properties of security protocols by induction. In: Proc. 10th IEEE Workshop on Computer Security Foundations, CSFW (1997)
Crazzolara, F., Winskel, G.: Events in security protocols. In: ACM Conference on Computer and Communications Security (2001)
Kremer, S., Raskin, J.F.: Game analysis of abuse-free contract signing. In: Proc. 15th IEEE Workshop on Computer Security Foundations, CSFW (2002)
Rideau, S., Winskel, G.: Concurrent strategies. In: Proc. LICS, pp. 409–418. IEEE Computer Society (2011)
Winskel, G.: Distributed probabilistic and quantum strategies. In: Proc. MFPS. ENTCS, vol. 298 (2013)
Castellan, S., Clairambault, P., Winskel, G.: Symmetry in concurrent games. In: Proc. LICS (2014)
Asokan, N., Shoup, V., Waidner, M.: Asynchronous protocols for optimistic fair exchange. In: Proc. 1998 IEEE Symp. on Security and Privacy, pp. 86–99 (May 1998)
Menezes, A., van Oorschot, P., Vanstone, S.: Handbook of Applied Cryptography. CRC Press (2001)
Even, S., Goldreich, O., Lempel, A.: A randomized protocol for signing contracts. Commun. ACM 28(6) (June 1985)
Pagnia, H., Gärtner, F.C.: On the impossibility of fair exchange without a trusted third party. Technical report. Darmstadt University of Technology (1999)
Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Petri Nets: Applications and Relationships to Other Models of Concurrency. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1986)
Clairambault, P., Gutierrez, J., Winskel, G.: The winning ways of concurrent games. In: Proc. LICS, IEEE (2012)
Winskel, G.: Event structure semantics for CCS and related languages. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP. LNCS, vol. 140, pp. 561–576. Springer, Heidelberg (1982)
Dolev, D., Yao, A.C.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–207 (1983)
Shmatikov, V., Mitchell, J.C.: Finite-state analysis of two contract signing protocols. TCS 283(2), (2002)
Chadha, R., Kanovich, M., Scedrov, A.: Inductive methods and contract-signing protocols. In: ACM Conference on Computer and Communications Security (2001)
Garay, J.A., Jakobsson, M., MacKenzie, P.D.: Abuse-free optimistic contract signing. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, p. 449. Springer, Heidelberg (1999)
Castellan, S., Hayman, J., Winskel, G.: Strategies as concurrent processes. In: Proceedings of the 30th Conference on the Mathematical Foundations of Programmings Semantics (MFPS XXX), vol. 308, pp. 1–328 (Ocotober 29, 2014)
Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hayman, J. (2014). Interaction and Causality in Digital Signature Exchange Protocols. In: Maffei, M., Tuosto, E. (eds) Trustworthy Global Computing. TGC 2014. Lecture Notes in Computer Science(), vol 8902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45917-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-662-45917-1_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-45916-4
Online ISBN: 978-3-662-45917-1
eBook Packages: Computer ScienceComputer Science (R0)