Skip to main content
SpringerLink
Log in

Alice and Bob: Reconciling Formal Models and Implementation

  • Chapter
  • First Online:
Programming Languages with Applications to Biology and Security

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9465))

Abstract

This paper defines the “ultimate” formal semantics for Alice and Bob notation, i.e., what actions the honest agents have to perform, in the presence of an arbitrary set of cryptographic operators and their algebraic theory. Despite its generality, this semantics is mathematically simpler than any previous attempt. For practical applicability, we introduce the language SPS and an automatic translation to robust real-world implementations and corresponding formal models, and we prove this translation correct with respect to the semantics.

This work was partially supported by the EU FP7 Projects no. 318424, “FutureID: Shaping the Future of Electronic Identity” (futureid.eu), and by the PRIN 2010–2011 Project “Security Horizons”.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We have learned that from Pierpaolo Degano, who is renowned for his ability to explain complex things in a simple way.

  2. 2.

    We use \(\mathtt {p}\) instead of \(\mathtt {i}\) in honor of our “favorite intruder” Pierpaolo.

  3. 3.

    One may employ an entirely different model for the intruder (e.g., a cryptographic one); using a Dolev-Yao style deduction for honest agents is simply the semantic decision that they perform only standard public operations (that would be part of a crypto API), but no operations that would amount to cryptographic attacks.

  4. 4.

    One may argue that JavaScript is not suitable for implementing security protocols, but in fact, using systematic mechanisms such as our formats, we can produce robust implementations that do not suffer from type flaw attacks, for instance. It is relatively easy to adapt to other languages like Java or the AVANTSSAR Platform [5], e.g., for using the tool OFMC, for which we have implemented a connector.

  5. 5.

    Interestingly also the Festschrift for José Meseguer this year received a treatment of Alice and Bob notation [7] that is very similar to our low-level semantics \([\![\cdot ]\!]_L\), however cannot handle exponentiation and multiplication. Thus, we can conclude that Pierpaolo received a strictly stronger Festschrift.

References

  1. Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoret. Comput. Sci. 367(1–2), 2–32 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  2. Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL, pp. 104–115. ACM (2001)

    Google Scholar 

  3. Almousa, O., Mödersheim, S., Modesti, P., Viganò, L.: Typing and Compositionality for Security Protocols: A Generalization to the Geometric Fragment. In: ESORICS 2015, 2015, to appear, http://compute.dtu.dk/~samo

  4. Almousa, O., Mödersheim, S., Viganò, L.: Alice and Bob: reconciling formal models and implementation (Extended Version). Technical report 2014-10, DTU Compute (2015). http://www.imm.dtu.dk/~samo/

  5. Armando, A., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267–282. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. Hriţcu, C., Busenius, A., Backes, M.: 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)

    Chapter  Google Scholar 

  7. Basin, D., Keller, M., Radomirović, S., Sasse, R.: Alice and Bob meet equational theories. In: Festschrift for José Meseguer on his 65th Birthday (2015)

    Google Scholar 

  8. Bhargavan, K., Fournet, C., Corin, R., Zălinescu, E.: Verified cryptographic implementations for TLS. ACM Trans. Inf. Syst. Secur. 15, 1 (2012). Article 3

    Article  Google Scholar 

  9. Bhargavan, K., Fournet, C., Gordon, A.D., Tse, S.: Verified interoperable implementations of security protocols. In: CSF 19, pp. 139–152. IEEE (2006)

    Google Scholar 

  10. Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSF, pp. 82–96. IEEE (2001)

    Google Scholar 

  11. Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Riis Nielson, H.: Static validation of security protocols. J. Comput. Secur. 13(3), 347–390 (2005)

    Article  MATH  Google Scholar 

  12. Briais, S., Nestmann, U.: A formal semantics for protocol narrations. Theoret. Comput. Sci. 389(3), 484–511 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  13. Caleiro, C., Viganò, L., Basin, D.: On the semantics of Alice&Bob specifications of security protocols. Theoret. Comput. Sci. 367(1), 88–122 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  14. Chevalier, Y., Rusinowitch, M.: Compiling and securing cryptographic protocols. Inf. Process. Lett. 110(3), 116–122 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  15. Cremers, C.J.F., Mauw, S.: Operational semantics of security protocols. In: Leue, S., Systä, T.J. (eds.) Scenarios: Models, Transformations and Tools. LNCS, vol. 3466, pp. 66–89. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  16. Dierks, T., Rescorla, E.: RFC 5246: The Transport Layer Security (TLS) Protocol, Version 1.2 (2008)

    Google Scholar 

  17. FutureID Project: Deliverable D42.6: Specification of execution environment (2014). www.futureid.eu

  18. FutureID Project: Deliverable D42.8: APS Files for Selected Authentication Protocols (2015). www.futureid.eu

  19. German Federal Office for Information Security (BSI): Advanced Security Mechanism for Machine Readable Travel Documents (2008). www.bsi.bund.de/EN/Publications/TechnicalGuidelines/TR03110/BSITR03110

  20. Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and verifying security protocols. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 131–160. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  21. Küsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: CSF, pp. 157–171. IEEE (2009)

    Google Scholar 

  22. Lowe, G.: Casper: a compiler for the analysis of security protocols. In: CSFW, pp. 18–30. IEEE (1997)

    Google Scholar 

  23. Millen, J.: CAPSL: common authentication protocol specification language. Technical report, Technical Report MP 97B48, The MITRE Corporation (1997)

    Google Scholar 

  24. Mödersheim, S.: Algebraic properties in Alice and Bob notation. In: ARES 2009, pp. 433–440. IEEE (2009)

    Google Scholar 

  25. Mödersheim, S.: Diffie-Hellman without difficulty. In: Barthe, G., Datta, A., Etalle, S. (eds.) FAST 2011. LNCS, vol. 7140, pp. 214–229. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  26. Mödersheim, S., Katsoris, G.: A sound abstraction of the parsing problem. In: CSF, pp. 259–273. IEEE (2014)

    Google Scholar 

  27. Modesti, P.: Efficient Java code generation of security protocols specified in AnB/AnBx. In: STM (2014)

    Google Scholar 

  28. Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7(1), 191–230 (1999)

    Article  Google Scholar 

  29. Tobler, B., Hutchison, A.C.: Generating network security protocol implementations from formal specifications. In: Nardelli, E., Talamo, M. (eds.) Certification and Security in Inter-Organizational E-Service. IFIP, vol. 177, pp. 33–54. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DTU Compute, Lyngby, Denmark

    Omar Almousa & Sebastian Mödersheim

  2. Department of Informatics, King’s College London, London, UK

    Luca Viganò

Authors
  1. Omar Almousa
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sebastian Mödersheim
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Luca Viganò
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Luca Viganò .

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Pisa, Pisa, Italy

    Chiara Bodei

  2. Dipartimento di Informatica, Università di Pisa, Pisa, Italy

    Gianluigi Ferrari

  3. Università degli Studi di Trento, Povo, Italy

    Corrado Priami

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Almousa, O., Mödersheim, S., Viganò, L. (2015). Alice and Bob: Reconciling Formal Models and Implementation. 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_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-25527-9_7

  • 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)

Publish with us

Policies and ethics

Search

Navigation