A. Armando, R. Carbone, L. Compagna, J. Cuellar, and L. T. Abad, Formal analysis of saml 2.0 web browser single signon: Breaking the saml-based single sign-on for google apps, Proc. 6th ACM Workshop on Formal Methods in Security Engineering (FMSE'08), pp.1-10, 2008.

M. Bortolozzo, M. Centenaro, R. Focardi, and G. Steel, Attacking and fixing PKCS#11 security tokens, Proceedings of the 17th ACM conference on Computer and communications security, CCS '10, pp.260-269, 2010.
DOI : 10.1145/1866307.1866337

G. Lowe, Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR, Proc. 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS'96), ser. LNCS, pp.147-166, 1996.
DOI : 10.1007/3-540-61042-1_43

B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., pp.82-96, 2001.
DOI : 10.1109/CSFW.2001.930138

A. Armando, D. A. Basin, Y. Boichut, Y. Chevalier, L. Compagna et al., The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, Proc. 17th International Conference on Computer Aided Verification (CAV'05), ser, pp.281-285, 2005.
DOI : 10.1007/11513988_27
URL : https://hal.archives-ouvertes.fr/inria-00000408

S. Escobar, C. Meadows, and J. Meseguer, Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, Foundations of Security Analysis and Design V, ser. LNCS, pp.1-50, 2009.
DOI : 10.1007/s10990-007-9000-6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.226.3197

M. Abadi and C. Fournet, Mobile values, new names, and secure communication, Proc. 28th ACM Symp. on Principles of Programming Languages (POPL'01, pp.104-115, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01423924

M. Arapinis, E. Ritter, and M. Ryan, Statverif: Verification of stateful processes, Proc. 24th IEEE Computer Security Foundations Symposium (CSF'11, pp.33-47, 2011.

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

S. Delaune, S. Kremer, M. D. Ryan, and G. Steel, Formal Analysis of Protocols Based on TPM State Registers, 2011 IEEE 24th Computer Security Foundations Symposium, pp.66-82, 2011.
DOI : 10.1109/CSF.2011.12
URL : https://hal.archives-ouvertes.fr/inria-00636747

C. Trusted and . Group, TPM Specification version 1.2. Parts 1?3, revision 103, 2007.

D. Longley and S. Rigby, An automatic search for security flaws in key management schemes, Computers & Security, vol.11, issue.1, pp.75-89, 1992.
DOI : 10.1016/0167-4048(92)90222-D

M. Bond and R. Anderson, API-level attacks on embedded systems, Computer, vol.34, issue.10, pp.67-75, 2001.
DOI : 10.1109/2.955101

J. Herzog, Applying protocol analysis to security device interfaces, IEEE Security & Privacy Magazine, vol.4, issue.4, pp.84-87, 2006.
DOI : 10.1109/MSP.2006.85

B. Schmidt, S. Meier, C. Cremers, and D. Basin, Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties, 2012 IEEE 25th Computer Security Foundations Symposium, pp.78-94, 2012.
DOI : 10.1109/CSF.2012.25

S. Delaune, S. Kremer, and G. Steel, Formal security analysis of PKCS#11 and proprietary extensions, Journal of Computer Security, vol.18, issue.6, pp.1211-1245, 2010.
DOI : 10.3233/JCS-2009-0394

J. D. Guttman, State and Progress in Strand Spaces: Proving Fair Exchange, Journal of Automated Reasoning, vol.14, issue.5, pp.159-195, 2012.
DOI : 10.1007/s10817-010-9202-1

]. S. Bistarelli, I. Cervesato, G. Lenzini, and F. Martinelli, Relating multiset rewriting and process algebras for security protocol analysis, Journal of Computer Security, vol.13, issue.1, pp.3-47, 2005.
DOI : 10.3233/JCS-2005-13102

R. Künnemann and G. Steel, YubiSecure? Formal Security Analysis Results for the Yubikey and YubiHSM, Proc. 8th Workshop on Security and Trust Management (STM'12), ser. LNCS, pp.257-272, 2012.
DOI : 10.1007/978-3-642-38004-4_17

J. A. Garay, M. Jakobsson, and P. D. Mackenzie, Abusefree optimistic contract signing, Advances in Cryptology? Crypto'99, ser. LNCS, pp.449-466, 1999.

A. Yubico, 2013, accessed: Wed 1740:50 CEST. [Online] Available: https://www.yubico.com/about/reference-customers/ APPENDIX Definition 17 (Process annotation) Given a ground process P we define the annotated ground process P as follows, 201311-07.