Publications

2014
[122] Beagle as a HOL4 external ATP method (Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish), In PAAR-2014 - 4th Workshop on Practical Aspects of Automated Reasoning, 2014. (To appear) [bib]
[121] Gradual typing embedded securely in JavaScript (Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman), In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014. [bib]
[120] A Verified Information-Flow Architecture (Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach), In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014. [bib]
[119] Verification of cryptographic protocols with lists of unbounded length (Miriam Paiola), PhD thesis, Université Paris VII, 2014. [bib]
[118] Proving the TLS Handshake Secure (as it is) (Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin), In Proceedings of CRYPTO, 2014. (Long version at Cryptology ePrint Archive, Report 2014/182: https://eprint.iacr.org/2014/182) [bib]
[117] Web PKI: Closing the Gap between Guidelines and Practices (Antoine Delignat-Lavaud, Martin Abadí, Matthew Birrell, Ilya Mironov, Ted Wobber, Yinglian Xie), In Proceedings of the ISOC Network and Distributed System Security Symposium (NDSS '14), 2014. [bib]
[116] Automated analysis of security protocols with global state (Steve Kremer, Robert Künnemann), In IEEE Symposium on Security & Privacy (Oakland), 2014. [bib]
[115] A Formal Library for Elliptic Curves in the Coq Proof Assistant (Evmorfia-Iro Bartzia, Pierre-Yves Strub), In Interactive Theorem Proving (ITP), 2014. [bib]
[114] Automatic Verification of Security Protocols in the Symbolic Model: the Verifier ProVerif (Bruno Blanchet), Chapter in Foundations of Security Analysis and Design VII, FOSAD Tutorial Lectures (Alessandro Aldini, Javier Lopez, Fabio Martinelli, eds.), Springer Verlag, volume 8604, 2014. [bib]
[113] Defensive JavaScript - Building and Verifying Secure Web Components (Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis), Chapter in Foundations of Security Analysis and Design VII, FOSAD Tutorial Lectures (Alessandro Aldini, Javier Lopez, Fabio Martinelli, eds.), Springer Verlag, volume 8604, 2014. [bib]
[112] Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS (Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, and Alfredo Pironti, Pierre-Yves Strub), In IEEE Symposium on Security & Privacy (Oakland), 2014. [bib]
[111] Discovering concrete attacks on website authorization by formal analysis (Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis), In Journal of Computer Security, volume 22, 2014. [bib]
[110] Computationally Complete Symbolic Adversary and Key Exchange (in Japanese) (Gergei Bana, Koji Hasebe, Mitsuhiro Okada), 2014. [bib]
[109] A Computationally Complete Symbolic Attacker for Equivalence Properties (Gergei Bana, Hubert Comon-Lundh), In ACM Conference on Computer and Communications Security (CCS'14), ACM, 2014. [bib]
[108] Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations (Michael Backes, Catalin Hritcu, Matteo Maffei), In Journal of Computer Security (JCS); Special Issue on Foundational Aspects of Security, IOS Press, volume 22, 2014. [bib] [doi]
[107] Election Verifiability: Definitions and an Analysis of Helios and JCJ (Ben Smyth, Steven Frink, Michael R. Clarkson), 2014. [bib]
[106] Ballot secrecy with malicious bulletin boards (Ben Smyth), Technical report, Cryptology ePrint Archive, 2014. [bib]
[105] Ballot secrecy and ballot independence: definitions and relations (Ben Smyth, David Bernhard), Technical report, Cryptology ePrint Archive, 2014. [bib]
[104] Hawk and Aucitas: e-auction schemes from the Helios and Civitas e-voting schemes (Adam McCarthy, Ben Smyth, Elizabeth A. Quaglia), In FC'14: 18th International Conference on Financial Cryptography and Data Security, Springer Verlag, volume 8437, 2014. [bib]
2013
[103] Secure distributed programming with value-dependent types (Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang), In J. Funct. Program., volume 23, 2013. [bib]
[102] Verification of Security Protocols with Lists: from Length One to Unbounded Length (Miriam Paiola, Bruno Blanchet), In Journal of Computer Security, volume 21, 2013. (Special issue POST'12) [bib]
[101] Towards Unified Authorization for Android (Michael J. May, Karthikeyan Bhargavan), In 5th International Symposium on Engineering Secure Software and Systems (ESSoS 2013), Springer Verlag, volume 7781, 2013. [bib]
[100] Universally Composable Key-Management (Steve Kremer, Robert Künnemann, Graham Steel), In Proceedings of the 18th European Symposium on Research in Computer Security (ESORICS'13) (Jason Crampton, Sushil Jajodia, Keith Mayes, eds.), Springer, volume 8134, 2013. [bib] [doi]
[99] Language-Based Defenses Against Untrusted Browser Origins (Antoine Delignat-Lavaud, Karthikeyan Bhargavan, Sergio Maffeis), In Proceedings of the 22th USENIX Security Symposium, 2013. [bib]
[98] Proving More Observational Equivalences with ProVerif (Vincent Cheval, Bruno Blanchet), In 2nd Conference on Principles of Security and Trust (POST 2013) (David Basin, John Mitchell, eds.), Springer Verlag, volume 7796, 2013. [bib]
[97] From Computationally-Proved Protocol Specifications to Implementations and Application to SSH (David Cadé, Bruno Blanchet), In Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), Innovative Information Science & Technology Research Group (ISYOU), volume 4, 2013. (Special issue ARES'12) [bib]
[96] Proved Generation of Implementations from Computationally-Secure Protocol Specifications (David Cadé, Bruno Blanchet), In 2nd Conference on Principles of Security and Trust (POST 2013) (David Basin, John Mitchell, eds.), Springer Verlag, volume 7796, 2013. [bib]
[95] Proved Implementations of Cryptographic Protocols in the Computational Model (David Cadé), PhD thesis, Université Paris VII, 2013. [bib]
[94] Automatic Verification of Protocols with Lists of Unbounded Length (Bruno Blanchet, Miriam Paiola), In ACM Conference on Computer and Communications Security (CCS'13), ACM, 2013. [bib]
[93] Implementing TLS with Verified Cryptographic Security (Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub), In IEEE Symposium on Security & Privacy (Oakland), 2013. [bib]
[92] Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage (Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis), In 2nd Conference on Principles of Security and Trust (POST 2013) (David Basin, John Mitchell, eds.), Springer Verlag, volume 7796, 2013. [bib]
[91] Computationally Complete Symbolic Attacker and Key Exchange (Gergei Bana, Koji Hasebe, Mitsuhiro Okada), In ACM Conference on Computer and Communications Security (CCS'13), ACM, 2013. [bib]
[90] Computationally Complete Symbolic Adversary and Computationally Sound Veri?cation of Security Protocols (in Japanese) (Gergei Bana, Pedro Adaõ, Hideki Sakurada), 2013. [bib]
[89] Truncating TLS Connections to Violate Beliefs in Web Applications (Ben Smyth, Alfredo Pironti), In WOOT'13: 7th USENIX Workshop on Offensive Technologies, USENIX Association, 2013. (First appeared at Black Hat USA 2013.) [bib]
[88] Ballot secrecy and ballot independence coincide (Ben Smyth, David Bernhard), In ESORICS'13: 18th European Symposium on Research in Computer Security, Springer, volume 8134, 2013. [bib]
[87] Attacking and fixing Helios: An analysis of ballot secrecy (Véronique Cortier, Ben Smyth), In Journal of Computer Security, IOS Press, volume 21, 2013. [bib]
2012
[86] Formal verification of security protocol implementations: a survey (Matteo Avalle, Alfredo Pironti, Riccardo Sisto), In Formal Aspects of Computing, 2012. [bib]
[85] Identifying Website Users by TLS Traffic Analysis: New Attacks and Effective Countermeasures (Alfredo Pironti, Pierre-Yves Strub, Karthikeyan Bhargavan), 2012. (INRIA Technical Report RR-8067) [bib]
[84] Revoke and Let Live: A Secure Key Revocation API for Cryptographic Devices (Véronique Cortier, Graham Steel, Cyrille Wiedling), 2012. (INRIA Technical Report RR-7949) [bib]
[83] Efficient Padding Oracle Attacks on Cryptographic Hardware (Romain Bardou, Riccardo Focardi, Yusuke Kawamoto, Lorenzo Simionato, Graham Steel, Joe-Kai Tsay), 2012. (INRIA Technical Report RR-7944) [bib]
[82] Computationally Complete Symbolic Attacker in Action (Gergei Bana, Pedro Adão, Hideki Sakurada), In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012), 2012. [bib]
[81] Safe Abstractions of Data Encodings in Formal Security Protocol Models (Alfredo Pironti, Riccardo Sisto), In Formal Aspects of Computing, 2012. [bib]
[80] Formally-Based Semi-Automatic Implementation of an Open Security Protocol (Alfredo Pironti, Davide Pozza, Riccardo Sisto), In Journal of Systems and Software, Elsevier, volume 85, 2012. [bib]
[79] Verification of Security Protocols with Lists: from Length One to Unbounded Length (Miriam Paiola, Bruno Blanchet), In First Conference on Principles of Security and Trust (POST'12) (Pierpaolo Degano, Joshua Guttman, eds.), Springer Verlag, volume 7215, 2012. [bib]
[78] YubiSecure? Formal Security Analysis Results for the Yubikey and YubiHSM (Robert Künnemann, Graham Steel), In Revised Selected Papers of the 8th Workshop on Security and Trust Management (STM'12) (Audun Jøsang, Pierangela Samarati, Marinella Petrocchi, eds.), Springer, volume 7783, 2012. [bib] [doi]
[77] Towards Unconditional Soundness: Computationally Complete Symbolic Attacker (Gergei Bana, Hubert Comon-Lundh), In 2nd Conference on Principles of Security and Trust (POST 2012), Springer Verlag, volume 7215, 2012. [bib]
[76] From Computationally-proved Protocol Specifications to Implementations (David Cadé, Bruno Blanchet), In 7th International Conference on Availability, Reliability and Security (AReS 2012), IEEE, 2012. [bib]
[75] Mechanizing Game-Based Proofs of Security Protocols (Bruno Blanchet), Chapter in Software Safety and Security - Tools for Analysis and Verification (Tobias Nipkow, Olga Grumberg, Benedikt Hauptmann, eds.), IOS Press, volume 33, 2012. (Proceedings of the summer school MOD 2011) [bib]
[74] Security Protocol Verification: Symbolic and Computational Models (Bruno Blanchet), In First Conference on Principles of Security and Trust (POST'12) (Pierpaolo Degano, Joshua Guttman, eds.), Springer Verlag, volume 7215, 2012. [bib]
[73] Automatically Verified Mechanized Proof of One-Encryption Key Exchange (Bruno Blanchet), In 25th IEEE Computer Security Foundations Symposium (CSF'12), 2012. [bib]
[72] Towards the Automated Verification of Cryptographic Protocol Implementations (Karthikeyan Bhargavan), 2012. [bib]
[71] Verified Cryptographic Implementations for TLS (Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu), In ACM Transactions Inf. Syst. Secur., ACM, volume 15, 2012. [bib] [doi]
[70] Web-based Attacks on Host-Proof Encrypted Storage (Karthikeyan Bhargavan, Antoine Delignat-Lavaud), In 6th USENIX Workshop on Offensive Technologies (WOOT'12), 2012. [bib]
[69] Visual Model-Driven Design, Verification and Implementation of Security Protocols (Piergiuseppe Bettassa Copet, Alfredo Pironti, Davide Pozza, Riccardo Sisto, Pietro Vivoli), In IEEE International Symposium on High Assurance Systems Engineering (HASE 12), IEEE Computer Security, 2012. (Short paper) [bib]
[68] Efficient Padding Oracle Attacks on Cryptographic Hardware (Romain Bardou, Riccardo Focardi, Yusuke Kawamoto, Lorenzo Simionato, Graham Steel, Joe-Kai Tsay), In CRYPTO, 2012. [bib]
[67] Discovering Concrete Attacks on Website Authorization by Formal Analysis (Chetan Bansal, Karthikeyan Bhargavan, Sergio Maffeis), In 25th IEEE Computer Security Foundations Symposium (CSF'12), 2012. [bib]
2011
[66] Formal Analysis of Security APIs (Graham Steel), 2011. [bib]
[65] Secure distributed programming with value-dependent types (Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang), In 16th ACM SIGPLAN international conference on Functional Programming, 2011. [bib]
[64] Security for Key Management Interfaces (Steve Kremer, Graham Steel, Bogdan Warinschi), In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11), IEEE Computer Society Press, 2011. [bib]
[63] Cryptographic Verification by Typing for a Sample Protocol Implementation (Cédric Fournet, Karthikeyan Bhargavan, Andrew D. Gordon), In Foundations of Security Analysis and Design VI (FOSAD'10), 2011. [bib]
[62] Formal analysis of protocols based on TPM state registers (Stéphanie Delaune, Steve Kremer, Mark D. Ryan, Graham Steel), In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11), IEEE Computer Society Press, 2011. [bib]
[61] Formal Analysis of Privacy for Anonymous Location Based Services (Morten Dahl, Stéphanie Delaune, Graham Steel), In Proceedings of the Workshop on Theory of Security and Applications (TOSCA'11), 2011. (To appear) [bib]
[60] A second look at Shoup's lemma (Bruno Blanchet), In Workshop on Formal and Computational Cryptography (FCC 2011), 2011. [bib]
[59] Using Horn Clauses for Analyzing Security Protocols (Bruno Blanchet), Chapter in Formal Models and Techniques for Analyzing Security Protocols (Véronique Cortier, Steve Kremer, eds.), IOS Press, volume 5, 2011. [bib]
[58] Refinement types for secure implementations (Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis), In ACM Trans. Program. Lang. Syst., volume 33, 2011. [bib]
2010
[57] Formal Analysis of PKCS\11 and Proprietary Extensions (Stéphanie Delaune, Steve Kremer, Graham Steel), In Journal of Computer Security, IOS Press, volume 18, 2010. [bib] [doi]
[56] A Formal Analysis of Authentication in the TPM (Stéphanie Delaune, Steve Kremer, Mark D. Ryan, Graham Steel), In Revised Selected Papers of the 7th International Workshop on Formal Aspects in Security and Trust (FAST'10) (Pierpaolo Degano, Sandro Etalle, Joshua Guttman, eds.), Springer, volume 6561, 2010. [bib] [doi]
[55] Formal Analysis of Privacy for Vehicular Mix-Zones (Morten Dahl, Stéphanie Delaune, Graham Steel), In Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS'10) (Dimitris Gritzalis, Bart Preneel, eds.), Springer, volume 6345, 2010. [bib] [doi]
[54] The computational and decisional Diffie-Hellman assumptions in CryptoVerif (Bruno Blanchet, David Pointcheval), In Workshop on Formal and Computational Cryptography (FCC 2010), 2010. [bib]
[53] Typechecking Higher-Order Security Libraries (Karthikeyan Bhargavan, Cédric Fournet, Nataliya Guts), In 8th Asian Symposium on Programming Languages and Systems, 2010. [bib]
[52] Modular verification of security protocol code by typing (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon), In 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'10), 2010. [bib]
[51] Attacking and Fixing PKCS\11 Security Tokens (Matteo Bortolozzo, Matteo Centenaro, Riccardo Focardi, Graham Steel), In Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS'10), ACM Press, 2010. [bib] [doi]
2009
[50] Towards a Type System for Security APIs (Gavin Keighren, David Aspinall, Graham Steel), In Revised Selected Papers of the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS'09) (Pierpaolo Degano, Luca Viganò, eds.), Springer, volume 5511, 2009. [bib] [doi]
[49] Analysing PKCS\11 Key Management APIs with Unbounded Fresh Data (Sibylle Fröschle, Graham Steel), In Revised Selected Papers of the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS'09) (Pierpaolo Degano, Luca Viganò, eds.), Springer, volume 5511, 2009. [bib] [doi]
[48] Blunting Differential Attacks on PIN Processing APIs (Riccardo Focardi, Flaminia L. Luccio, Graham Steel), In Proceedings of the 14th Nordic Workshop on Secure IT Systems (NordSec'09) (Audun Jøsang, Torleiv Maseng, Svein Johan Knapskog, eds.), Springer, volume 5838, 2009. [bib] [doi]
[47] A generic security API for symmetric key management on cryptographic devices (Véronique Cortier, Graham Steel), In Proceedings of the 14th European Symposium on Research in Computer Security (ESORICS'09) (Michael Backes, Peng Ning, eds.), Springer, volume 5789, 2009. [bib] [doi]
[46] Type-based Analysis of PIN Processing APIs (Matteo Centenaro, Riccardo Focardi, Flaminia L. Luccio, Graham Steel), In Proceedings of the 14th European Symposium on Research in Computer Security (ESORICS'09) (Michael Backes, Peng Ning, eds.), Springer, volume 5789, 2009. [bib] [doi]
[45] A compositional theory for STM Haskell (Johannes Borgström, Karthikeyan Bhargavan, Andrew D. Gordon), In 2nd ACM SIGPLAN Symposium on Haskell, 2009. [bib]
[44] Refining Computationally Sound Mechanized Proofs for Kerberos (Bruno Blanchet, Aaron D. Jaggard, Jesse Rao, Andre Scedrov, Joe-Kai Tsay), In Workshop on Formal and Computational Cryptography (FCC 2009), 2009. [bib]
[43] Automatic Verification of Correspondences for Security Protocols (Bruno Blanchet), In Journal of Computer Security, volume 17, 2009. [bib]
[42] Cryptographic Protocol Synthesis and Verification for Multiparty Sessions (Karthikeyan Bhargavan, Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, James J. Leifer), In 22nd IEEE Computer Security Foundations Symposium (CSF-22), 2009. [bib]
[41] Models and Proofs of Protocol Security: A Progress Report (Martín Abadi, Bruno Blanchet, Hubert Comon-Lundh), In 21st International Conference on Computer Aided Verification (CAV'09) (Ahmed Bouajjani, Oded Maler, eds.), Springer Verlag, volume 5643, 2009. [bib]
2008
[40] The Importance of Non-theorems and Counterexamples in Program Verification (Graham Steel), In Revised Selected Papers and Discussions of the 1st IFIP TC2\slashWG2.3 Conference Verified Software---Theories, Tools, and Experiments (VSTTE'05) (Bertrand Meyer, Jim Woodcock, eds.), Springer, volume 4171, 2008. [bib] [doi]
[39] Formal Analysis of PKCS\11 (Stéphanie Delaune, Steve Kremer, Graham Steel), In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF'08), IEEE Computer Society Press, 2008. [bib] [doi]
[38] A secure compiler for session abstractions (Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, Karthikeyan Bhargavan, James J. Leifer), In Journal of Computer Security, volume 16, 2008. [bib]
[37] A Computationally Sound Mechanized Prover for Security Protocols (Bruno Blanchet), In IEEE Transactions on Dependable and Secure Computing, volume 5, 2008. [bib]
[36] Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos (Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, Joe-Kai Tsay), In ACM Symposium on Information, Computer and Communications Security (ASIACCS'08), ACM, 2008. [bib]
[35] Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire. Automatic verification of security protocols: formal model and computational model (Bruno Blanchet), 2008. [bib]
[34] Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage (Bruno Blanchet, Avik Chaudhuri), In IEEE Symposium on Security and Privacy, IEEE, 2008. [bib]
[33] Automated Verification of Selected Equivalences for Security Protocols (Bruno Blanchet, Martín Abadi, Cédric Fournet), In Journal of Logic and Algebraic Programming, volume 75, 2008. [bib]
[32] Service Combinators for Farming Virtual Machines (Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya), In 10th International Conference on Coordination Models and Languages, 2008. [bib]
[31] Verified interoperable implementations of security protocols (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse), In ACM Transactions on Programming Languages and Systems, volume 31, 2008. [bib]
[30] Verified implementations of the information card federated identity-management protocol (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Nikhil Swamy), In ACM Symposium on Information, Computer and Communications Security (ASIACCS), 2008. [bib]
[29] Verifying policy-based web services security (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon), In ACM Transactions on Programming Languages and Systems, volume 30, 2008. [bib]
[28] Cryptographically verified implementations for TLS (Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu), In ACM Conference on Computer and Communications Security, 2008. [bib]
[27] Refinement Types for Secure Implementations (Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis), In 21st IEEE Computer Security Foundations Symposium (CSF-21), 2008. [bib]
2007
[26] Automatic Analysis of the Security of XOR-Based Key Management Schemes (Véronique Cortier, Gavin Keighren, Graham Steel), In Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'07) (Orna Grumberg, Michael Huth, eds.), Springer, volume 4424, 2007. [bib] [doi]
[25] A Formal Theory of Key Conjuring (Véronique Cortier, Stéphanie Delaune, Graham Steel), In Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF'07), IEEE Computer Society Press, 2007. [bib] [doi]
[24] Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos (Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, Joe-Kai Tsay), In Dagstuhl seminar "Formal Protocol Verification Applied", 2007. [bib]
[23] CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols (Bruno Blanchet), In Dagstuhl seminar "Formal Protocol Verification Applied", 2007. [bib]
[22] Computationally Sound Mechanized Proofs of Correspondence Assertions (Bruno Blanchet), In 20th IEEE Computer Security Foundations Symposium (CSF'07), 2007. [bib]
[21] Service Combinators for Farming Virtual Machines (Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya), In Third Symposium on Trustworthy Global Computing (TGC), 2007. [bib]
[20] Secure sessions for Web services (Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Andrew D. Gordon), In ACM Transactions on Information and System Security, volume 10, 2007. [bib]
[19] Just Fast Keying in the Pi Calculus (Martín Abadi, Bruno Blanchet, Cédric Fournet), In ACM Transactions on Information and System Security (TISSEC), volume 10, 2007. [bib]
2006
[18] Formal analysis of PIN block attacks (Graham Steel), In Theoretical Computer Science, Elsevier Science Publishers, volume 367, 2006. [bib] [doi]
[17] Attacking Group Protocols by Refuting Incorrect Inductive Conjectures (Graham Steel, Alan Bundy), In Journal of Automated Reasoning, Springer, volume 36, 2006. [bib] [doi]
[16] Automated Security Proofs with Sequences of Games (Bruno Blanchet, David Pointcheval), In CRYPTO'06 (Cynthia Dwork, ed.), Springer Verlag, volume 4117, 2006. [bib]
[15] A Computationally Sound Mechanized Prover for Security Protocols (Bruno Blanchet), In IEEE Symposium on Security and Privacy, 2006. [bib]
[14] Verified Reference Implementations of WS-Security Protocols (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon), In Third International Workshop on Web Services and Formal Methods, 2006. [bib]
[13] Verified Interoperable Implementations of Security Protocols (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse), In 19th IEEE Computer Security Foundations Workshop (CSFW'06), 2006. [bib]
2005
[12] Deduction with XOR Constraints in Security API Modelling (Graham Steel), In Proceedings of the 20th International Conference on Automated Deduction (CADE'05) (Robert Nieuwenhuis, ed.), Springer, volume 3632, 2005. [bib] [doi]
[11] Verification of Cryptographic Protocols: Tagging Enforces Termination (Bruno Blanchet, Andreas Podelski), In Theoretical Computer Science, volume 333, 2005. (Special issue FoSSaCS'03.) [bib]
[10] Security Protocols: From Linear to Classical Logic by Abstract Interpretation (Bruno Blanchet), In Information Processing Letters, volume 95, 2005. [bib]
[9] An Automatic Security Protocol Verifier based on Resolution Theorem Proving (invited tutorial) (Bruno Blanchet), In 20th International Conference on Automated Deduction (CADE-20), 2005. [bib]
[8] Automated Verification of Selected Equivalences for Security Protocols (Bruno Blanchet, Martín Abadi, Cédric Fournet), In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), IEEE Computer Society, 2005. [bib]
[7] Reconstruction of Attacks against Cryptographic Protocols (Xavier Allamigeon, Bruno Blanchet), In 18th IEEE Computer Security Foundations Workshop (CSFW-18), IEEE Computer Society, 2005. [bib]
[6] Computer-Assisted Verification of a Protocol for Certified Email (Martín Abadi, Bruno Blanchet), In Science of Computer Programming, volume 58, 2005. (Special issue SAS'03.) [bib]
[5] Analyzing Security Protocols with Secrecy Types and Logic Programs (Martín Abadi, Bruno Blanchet), In Journal of the ACM, volume 52, 2005. [bib]
2004
[4] Discovering Attacks on Security Protocols by Refuting Incorrect Inductive Conjectures (Graham Steel), 2004. [bib]
[3] Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures (Graham Steel, Alan Bundy, Monika Maidl), In Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR'04) (David A. Basin, Michaël Rusinowitch, eds.), Springer-Verlag, volume 3097, 2004. [bib] [doi]
[2] Automatic Proof of Strong Secrecy for Security Protocols (Bruno Blanchet), In IEEE Symposium on Security and Privacy, 2004. [bib]
[1] Just Fast Keying in the Pi Calculus (Martín Abadi, Bruno Blanchet, Cédric Fournet), In Programming Languages and Systems: Proceedings of the 13th European Symposium on Programming (ESOP'04) (David Schmidt, ed.), Springer Verlag, volume 2986, 2004. [bib]
Powered by bibtexbrowser