Publications
| 2013 | |
| [93] | Towards Unified Authorization for Android , In 5th International Symposium on Engineering Secure Software and Systems (ESSoS 2013), 2013. (To appear) [bib] |
| [92] | Proving More Observational Equivalences with ProVerif , In 2nd Conference on Principles of Security and Trust (POST 2013) (David Basin, John Mitchell, eds.), Springer Verlag, volume 7796, 2013. [bib] |
| [91] | From Computationally-Proved Protocol Specifications to Implementations and Application to SSH , 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] |
| [90] | Proved Generation of Implementations from Computationally-Secure Protocol Specifications , In 2nd Conference on Principles of Security and Trust (POST 2013) (David Basin, John Mitchell, eds.), Springer Verlag, volume 7796, 2013. [bib] |
| [89] | Implementing TLS with Verified Cryptographic Security , In IEEE Symposium on Security & Privacy (Oakland), 2013. (To appear) [bib] |
| [88] | Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage , In 2nd Conference on Principles of Security and Trust (POST 2013) (David Basin, John Mitchell, eds.), Springer Verlag, volume 7796, 2013. [bib] |
| [87] | Attacking and fixing Helios: An analysis of ballot secrecy , In Journal of Computer Security, volume 21, 2013. [bib] |
| 2012 | |
| [86] | Formal verification of security protocol implementations: a survey , In Formal Aspects of Computing, 2012. [bib] |
| [85] | Identifying Website Users by TLS Traffic Analysis: New Attacks and Effective Countermeasures , 2012. (INRIA Technical Report RR-8067) [bib] |
| [84] | Revoke and Let Live: A Secure Key Revocation API for Cryptographic Devices , 2012. (INRIA Technical Report RR-7949) [bib] |
| [83] | Efficient Padding Oracle Attacks on Cryptographic Hardware , 2012. (INRIA Technical Report RR-7944) [bib] |
| [82] | Computationally Complete Symbolic Attacker in Action , 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 , In Formal Aspects of Computing, 2012. [bib] |
| [80] | Formally-Based Semi-Automatic Implementation of an Open Security Protocol , In Journal of Systems and Software, Elsevier, volume 85, 2012. [bib] |
| [79] | Verification of Security Protocols with Lists: from Length One to Unbounded Length , 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 , In Preliminary Proceedings of the 8th Workshop on Security and Trust Management (STM'12) (Audun Jøsang, Pierangela Samarati, eds.), 2012. [bib] |
| [77] | Towards Unconditional Soundness: Computationally Complete Symbolic Attacker , In 2nd Conference on Principles of Security and Trust (POST 2013), 2012. [bib] |
| [76] | From Computationally-proved Protocol Specifications to Implementations , In 7th International Conference on Availability, Reliability and Security (AReS 2012), IEEE, 2012. [bib] |
| [75] | Mechanizing Game-Based Proofs of Security Protocols , 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 , 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 , In 25th IEEE Computer Security Foundations Symposium (CSF'12), 2012. [bib] |
| [72] | Towards the Automated Verification of Cryptographic Protocol Implementations , 2012. [bib] |
| [71] | Verified Cryptographic Implementations for TLS , In ACM Transactions Inf. Syst. Secur., ACM, volume 15, 2012. [bib] [doi] |
| [70] | Web-based Attacks on Host-Proof Encrypted Storage , In 6th USENIX Workshop on Offensive Technologies (WOOT'12), 2012. [bib] |
| [69] | Efficient Padding Oracle Attacks on Cryptographic Hardware , In CRYPTO, 2012. [bib] |
| [68] | Discovering Concrete Attacks on Website Authorization by Formal Analysis , In 25th IEEE Computer Security Foundations Symposium (CSF'12), 2012. [bib] |
| 2011 | |
| [67] | Formal Analysis of Security APIs , 2011. [bib] |
| [66] | Secure distributed programming with value-dependent types , In 16th ACM SIGPLAN international conference on Functional Programming, 2011. [bib] |
| [65] | Security for Key Management Interfaces , In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11), IEEE Computer Society Press, 2011. [bib] |
| [64] | Cryptographic Verification by Typing for a Sample Protocol Implementation , In Foundations of Security Analysis and Design VI (FOSAD'10), 2011. [bib] |
| [63] | Formal analysis of protocols based on TPM state registers , In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11), IEEE Computer Society Press, 2011. [bib] |
| [62] | Formal Analysis of Privacy for Anonymous Location Based Services , In Proceedings of the Workshop on Theory of Security and Applications (TOSCA'11), 2011. (To appear) [bib] |
| [61] | A second look at Shoup's lemma , In Workshop on Formal and Computational Cryptography (FCC 2011), 2011. [bib] |
| [60] | Using Horn Clauses for Analyzing Security Protocols , Chapter in Formal Models and Techniques for Analyzing Security Protocols (Véronique Cortier, Steve Kremer, eds.), IOS Press, volume 5, 2011. [bib] |
| [59] | Refinement types for secure implementations , In ACM Trans. Program. Lang. Syst., volume 33, 2011. [bib] |
| 2010 | |
| [58] | Formal Analysis of PKCS\11 and Proprietary Extensions , In Journal of Computer Security, IOS Press, volume 18, 2010. [bib] [doi] |
| [57] | A Formal Analysis of Authentication in the TPM , 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] |
| [56] | Formal Analysis of Privacy for Vehicular Mix-Zones , 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] |
| [55] | The computational and decisional Diffie-Hellman assumptions in CryptoVerif , In Workshop on Formal and Computational Cryptography (FCC 2010), 2010. [bib] |
| [54] | Typechecking Higher-Order Security Libraries , In 8th Asian Symposium on Programming Languages and Systems, 2010. [bib] |
| [53] | Modular verification of security protocol code by typing , In 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'10), 2010. [bib] |
| [52] | Attacking and Fixing PKCS\11 Security Tokens , In Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS'10), ACM Press, 2010. [bib] [doi] |
| 2009 | |
| [51] | Towards a Type System for Security APIs , 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] |
| [50] | Analysing PKCS\11 Key Management APIs with Unbounded Fresh Data , 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] | Blunting Differential Attacks on PIN Processing APIs , 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] |
| [48] | A generic security API for symmetric key management on cryptographic devices , 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] |
| [47] | Type-based Analysis of PIN Processing APIs , 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] | A compositional theory for STM Haskell , In 2nd ACM SIGPLAN Symposium on Haskell, 2009. [bib] |
| [45] | Refining Computationally Sound Mechanized Proofs for Kerberos , In Workshop on Formal and Computational Cryptography (FCC 2009), 2009. [bib] |
| [44] | Automatic Verification of Correspondences for Security Protocols , In Journal of Computer Security, volume 17, 2009. [bib] |
| [43] | Cryptographic Protocol Synthesis and Verification for Multiparty Sessions , In 22nd IEEE Computer Security Foundations Symposium (CSF-22), 2009. [bib] |
| [42] | Models and Proofs of Protocol Security: A Progress Report , In 21st International Conference on Computer Aided Verification (CAV'09) (Ahmed Bouajjani, Oded Maler, eds.), Springer Verlag, volume 5643, 2009. [bib] |
| 2008 | |
| [41] | The Importance of Non-theorems and Counterexamples in Program Verification , 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] |
| [40] | Formal Analysis of PKCS\11 , In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF'08), IEEE Computer Society Press, 2008. [bib] [doi] |
| [39] | A secure compiler for session abstractions , In Journal of Computer Security, volume 16, 2008. [bib] |
| [38] | A Computationally Sound Mechanized Prover for Security Protocols , In IEEE Transactions on Dependable and Secure Computing, volume 5, 2008. [bib] |
| [37] | Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos , In ACM Symposium on Information, Computer and Communications Security (ASIACCS'08), ACM, 2008. [bib] |
| [36] | Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire. Automatic verification of security protocols: formal model and computational model , 2008. [bib] |
| [35] | Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage , In IEEE Symposium on Security and Privacy, IEEE, 2008. [bib] |
| [34] | Automated Verification of Selected Equivalences for Security Protocols , In Journal of Logic and Algebraic Programming, volume 75, 2008. [bib] |
| [33] | Service Combinators for Farming Virtual Machines , In 10th International Conference on Coordination Models and Languages, 2008. [bib] |
| [32] | Verified interoperable implementations of security protocols , In ACM Transactions on Programming Languages and Systems, volume 31, 2008. [bib] |
| [31] | Verified implementations of the information card federated identity-management protocol , In ACM Symposium on Information, Computer and Communications Security (ASIACCS), 2008. [bib] |
| [30] | Verifying policy-based web services security , In ACM Transactions on Programming Languages and Systems, volume 30, 2008. [bib] |
| [29] | Cryptographically verified implementations for TLS , In ACM Conference on Computer and Communications Security, 2008. [bib] |
| [28] | Refinement Types for Secure Implementations , In 21st IEEE Computer Security Foundations Symposium (CSF-21), 2008. [bib] |
| 2007 | |
| [27] | Automatic Analysis of the Security of XOR-Based Key Management Schemes , 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] |
| [26] | A Formal Theory of Key Conjuring , In Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF'07), IEEE Computer Society Press, 2007. [bib] [doi] |
| [25] | Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos , In Dagstuhl seminar "Formal Protocol Verification Applied", 2007. [bib] |
| [24] | CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols , In Dagstuhl seminar "Formal Protocol Verification Applied", 2007. [bib] |
| [23] | Computationally Sound Mechanized Proofs of Correspondence Assertions , In 20th IEEE Computer Security Foundations Symposium (CSF'07), 2007. [bib] |
| [22] | Service Combinators for Farming Virtual Machines , In Third Symposium on Trustworthy Global Computing (TGC), 2007. [bib] |
| [21] | Secure sessions for Web services , In ACM Transactions on Information and System Security, volume 10, 2007. [bib] |
| [20] | Just Fast Keying in the Pi Calculus , In ACM Transactions on Information and System Security (TISSEC), volume 10, 2007. [bib] |
| 2006 | |
| [19] | Formal analysis of PIN block attacks , In Theoretical Computer Science, Elsevier Science Publishers, volume 367, 2006. [bib] [doi] |
| [18] | Attacking Group Protocols by Refuting Incorrect Inductive Conjectures , In Journal of Automated Reasoning, Springer, volume 36, 2006. [bib] [doi] |
| [17] | Automated Security Proofs with Sequences of Games , In CRYPTO'06 (Cynthia Dwork, ed.), Springer Verlag, volume 4117, 2006. [bib] |
| [16] | A Computationally Sound Mechanized Prover for Security Protocols , In IEEE Symposium on Security and Privacy, 2006. [bib] |
| [15] | Verified Reference Implementations of WS-Security Protocols , In Third International Workshop on Web Services and Formal Methods, 2006. [bib] |
| [14] | Verified Interoperable Implementations of Security Protocols , In 19th IEEE Computer Security Foundations Workshop (CSFW'06), 2006. [bib] |
| 2005 | |
| [13] | Deduction with XOR Constraints in Security API Modelling , In Proceedings of the 20th International Conference on Automated Deduction (CADE'05) (Robert Nieuwenhuis, ed.), Springer, volume 3632, 2005. [bib] [doi] |
| [12] | Verification of Cryptographic Protocols: Tagging Enforces Termination , In Theoretical Computer Science, volume 333, 2005. (Special issue FoSSaCS'03.) [bib] |
| [11] | Security Protocols: From Linear to Classical Logic by Abstract Interpretation , In Information Processing Letters, volume 95, 2005. [bib] |
| [10] | An Automatic Security Protocol Verifier based on Resolution Theorem Proving (invited tutorial) , In 20th International Conference on Automated Deduction (CADE-20), 2005. [bib] |
| [9] | Automated Verification of Selected Equivalences for Security Protocols , In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), IEEE Computer Society, 2005. [bib] |
| [8] | Reconstruction of Attacks against Cryptographic Protocols , In 18th IEEE Computer Security Foundations Workshop (CSFW-18), IEEE Computer Society, 2005. [bib] |
| [7] | Computer-Assisted Verification of a Protocol for Certified Email , In Science of Computer Programming, volume 58, 2005. (Special issue SAS'03.) [bib] |
| [6] | Analyzing Security Protocols with Secrecy Types and Logic Programs , In Journal of the ACM, volume 52, 2005. [bib] |
| 2004 | |
| [5] | Discovering Attacks on Security Protocols by Refuting Incorrect Inductive Conjectures , 2004. [bib] |
| [4] | Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures , 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] |
| [3] | Automatic Proof of Strong Secrecy for Security Protocols , In IEEE Symposium on Security and Privacy, 2004. [bib] |
| [2] | Just Fast Keying in the Pi Calculus , In Programming Languages and Systems: Proceedings of the 13th European Symposium on Programming (ESOP'04) (David Schmidt, ed.), Springer Verlag, volume 2986, 2004. [bib] |
| In Press | |
| [1] | Visual Model-Driven Design, Verification and Implementation of Security Protocols , In IEEE International Symposium on High Assurance Systems Engineering (HASE 12), IEEE Computer Security, In Press. (Short paper) [bib] |
Powered by bibtexbrowser