Abstract
Many security properties of cryptographic protocols can be expressed by using information flow policies as non-interference. But, in general it is very difficult to design a system without interference. For that, many works try to weak the standard definition of the non-interference. For instance, in [21] Mullins defines the admissible interference as an interference that admits flow information only through a dowgrader. Thus, we present in this paper a type system that try to detect process that allow interference. Then, if we can type a process we can say that is free interference. Also, we extend the type system of process with another type system based on a standard message algebra used in the literature of cryptographic protocols. So, we define the theoric characterization, prove the correctness of our type system and present an illustration of our result.
Chapter PDF
Similar content being viewed by others
Keywords
References
Piazza, C., Bossi, A., Rossi, S.: Modelling downgrading in information flow security. In: Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW 2004), p. 187. IEEE Computer Society, Los Alamitos (2004)
Sabelfeld, A., Myers, A.C., Zdancewic, S.: Enforcing robust declassification. In: Proceedings of the 17th IEEE Computer Security Foundations Workshop, June 2004, pp. 172–186 (2004)
Abadi, M., Gordon, A.D.: A Calculus for Cryptographic Protocols: The Spi Calculus. In: Proceedings of the Fourth ACM Conference on Computer and Communications Security, April 1997. ACM Press, New York (1997)
Abadi, M.: Secrecy by typing in security protocols. J. ACM 46(5), 749–786 (1999)
Bella, G.: Inductive Verification of Cryptographic Protocols. PhD thesis, University of Cambridge (March 2000)
Boudol, G.: Asynchrony and the π-calulus. Technical report, INRIA-Sophia Antipolis (1992)
Buttyán, L.: Formal methods in the design of cryptographic protocols. Technical Report SSC/1999/038, Institute for computer Communications and Applications (November 1999)
Carlsen, U.: Cryptographic Protocol Flaws. In: Proceedings of the IEEE Computer Security Foundations Workshop VII, Franconia, June 1994, pp. 192–200. IEEE, Los Alamitos (1994)
Conchon, S.: Modular information flow analysis for process calculi. In: Proc. of Foundations of Computer Security, pp. 23–34 (2002)
Focardi, R., Gorrieri, R.: Classification of Security Properties (Part I: Information Flow). In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)
Giacobazzi, R., Mastroeni, I.: Abstract non-interference: parameterizing non-interference by abstract interpretation. In: POPL 2004: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 186–197. ACM Press, New York (2004)
Goguen, J.A., Meseguer, J.: Security Policies and Security Models. In: Proceedings of the 1982 IEEE Symposium on Research in Security and Privacy, April 1982, pp. 11–20. IEEE press, Los Alamitos (1982)
Hennessy, M.: The Security Picalculus and Non-interference. Journal of Logic and Algebraic Programming (2003) (to appear)
Hennessy, M., Riely, J.: Information flow vs. resource access in the asynchronous π-calculus. ACM Transactions on Programming Languages and Systems 24(5), 566–591 (2002)
Honda, K., Tokoro, M.: On asynchronous communication semantics. In: Proceedings of the ECOOP 1991 Workshop on Object-Based Concurrent Computing, vol. 612, pp. 21–51. Springer, Heidelberg (1992)
Honda, K., Yoshida, N.: A Uniform Type Structure for Secure Information Flow. ACM SIGPLAN Notices 37(1), 81–92 (2002)
Lafrance, S., Mullins, J.: Bisimulation-based non-deterministic admissible interference and its application to the analysis of cryptographic protocols. In: Harland, J. (ed.) Electronic Notes in Theoretical Computer Science, vol. 61. Elsevier Science Publishers, Amsterdam (2002)
Mejri, M., Debbabi, M., Durgin, N.A., Mitchell, J.C.: Security by typing. International Journal on Software Tools for Technology Transfer 4(4), 472–495 (2003)
Meadows, C.: Formal methods for cryptographic protocol analysis: emerging issues and trends (2003)
Mejri, M.: From type theory to the verification of security protocols. PhD thesis, Laval University (February 2001)
Mullins, J.: Nondeterministic Admissible Interference. Journal of Universal Computer Science 6(11), 1054–1070 (2000)
Sabelfeld, A., Myers, A.: Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications 21(1) (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fellah, A., Mullins, J. (2005). Admissible Interference by Typing for Cryptographic Protocols. In: Qing, S., Mao, W., López, J., Wang, G. (eds) Information and Communications Security. ICICS 2005. Lecture Notes in Computer Science, vol 3783. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11602897_11
Download citation
DOI: https://doi.org/10.1007/11602897_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30934-5
Online ISBN: 978-3-540-32099-9
eBook Packages: Computer ScienceComputer Science (R0)