Analyzing security protocols with secrecy types and logic programs, Journal of the ACM, vol.52, issue.1, pp.102-146, 2005. ,
DOI : 10.1145/1044731.1044735
A calculus for cryptographic protocols, Proceedings of the 4th ACM conference on Computer and communications security , CCS '97, pp.1-70, 1999. ,
DOI : 10.1145/266420.266432
DKM: Design and verification of a crypto-agile distributed key manager, 2011. ,
Extracting and verifying cryptographic models from C protocol code by symbolic execution, Proceedings of the 18th ACM conference on Computer and communications security, CCS '11, 2011. ,
DOI : 10.1145/2046707.2046745
Plaintext Recovery Attacks against SSH, 2009 30th IEEE Symposium on Security and Privacy, pp.16-26, 2009. ,
DOI : 10.1109/SP.2009.5
Computationally sound verification of source code, Proceedings of the 17th ACM conference on Computer and communications security, CCS '10, pp.387-398, 2010. ,
DOI : 10.1145/1866307.1866351
Union and Intersection Types for Secure Protocol Implementations, TOSCA, 2011. ,
DOI : 10.1007/978-3-642-27375-9_1
URL : https://hal.archives-ouvertes.fr/hal-01102192
Secure compilation of a multi-tier web language, Proceedings of the 4th international workshop on Types in language design and implementation, TLDI '09, pp.27-38, 2009. ,
DOI : 10.1145/1481861.1481866
Maintaining Database Integrity with Refinement Types, 2011. ,
DOI : 10.1017/S0956796806006216
Introduction to modern cryptography, UCSD CSE 207 Course Notes, 2005. ,
Keying Hash Functions for Message Authentication, LNCS, vol.1109, pp.1-15, 1996. ,
DOI : 10.1007/3-540-68697-5_1
Verified implementations of the information card federated identity-management protocol, Proceedings of the 2008 ACM symposium on Information, computer and communications security , ASIACCS '08, pp.123-135, 2008. ,
DOI : 10.1145/1368310.1368330
Verified interoperable implementations of security protocols, ACM Transactions on Programming Languages and Systems, vol.31, issue.1, pp.1-561, 2008. ,
DOI : 10.1145/1452044.1452049
Cryptographic Protocol Synthesis and Verification for Multiparty Sessions, 2009 22nd IEEE Computer Security Foundations Symposium, pp.124-140, 2009. ,
DOI : 10.1109/CSF.2009.26
Cryptographic Protocol Synthesis and Verification for Multiparty Sessions, 2009 22nd IEEE Computer Security Foundations Symposium, pp.124-140, 2009. ,
DOI : 10.1109/CSF.2009.26
Modular verification of security protocol code by typing, ACM Symposium on Principles of Programming Languages (POPL'10), pp.445-456, 2010. ,
Chosen ciphertext attacks against protocols based on the RSA encryption standard PKCS #1, Advances in Cryptology -CRYPTO '98, pp.1-12, 1998. ,
DOI : 10.1007/BFb0055716
Roles, stacks, histories: A triple for Hoare, Journal of Functional Programming, vol.29, issue.02, pp.159-207, 2011. ,
DOI : 10.1145/1057387.1057392
Breaking and fixing public-key Kerberos, Information and Computation, vol.206, pp.2-4402, 2008. ,
ASPIER: An Automated Framework for Verifying Security Protocol Implementations, 2009 22nd IEEE Computer Security Foundations Symposium, pp.172-185, 2009. ,
DOI : 10.1109/CSF.2009.20
VCC: A Practical System for Verifying Concurrent C, TPHOLs, pp.23-42, 2009. ,
DOI : 10.1007/978-3-540-74591-4_15
Efficient Symbolic Execution for Analysing Cryptographic Protocol Implementations, ESSoS, pp.58-72, 2011. ,
DOI : 10.1007/978-3-642-19125-1_5
On the security of public key protocols, IEEE Transactions on Information Theory, vol.29, issue.2, pp.198-208, 1983. ,
DOI : 10.1109/TIT.1983.1056650
Guiding a general-purpose C verifier to prove cryptographic protocols, 24th IEEE Computer Security Foundations Symposium, 2011. ,
Modular code-based cryptographic verification, Proceedings of the 18th ACM conference on Computer and communications security, CCS '11, p.7, 2011. ,
DOI : 10.1145/2046707.2046746
URL : https://hal.archives-ouvertes.fr/inria-00614372
A Digital Signature Scheme Secure Against Adaptive Chosen-Message Attacks, SIAM Journal on Computing, vol.17, issue.2, pp.281-308, 1988. ,
DOI : 10.1137/0217017
Principles and applications of refinement types Logics and Languages for Reliability and Security, 2010. ,
Cryptographic Protocol Analysis on Real C Code, VMCAI, pp.363-379, 2005. ,
DOI : 10.1007/978-3-540-30579-8_24
Reliable Evidence: Auditability by Typing, 14th European Symposium on Research in Computer Security (ESORICS'09), pp.168-183, 2009. ,
DOI : 10.1016/S0140-3664(02)00049-X
HMAC: Keyed-hashing for message authentication, 1997. ,
DOI : 10.17487/rfc2104
Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR, TACAS, volume 1055 of Lecture Notes in Computer Science, pp.147-166, 1996. ,
DOI : 10.1007/3-540-61042-1_43
Communicating and Mobile Systems: the ?-Calculus, 1999. ,
Using encryption for authentication in large networks of computers, Communications of the ACM, vol.21, issue.12, pp.993-999, 1978. ,
DOI : 10.1145/359657.359659
Formally-Based Black-Box Monitoring of Security Protocols, ESSoS, pp.79-95, 2010. ,
DOI : 10.1007/978-3-642-11747-3_7
Enforcing Stateful Authorization and Information Flow Policies in Fine, ESOP, pp.529-549, 2010. ,
DOI : 10.1007/978-3-642-11957-6_28
Secure distributed programming with value-dependent types, International Conference on Functional Programming, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00939188
Security Flaws Induced by CBC Padding ??? Applications to SSL, IPSEC, WTLS..., Advances in Cryptology -EUROCRYPT 2002, pp.534-545, 2002. ,
DOI : 10.1007/3-540-46035-7_35