B. Blanchet and M. Paiola. Automatic verification of protocols with lists of unbounded length. In Proc. 17th ACM Conference on Computer and Communications Security (CCS'10), pages 573-584. ACM, 2010.

B. Blanchet, M. Abadi, and C. Fournet. Automated Verification of Selected Equivalences for Security Protocols. In Proc. 20th Symposium on Logic in Computer Science (LICS'05), pages 331-340. IEEE Comp. Soc. Press, 2005.

B. Blanchet, B. Smyth, and V. Cheval. ProVerif 1.88: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial, 2013.

F. Böhl and D. Unruh. Symbolic universal composability. In Proc. 26rd Computer Security Foundations Symposium (CSF'13), pages 257-271, 2013.

M. Bond and R. Anderson. API level attacks on embedded systems. IEEE Computer Magazine, pages 67-75, October 2001.

M. Bortolozzo, M. Centenaro, R. Focardi, and G. Steel. Attacking and fixing PKCS#11 security tokens. In Proc. 17th ACM Conference on Computer and Communications Security (CCS'10), pages 260-269. ACM, 2010.

M. Brusò, K. Chatzikokolakis, and J. den Hartog. Formal verification of privacy for rfid systems. In Proc. 23rd Computer Security Foundations Symposium (CSF'10), pages 75-88. IEEE Comp. Soc. Press, 2010.

S. Bursuc, H. Comon-Lundh, and S. Delaune. Associative-commutative deducibility constraints. In Proc. 24th Annual Symposium on Theoretical Aspects of Computer Science (STACS'07), volume 4393 of Lecture Notes in Computer Science, pages 634-645. Springer, 2007.

D. Cadé and B. Blanchet. Proved generation of implementations from computationally-secure protocol specifications. In Proc. 2nd Conference on Principles of Security and Trust (POST'13), volume 7796 of Lecture Notes in Computer Science, pages 63-82. Springer, 2013.

R. Canetti. Universally composable security: A new paradigm for cryptographic protocols. In Proc. 42nd IEEE Symp. on Foundations of Computer Science (FOCS'01), pages 136-145. IEEE Comp. Soc. Press, 2001.

R. Chadha, S. Ciobăcă, and S. Kremer. Automated verification of equivalence properties of cryptographic protocols. In Programming Languages and Systems —Proc. 21th European Symposium on Programming (ESOP'12), volume 7211 of Lecture Notes in Computer Science, pages 108-127. Springer, 2012.

S. Chaki and A. Datta. Aspier: An automated framework for verifying security protocol implementations. In Proc. 22nd Computer Security Foundations Symposium (CSF'09), pages 172-185. IEEE Comp. Soc. Press, 2009.
V. Cheval. Automatic verification of cryptographic protocols: privacy-type properties. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2012.

V. Cheval. Apte: an algorithm for proving trace equivalence. In Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), volume 8413 of Lecture Notes in Computer Science, pages 587-592. Springer, 2014.

V. Cheval, H. Comon-Lundh, and S. Delaune. Trace equivalence decision: Negative tests and non-determinism. In Proc. 18th ACM Conference on Computer and Communications Security (CCS'11), pages 321-330. ACM, 2011.

V. Cheval, V. Cortier, and A. Plet. Lengths may break privacy – or how to check for equivalences with length. In Proc. 25th International Conference on Computer Aided Verification (CAV'13), volume 8043 of Lecture Notes in Computer Science, pages 708-723. Springer, 2013.

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

T. Chothia and V. Smirnov. A traceability attack against e-passports. In Proc. 14th International Conference on Financial Cryptography and Data Security (FC'10), volume 6052 of Lecture Notes in Computer Science, pages 20-34. Springer, 2010.

N. Chridi, M. Turuani, and M. Rusinowitch. Decidable analysis for a class of cryptographic group protocols with unbounded lists. In Proc. 22nd Computer Security Foundations Symposium (CSF'09), pages 277-289. IEEE Comp. Soc. Press, 2009.

Ş. Ciobâcă, S. Delaune, and S. Kremer. Computing knowledge in security protocols under convergent equational theories. Journal of Automated Reasoning, 48(2):219-262, 2012.

H. Comon-Lundh and V. Shmatikov. Intruder deductions, constraint solving and insecurity decision in presence of Exclusive Or. In Proc. 18th Annual IEEE Symposium on Logic in Computer Science (LICS '03), pages 271-280, Los Alamitos, CA, 2003. IEEE Computer Society.

H. Comon-Lundh, V. Cortier, and E. Zălinescu. Deciding security properties for cryptographic protocols. Application to key cycles. ACM Transactions on Computational Logic, 11(2), 2010.
R. Corin and S. Etalle. An improved constraint-based system for the verification of security protocols. In Proc. 9th International Static Analysis Symposium (SAS'02), volume 2477 of Lecture Notes in Computer Science, pages 326–341. Springer, 2003.

R. Corin, J. Doumen, and S. Etalle. Analysing password protocol security against off-line dictionary attacks. ENTCS, 121:47–63, 2005.

R. Corin, S. Etalle, and A. Saptawijaya. A logic for constraint-based security protocol analysis. In Proc. IEEE Symposium on Security and Privacy (SP'06), pages 155–168. IEEE Comp. Soc. Press, 2006.

V. Cortier and S. Delaune. Decidability and combination results for two notions of knowledge in security protocols. Journal of Automated Reasoning, 48, 2012.

V. Cortier and S. Kremer, editors. Formal Models and Techniques for Analyzing Security Protocols, volume 5 of Cryptology and Information Security Series. IOS Press, 2011.

V. Cortier, S. Kremer, and B. Warinschi. A survey of symbolic methods in computational analysis of cryptographic systems. Journal of Automated Reasoning, 46(3-4):225–259, 2010.

C. Cremers. The Scyther Tool: Verification, falsification, and analysis of security protocols. In Proc. 20th International Conference on Computer Aided Verification (CAV'08), volume 5123 of Lecture Notes in Computer Science, pages 414–418. Springer, 2008.

M. D. Davis and E. J. Weyuker. Computability, complexity and languages, chapter 7, pages 128–132. Computer Science and Applied Mathematics. Academic Press, 1983.

H. de Nivelle. Ordering Refinements of Resolution. PhD thesis, Technische Universiteit Delft, 1995.

S. Delaune and F. Jacquemard. A decision procedure for the verification of security protocols with explicit destructors. In Proc. 11th ACM Conference on Computer and Communications Security (CCS'04), pages 278–287. ACM, 2004.

S. Delaune and F. Jacquemard. Decision procedures for the security of protocols with probabilistic encryption against offline dictionary attacks. Journal of Automated Reasoning, 36(1-2):85–124, 2006.
S. Delaune, S. Kremer, and O. Pereira. Simulation based security in the applied pi calculus. In Proc. 29th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'09), volume 4 of Leibniz International Proceedings in Informatics, pages 169–180. Leibniz-Zentrum für Informatik, 2009a.

S. Delaune, S. Kremer, and M. D. Ryan. Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security, 17(4):435–487, 2009b.

S. Delaune, S. Kremer, and M. D. Ryan. Symbolic bisimulation for the applied pi calculus. Journal of Computer Security, 18(2):317–377, 2010a.

S. Delaune, S. Kremer, and G. Steel. Formal analysis of PKCS#11 and proprietary extensions. Journal of Computer Security, 18(6):1211–1245, 2010b.

S. Delaune, S. Kremer, M. D. Ryan, and G. Steel. Formal analysis of protocols based on TPM state registers. In Proc. 24th IEEE Computer Security Foundations Symposium (CSF'11), pages 66–82. IEEE Press, 2011.

S. Delaune, S. Kremer, and D. Pasaila. Security protocols, constraint systems, and group theories. In Proc. 6th International Joint Conference on Automated Reasoning (IJCAR'12), volume 7364 of Lecture Notes in Artificial Intelligence, pages 164–178. Springer, 2012.

W. Diffie and M. Helman. New directions in cryptography. IEEE Transactions on Information Society, 22(6):644–654, 1976.

D. Dolev and A.C. Yao. On the security of public key protocols. In Proc. 22nd Symposium on Foundations of Computer Science, pages 350–357. IEEE Comp. Soc. Press, 1981.

H. Dong, N. and Jonker and J. Pang. Analysis of a receipt-free auction protocol in the applied pi calculus. In Proc. International Workshop on Formal Aspects in Security and Trust (FAST'10), volume 6561 of Lecture Notes in Computer Science, pages 223–238. Springer, 2011.

J. Dreier, P. Lafourcade, and Y. Lakhnech. Formal verification of e-auction protocols. In Proc. 2nd Conferences on Principles of Security and Trust (POST'13), volume 7796 of Lecture Notes in Computer Science, pages 247–266. Springer, 2013.

F. Dupressoir, A. D. Gordon, J. Jürjens, and D. A. Naumann. Guiding a general-purpose c verifier to prove cryptographic protocols. In Proc. 24th Computer Security Foundations Symposium (CSF'11), pages 3–17. IEEE Comp. Soc. Press, 2011.
N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In *Proc. Workshop on Formal Methods and Security Protocols*, 1999.

S. Escobar, C. Meadows, and J. Meseguer. Maude-npa: Cryptographic protocol analysis modulo equational properties. In *Foundations of Security Analysis and Design V*, volume 5705 of *Lecture Notes in Computer Science*, pages 1–50. Springer, 2009.

R. Focardi and M. Maffei. *Formal Models and Techniques for Analyzing Security Protocols*, chapter Types for Security Protocols. Volume 5 of Cortier and Kremer [2011], 2011.

R. Focardi and F. Martinelli. A uniform approach for the definition of security properties. In *Proc. World Congress on Formal Methods (FM'99)*, Lecture Notes in Computer Science, pages 794–813. Springer, 1999.

A. Fujioka, T. Okamoto, and K. Ohta. A practical secret voting scheme for large scale elections. In *Advances in Cryptology - AUSCRYPT'92*, volume 718 of *Lecture Notes in Computer Science*, pages 244–251. Springer-Verlag, 1992.

Th. Genet and F. Klay. Rewriting for cryptographic protocol verification. In *Proc. 17th International Conference on Automated Deduction (CADE'00)*, volume 1831 of *Lecture Notes in Computer Science*, pages 271–290. Springer, 2000.

S. Goldwasser and S. Micali. Probabilistic encryption. *Journal of Computer and System Sciences*, 28, 1984.

D. Gollmann. What do we mean by entity authentication? In *Proc. Symposium on Security and Privacy (SP'96)*, pages 46–54. IEEE Comp. Soc. Press, 1996.

J. Goubault-Larrecq. A method for automatic cryptographic protocol verification (extended abstract). In *Proc. Workshops of the 15th International Parallel and Distributed Processing Symposium*, volume 1800 of *Lecture Notes in Computer Science*, pages 977–984. Springer, 2000.

J. Goubault-Larrecq and F. Parrennes. Cryptographic protocol analysis on real C code. In *Proc. 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05)*, volume 3385 of *Lecture Notes in Computer Science*, pages 363–379. Springer, 2005.

ISO/IEC-9798-1. *Information technology - Security techniques - Entity authentication mechanisms; Part 1: General model*. ISO/IEC 9798-1. International Organization for Standardization, second edition, sep 1991.
F. Jacquemard, M.Rusinowitch, and L. Vigneron. Compiling and verifying security protocols. In Proc. 7th International Conference on Logic for Programming and Automated Reasoning (LPAR'00), volume 1955 of Lecture Notes in Computer Science, pages 131-160. Springer, 2000.

S. Kremer and R. Künnemann. Automated analysis of security protocols with global state. In Proceedings of the 35th IEEE Symposium on Security and Privacy (SP'14), pages 163-178. IEEE Comp. Soc. Press, 2014.

S. Kremer and L. Mazaré. Adaptive soundness of static equivalence. In Proc. 12th European Symposium on Research in Computer Security (ESORICS'07), volume 4734 of Lecture Notes in Computer Science, pages 610-625. Springer, 2007.

S. Kremer and M. D. Ryan. Analysis of an electronic voting protocol in the applied pi-calculus. In Programming Languages and Systems — Proc. 14th European Symposium on Programming (ESOP'05), volume 3444 of Lecture Notes in Computer Science, pages 186-200. Springer, 2005.

S. Kremer, A. Mercier, and R. Treinen. Reducing equational theories for the decision of static equivalence. Journal of Automated Reasoning, 48(2): 197-217, 2012.

R. Küsters, T. Truderung, and J. Graf. A framework for the cryptographic verification of java-like programs. In Proc. 25th Computer Security Foundations Symposium (CSF'12), pages 198-212. IEEE Comp. Soc. Press, 2012.

D. Longley and S. Rigby. An automatic search for security flaws in key management schemes. Computers and Security, 11(1):75-89, March 1992.

G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proc. 2nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96), volume 1055 of Lecture Notes in Computer Science, pages 147-166. Springer-Verlag, 1996.

G. Lowe. A hierarchy of authentication specifications. In Proc. 10th Computer Security Foundations Workshop (CSFW'97), pages 31-44. IEEE Comp. Soc. Press, 1997a.

G. Lowe. Casper: a compiler for the analysis of security protocols. In Proc. 10th Computer Security Foundations Workshop (CSFW'97), pages 18-30. IEEE Comp. Soc. Press, 1997b.

G. Lowe. Analysing protocols subject to guessing attacks. Journal of Computer Security, 12(1):83-98, 2004.

C. Meadows. The NRL protocol analyzer: An overview. Journal of Logic Programming, 26(2):113-131, 1996.

J. Millen. A necessarily parallel attack. In FMSP '99, 1999.
J. Millen and G. Denker. Capsl and mucapsl. *J. Telecommunications and Information Technology*, 4:16–27, 2002.

J. Millen and V. Shmatikov. Constraint solving for bounded-process cryptographic protocol analysis. In *Proc. 8th ACM Conference on Computer and Communications Security (CCS'01)*, 2001.

J. C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using Murmur. In *Proc. IEEE Symposium on Security and Privacy (SP'97)*, pages 141–153, 1997.

S. Mödersheim. Abstraction by set-membership: verifying security protocols and web services with databases. In *Proc. 17th ACM Conference on Computer and Communications Security (CCS'10)*, pages 351–360. ACM, 2010.

D. Monniaux. Abstracting cryptographic protocols with tree automata. *Sci. Comput. Program.*, 47(2-3):177–202, 2003.

R. M. Needham and M. D. Schroeder. Using encryption for authentication in large networks of computers. *Communications of the ACM*, 21(12):993–999, 1978.

L. C. Paulson. Mechanized proofs for a recursive authentication protocol. In *Proc. 10th Computer Security Foundations Workshop (CSFW'97)*, pages 84–95. IEEE Comp. Soc. Press, 1997.

L. C. Paulson. The inductive approach to verifying cryptographic protocols. *Journal of Computer Security*, 6(1/2):85–128, 1998.

Alfredo Pironti and Riccardo Sisto. Provably correct Java implementations of Spi Calculus security protocols specifications. *Computers & Security*, 29: 302–314, 2010.

M. Rusinowitch and M. Turuani. Protocol insecurity with finite number of sessions is NP-complete. In *Proc. 14th Computer Security Foundations Workshop (CSFW'01)*, pages 174–190. IEEE Comp. Soc. Press, 2001.

M. Rusinowitch and M. Turuani. Protocol Insecurity with Finite Number of Sessions and Composed Keys is NP-complete. *Theoretical Computer Science*, 299:451–475, 2003.

P.Y.A Ryan, S.A. Schneider, M. Goldsmith, G. Lowe, and A.W. Roscoe. *Modelling and Analysis of Security Protocols*. Addison Wesley, 2000.

B. Schmidt, S. Meier, C. Cremers, and D. Basin. Automated analysis of Diffie-Hellman protocols and advanced security properties. In *Proc. 25th IEEE Computer Security Foundations Symposium (CSF'12)*, pages 78–94. IEEE Comp. Soc. Press, 2012.
B. Schmidt, S. Meier, C. Cremers, and D. Basin. The tamarin prover for the symbolic analysis of security protocols. In Proc. 25th International Conference on Computer Aided Verification (CAV'13), volume 8044 of Lecture Notes in Computer Science, pages 696-701. Springer, 2013.

S. Schneider. Verifying authentication protocols with CSP. In Proc. 10th Computer Security Foundations Workshop (CSFW'97). IEEE Comp. Soc. Press, 1997.

D. Song. Athena, an automatic checker for security protocol analysis. In Proc. 12th IEEE Computer Security Foundations Workshop (CSFW'99). IEEE Comp. Soc. Press, 1999.

J. Thayer, J. Herzog, and J. Guttman. Strand spaces: proving security protocols correct. IEEE Journal of Computer Security, 7:191-230, 1999.

A. Tiu and J. Dawson. Automating open bisimulation checking for the spi-calculus. In Proc. 23rd Computer Security Foundations Symposium (CSF'10), pages 307-321. IEEE Comp. Soc. Press, 2010.

T. Truderung. Selecting theories and recursive protocols. In Proc. 16th International Conference on Concurrency Theory (Concur'05), volume 3653 of Lecture Notes in Computer Science, pages 217-232. Springer, 2005.

Ch. Weidenbach. Towards an automatic analysis of security protocols in first-order logic. In Proc. 16th International Conference on Automated Deduction (CADE'99), volume 1632 of Lecture Notes in Computer Science, pages 314-328. Springer, 1999.

T.Y.C. Woo and S.S. Lam. Authentication for distributed systems. In Proc. Symposium on Security and Privacy (SP'92), pages 178-194. IEEE Comp. Soc. Press, 1992.