Abstract
The aim of this work is to obtain an interactive proof environment based on Isabelle/HOL for reasoning formally about cryptographic protocols, expressed as processes of the spi calculus (a π-calculus with cryptographic primitives). To this end, we formalise syntax, semantics, and hedged bisimulation, an environment-sensitive bisimulation which can be used for proving security properties of protocols. In order to deal smoothly with binding operators and reason up-to α-equivalence of bound names, we adopt the new Nominal datatype package. This simplifies both the encoding, and the formal proofs, which turn out to correspond closely to “manual proofs”.
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
Abadi, M., Gordon, A.D.: A bisimulation method for cryptographic protocols. Nord. J. Comput. 5(4), 267 (1998)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The Spi calculus. Journal of Information and Computation 148(1), 1–70 (1999)
Armando, A., Basin, D.A., Boichut, Y., Chevalier, Y., Compagna, L., Cuéllar, J., Drielsma, P.H., Héam, P.-C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Bengtson, J., Parrow, J.: Formalising the π-calculus using nominal logic. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 63–77. Springer, Heidelberg (2007)
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., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: Proc. 20th LICS, pp. 331–340. IEEE (2005)
Boreale, M., Nicola, R.D., Pugliese, R.: Proof techniques for cryptographic processes. SIAM J. Comput. 31(3), 947–986 (2001)
Borgström, J., Briais, S., Nestmann, U.: Symbolic bisimulation in the spi calculus. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 161–176. Springer, Heidelberg (2004)
Borgström, J., Nestmann, U.: On bisimulations for the spi calculus. Mathematical Structures in Computer Science 15(3), 487–552 (2005)
Clarke, E.M., Jha, S., Marrero, W.: Verifying security protocols with brutus. ACM Trans. Softw. Eng. Methodol. 9(4), 443–487 (2000)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax involving binders. In: Proc. 14th LICS, pp. 214–224. IEEE (1999)
Hirschkoff, D.: Bisimulation proofs for the π-calculus in the Calculus of Constructions. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275. Springer, Heidelberg (1997)
Honsell, F., Miculan, M., Scagnetto, I.: π-calculus in (co)inductive type theory. Theoretical Computer Science 253(2), 239–285 (2001)
Hüttel, H.: Deciding framed bisimilarity. In: Proceedings of Infinity 2002. Electronic Notes in Theoretical Computer Science, vol. 68, pp. 1–18 (2003)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Inform. and Comput. 100(1), 1–77 (1992)
Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murφ. In: IEEE Symposium on Security and Privacy, pp. 141–151. IEEE Computer Society (1997)
Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2–13. Springer, Heidelberg (2001)
Nipkow, T., Paulson, L.C.: Isabelle-91. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 673–676. Springer, Heidelberg (1992)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1-2), 85–128 (1998)
Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 186, 165–193 (2003)
Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. In: Proc. LICS, pp. 293–302. IEEE Computer Society (2007)
Urban, C., Tasson, C.: Nominal techniques in Isabelle/HOL. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 38–53. Springer, Heidelberg (2005)
Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167–184. Springer, Heidelberg (1999)
Yu, S., Luo, Z.: Implementing a model checker for LEGO. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 442–458. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kahsai, T., Miculan, M. (2008). Implementing Spi Calculus Using Nominal Techniques. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds) Logic and Theory of Algorithms. CiE 2008. Lecture Notes in Computer Science, vol 5028. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69407-6_33
Download citation
DOI: https://doi.org/10.1007/978-3-540-69407-6_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69405-2
Online ISBN: 978-3-540-69407-6
eBook Packages: Computer ScienceComputer Science (R0)