Literature list for Seminar Formal Models and Techniques for Analyzing Security Protocols

The tutorial we follow is Formal Models and Techniques for Analyzing Security Protocols: A Tutorial by Véronique Cortier and Steve Kremer.

For the hands-on session , refer to this document with instructions.

Chapters

  1. Intro & running example (Hizbullah)
  2. Messages and deduction (Robert)
  3. Equational theory and static equivalence (Matthias)
  1. A cryptographic process calculus (Siavash)
    • Kobeissi, Bhargavan, and Blanchet (2017) .,
      04_signal ,
      Robert
  2. Security properties (Rati)
    • (moved to Chapter: Automated verification: unbounded case)
  1. Automated verification: unbounded case (Sven)
    • Blanchet, Abadi, and Fournet (2008) ,
      05_diffeq ,
      Hizbullah
  2. Automated verification: bounded case (Alexander)
  3. Further readings and conclusion
    • Bhargavan, Blanchet, and Kobeissi (2017) ,
      07_tls ,
      Rati

Skipped:

  • Dreier et al. (2015) ,
    05_exams ,
    Robert
  • Babel, Cheval, and Kremer (2017) ,
    05_comm ,
    (for fun)

References

Abadi, Martin, and Phillip Rogaway. 2002. “Reconciling Two Views of Cryptography (the Computational Soundness of Formal Encryption).” Journal of Cryptology 15 (2). Springer: 103–27.

Abadi, Martín, and Véronique Cortier. 2006. “Deciding Knowledge in Security Protocols Under Equational Theories.” Theoretical Computer Science 367 (1-2). Elsevier: 2–32.

Babel, Kushal, Vincent Cheval, and Steve Kremer. 2017. “On Communication Models When Verifying Equivalence Properties.” In International Conference on Principles of Security and Trust , 141–63. Springer.

Bhargavan, Karthikeyan, Bruno Blanchet, and Nadim Kobeissi. 2017. “Verified Models and Reference Implementations for the Tls 1.3 Standard Candidate.” In IEEE Symposium on Security and Privacy (S&P’17) . San Jose, CA: IEEE.

Blanchet, Bruno, Martín Abadi, and Cédric Fournet. 2008. “Automated Verification of Selected Equivalences for Security Protocols.” The Journal of Logic and Algebraic Programming 75 (1). Elsevier: 3–51.

Cheval, Vincent. 2014. “Apte: An Algorithm for Proving Trace Equivalence.” In International Conference on Tools and Algorithms for the Construction and Analysis of Systems , 587–92. Springer.

Cheval, Vincent, Véronique Cortier, and Antoine Plet. 2013. “Lengths May Break Privacy–or How to Check for Equivalences with Length.” In International Conference on Computer Aided Verification , 708–23. Springer.

Comon-Lundh, Hubert, and Stéphanie Delaune. 2005. “The Finite Variant Property: How to Get Rid of Some Algebraic Properties.” In International Conference on Rewriting Techniques and Applications , 294–307. Springer.

Dreier, Jannik, Rosario Giustolisi, Ali Kassem, Pascal Lafourcade, and Gabriele Lenzini. 2015. “A Framework for Analyzing Verifiability in Traditional and Electronic Exams.” In Information Security Practice and Experience , 514–29. Springer.

Kobeissi, Nadim, Karthikeyan Bhargavan, and Bruno Blanchet. 2017. “Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach.” In 2nd Ieee European Symposium on Security and Privacy (Euros&P’17) . Paris, France: IEEE.

Lowe, Gavin. 1996. “Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR.” In Proc. 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS’96) , 1055:147–66. Lncs. Springer.

Needham, Roger M, and Michael D Schroeder. 1978. “Using Encryption for Authentication in Large Networks of Computers.” Communications of the ACM 21 (12). ACM: 993–99.

Impressum ● Data Privacy Policy ● Sitemap ● ©  2019 Information Security & Cryptography Group