Abstract
Gordon and Jeffrey have proposed a type and effect system for checking authenticity in cryptographic protocols. The type system reduces the protocol verification problem to the type checking problem, but protocols must be manually annotated with non-trivial types and effects. To automate the verification of cryptographic protocols, we modify Gordon and Jeffrey’s type system and develop a type inference algorithm. Key modifications for enabling automated type inference are introduction of fractional effects and replacement of typing rules with syntax-directed ones. We have implemented and tested a prototype protocol verifier based on our type system.
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
Gordon, A.D., Jeffrey, A.: Typing correspondence assertions for communication protocols. Theor. Comput. Sci. 300, 379–409 (2003)
Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. Journal of Computer Security 11(4), 451–520 (2003)
Gordon, A.D., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. In: 15th IEEE Computer Security Foundations Workshop (CSFW-15), pp. 77–91 (2002)
Woo, T.Y., Lam, S.S.: A semantic model for authentication protocols. In: RSP: IEEE Computer Society Symposium on Research in Security and Privacy, pp. 178–193 (1993)
Haack, C., Jeffrey, A.: Cryptyc (2004), http://www.cryptyc.org/
Kikuchi, D., Kobayashi, N.: Type-based verification of correspondence assertions for communication protocols. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 191–205. Springer, Heidelberg (2007)
Gordon, A.D., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. Journal of Computer Security 12(3-4), 435–483 (2004)
Abadi, M., Gordon, A.D.: A Calculus for Cryptographic Protocols: The Spi Calculus. Information and Computation 148(1), 1–70 (1999)
GNU Linear Programming Kit, http://www.gnu.org/software/glpk
Gordon, A.D., HĂĽttel, H., Hansen, R.R.: Type inference for correspondence types. In: 6th International Workshop on Security Issues in Concurrency (SecCo 2008) (2008)
Bugliesi, M., Focardi, R., Maffei, M.: Compositional analysis of authentication protocols. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 140–154. Springer, Heidelberg (2004)
Bugliesi, M., Focardi, R., Maffei, M.: Authenticity by tagging and typing. In: Proceedings of the 2004 ACM Workshop on Formal Methods in Security Engineering (FMSE 2004), pp. 1–12 (2004)
Focardi, R., Maffei, M., Placella, F.: Inferring authentication tags. In: Proceedings of the Workshop on Issues in the Theory of Security (WITS 2005), pp. 41–49 (2005)
Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008), pp. 17–32 (2008)
Blanchet, B.: From Secrecy to Authenticity in Security Protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 342–359. Springer, Heidelberg (2002)
Blanchet, B.: Computationally sound mechanized proofs of correspondence assertions. In: 20th IEEE Computer Security Foundations Symposium (CSF 2007), pp. 97–111 (2007)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)
Terauchi, T., Aiken, A.: Witnessing side-effects. In: Proc. of ICFP, pp. 105–115. ACM, New York (2005)
Terauchi, T., Aiken, A.: A capability calculus for concurrency and determinism. ACM Trans. Prog. Lang. Syst. 30(5) (2008)
Terauchi, T.: Checking race freedom via linear programming. In: Proc. of PLDI, pp. 1–10 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kikuchi, D., Kobayashi, N. (2009). Type-Based Automated Verification of Authenticity in Cryptographic Protocols. In: Castagna, G. (eds) Programming Languages and Systems. ESOP 2009. Lecture Notes in Computer Science, vol 5502. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00590-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-00590-9_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00589-3
Online ISBN: 978-3-642-00590-9
eBook Packages: Computer ScienceComputer Science (R0)