Advertisement

AnBx: Automatic Generation and Verification of Security Protocols Implementations

  • Paolo ModestiEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9482)

Abstract

The AnBx compiler is a tool for automatic generation of Java implementations of security protocols specified in a simple and abstract model that can be formally verified. In our model-driven development approach, protocols are described in AnBx, an extension of the Alice & Bob notation. Along with the synthesis of consistency checks, the tool analyses the security goals and produces annotations that allow the verification of the generated implementation with ProVerif.

Keywords

Security protocols Java code generation Applied formal methods Verification 

Notes

Acknowledgements

This work was partially supported by the EU FP7 Project no. 318424, “FutureID: Shaping the Future of Electronic Identity” (futureid.eu). The author thanks Michele Bugliesi, Thomas Groß and Sebastian Mödersheim for useful discussions and Bruno Blanchet for his support on the use of the ProVerif tool.

References

  1. 1.
    Avalle, M., Pironti, A., Sisto, R.: Formal verification of security protocol implementations: a survey. Formal Aspects Comput. 26(1), 99–123 (2014)CrossRefGoogle Scholar
  2. 2.
    Mödersheim, S.: Algebraic properties in Alice and Bob notation. In: International Conference on Availability, Reliability and Security (ARES 2009), pp. 433–440 (2009)Google Scholar
  3. 3.
    Bugliesi, M., Modesti, P.: AnBx - security protocols design and verification. In: Armando, A., Lowe, G. (eds.) ARSPA-WITS 2010. LNCS, vol. 6186, pp. 164–184. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  4. 4.
    Modesti, P.: Efficient Java code generation of security protocols specified in AnB/AnBx. In: Mauw, S., Jensen, C.D. (eds.) STM 2014. LNCS, vol. 8743, pp. 204–208. Springer, Heidelberg (2014)Google Scholar
  5. 5.
    Briais, S., Nestmann, U.: A formal semantics for protocol narrations. Theor. Comput. Sci. 389, 484–511 (2007)CrossRefMathSciNetzbMATHGoogle Scholar
  6. 6.
    Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: IEEE Computer Security Foundations Workshop, pp. 0082–0082. IEEE Computer Society (2001)Google Scholar
  7. 7.
    Basin, D., Mödersheim, S., Viganò, L.: OFMC: a symbolic model checker for security protocols. Int. J. Inf. Secur. 4(3), 181–208 (2005)CrossRefGoogle Scholar
  8. 8.
    Modesti, P.: Efficient Java code generation of security protocols specified in AnB/AnBx. Technical report CS-TR-1422, School of Computing Science, Newcastle University (2014)Google Scholar
  9. 9.
    Bellare, M., Garay, J., Hauser, R., Herzberg, A., Krawczyk, H., Steiner, M., Tsudik, G., Van Herreweghen, E., Waidner, M.: Design, implementation, and deployment of the iKP secure electronic payment system. IEEE J. Sel. Areas Commun. 18(4), 611–627 (2000)CrossRefGoogle Scholar
  10. 10.
    Bella, G., Massacci, F., Paulson, L.: Verifying the SET purchase protocols. J. Autom. Reasoning 36(1), 5–37 (2006)CrossRefzbMATHGoogle Scholar
  11. 11.
    Lowe, G.: A hierarchy of authentication specifications. In: CSFW 1997, pp. 31–43. IEEE Computer Society Press (1997)Google Scholar
  12. 12.
    Denker, G., Millen, J.: CAPSL and CIL language design. Technical report SRI-CSL-99-02, SRI International Computer Science Laboratory (1999)Google Scholar
  13. 13.
    Mödersheim, S.: Algebraic properties in Alice and Bob notation (extended version). Technical report RZ3709, IBM Zurich Research Lab (2008)Google Scholar
  14. 14.
    Blanchet, B., Smyth, B., Cheval, V.: ProVerif 1.91: automatic cryptographic protocol verifier, user manual and tutorial (2015)Google Scholar
  15. 15.
    Bruni, A., Modersheim, S., Nielson, F., Nielson, H.R.: Set-pi: set membership pi-calculus. In: IEEE Computer Security Foundations Symposium (CSF), pp. 185–198 (2015)Google Scholar
  16. 16.
    Bugliesi, M., Calzavara, S., Mödersheim, S., Modesti, P.: Security protocol specification and verification with AnBx. Technical report CS-TR-1479, School of Computing Science, Newcastle University (2015)Google Scholar
  17. 17.
    Tobler, B., Hutchison, A.: Generating network security protocol implementations from formal specifications. In: Nardelli, E., Talamo, M. (eds.) Certification and Security in Inter-Organizational E-Service. IFIP On-Line Library in Computer Science, vol. 177, pp. 33–54. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  18. 18.
    Backes, M., Busenius, A., Hriţcu, C.: On the development and formalization of an extensible code generator for real life security protocols. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 371–387. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  19. 19.
    Pironti, A., Pozza, D., Sisto, R.: Formally based semi-automatic implementation of an open security protocol. J. Syst. Softw. 85(4), 835–849 (2012)CrossRefGoogle Scholar
  20. 20.
    Avalle, M., Pironti, A., Pozza, D., Sisto, R.: JavaSPI: a framework for security protocol implementation. Int. J. Secure Softw. Eng. 2(4), 34–48 (2011)CrossRefGoogle Scholar
  21. 21.
    Millen, J., Muller, F.: Cryptographic protocol generation from CAPSL. Technical report SRI-CSL-01-07, SRI International, December 2001Google Scholar
  22. 22.
    Almousa, O., Mödersheim, S., Viganò, L.: Alice and Bob: reconciling formal models and implementation. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Degano Festschrift. LNCS, vol. 9465, pp. 66–85. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  23. 23.
    FutureID Consortium: FutureID Project. http://www.futureid.eu
  24. 24.
    Basin, D., Keller, M., Radomirović, S., Sasse, R.: Alice and Bob meet equational theories. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Meseguer Festschrift. LNCS, vol. 9200, pp. 160–180. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  25. 25.
    Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: 2012 IEEE 25th Computer Security Foundations Symposium (CSF), pp. 78–94. IEEE (2012)Google Scholar
  26. 26.
    Eclipse Foundation: Eclipse IDE. http://www.eclipse.org

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.School of Computing ScienceNewcastle UniversityNewcastle upon TyneUK

Personalised recommendations