Abstract
Control Flow Analysis (CFA) has been proven successful for the analysis of cryptographic protocols. Due to its over-approximative nature, the absence of detected flaws implies their absence also at run time, while their presence only says that there is the possibility for flaws to occur. Nevertheless, the static detection of a flaw can be considered as a warning bell that alerts against a possible attack, of which the flaw is the result. Reconstructing the possible attack leading to the detected flaw is not trivial, though. We propose a CFA enriched with causal information that accounts for attacker activity. In case a flaw is predicted, the causal information provides a sort of climbing holds that can be escalated to reconstruct the attack sequence leading to the flaw.
This work has been partially supported by the MIUR PRIN project Security Horizons.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
i.e. whenever there exist no Q, \(Q'\) such that \(P \rightarrow ^* Q \rightarrow Q'\) and \(P \rightarrow _{\mathsf {RM}}^* Q \ /\rightarrow _{\mathsf {RM}} \), where \(*\) stands for the transitive and reflexive closure of the relation, and \(Q \ /\rightarrow _{\mathsf {RM}} \) stands for \(\lnot \exists Q': Q \rightarrow _{\mathsf {RM}}Q'\).
- 2.
Where the tuples produced by the attacker or due to its messages and the histories of interest are indigo in the pdf.
References
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols - the Spi Calculus. Inf. Comput. 148(1), 1–70 (1999)
Allamigeon, X., Blanchet, B.: Reconstruction of attacks against cryptographic protocols. In: 18th IEEE Computer Security Foundations Workshop, (CSFW-18 2005), pp. 140–154 (2005)
Backes, M., Cortesi, A., Maffei, M.: Causality-based abstraction of multiplicity in security protocols. In: IEEE Computer Security Foundations Symposium (CSF’07), pp. 355–369 (2007)
Bodei, C., Brodo, L., Degano, P., Gao, H.: Detecting and preventing type flaws at static time. J. Comput. Secur. 18(2), 229–264 (2010)
Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Nielson, H.R.: Static validation of security protocols. Inf. Comput. 13(3), 347–390 (2005)
Buchholtz, M., Maidl, M., Bodei, C., Degano, P., Priami, C.: Deliverable D14, Final Report on Static Techniques. Technical report, Project DEGAS IST-2001-32072 (2004)
Buchholtz, M., Nielson, F., Nielson, H.R.: A calculus for control flow analysis of security protocols. Int. J. Inf. Secur. 2(3–4), 157–167 (2004)
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Trans. Comput. Syst. 8, 18–36 (1990)
Crazzolara, F., Winskel, G.: Events in security protocols. In: Proceedings of the 8th ACM Conference on Computer and Communications Security (CCS 2001), pp. 96–105 (2001)
Degano, P., Priami, C.: Non-interleaving semantics for mobile processes. Theor. Comput. Sci. 216(1–2), 237–270 (1999)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theor. IT–29(12), 198–208 (1983)
Gao, H., Bodei, C., Degano, P.: A formal analysis of complex type flaw attacks on security protocols. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 167–183. Springer, Heidelberg (2008)
Gao, H., Bodei, C., Degano, P., Nielson, H.R.: A formal analysis for capturing replay attacks in cryptographic protocols. In: Cervesato, I. (ed.) ASIAN 2007. LNCS, vol. 4846, pp. 150–165. Springer, Heidelberg (2007)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes (I and II). Inf. Comput. 100(1), 1–77 (1992)
Nielsen, C.R., Nielson, F., Nielson, H.R.: Cryptographic pattern matching. Electr. Notes Theor. Comput. Sci. 168, 91–107 (2007)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)
Sewell, P., Vitek, J.: Secure composition of untrusted code: box pi, wrappers, and causality. J. Comput. Secur. 11(2), 135–188 (2003)
Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7(1), 191–230 (1999)
Acknowledgements
We would like to thank Mikael Bucholtz, Hanne Riis Nielson, Flemming Nielson and, in particular, Pierpaolo Degano for the many valuable discussions on CFA, on LySa, and on other issues. Some of the ideas developed here have their roots in those discussions. Furthermore, we thank our anonymous referees for their useful comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Bodei, C., Brodo, L., Focardi, R. (2015). Static Evidences for Attack Reconstruction. In: Bodei, C., Ferrari, G., Priami, C. (eds) Programming Languages with Applications to Biology and Security. Lecture Notes in Computer Science(), vol 9465. Springer, Cham. https://doi.org/10.1007/978-3-319-25527-9_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-25527-9_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-25526-2
Online ISBN: 978-3-319-25527-9
eBook Packages: Computer ScienceComputer Science (R0)