ProVerif users

Research papers

2003
  1. Karthikeyan Bhargavan, Cédric Fournet, Andrew Gordon, and Riccardo Pucella. TulaFale: A Security Tool for Web Services. In Formal Methods for Components and Objects (FMCO 2003), Springer LNCS, Revised Lecture Series, volume 3188, pages 197-222, 2004. Available at http://moscova.inria.fr/~karthik/pubs/tulafale-a-security-tool-for-web-services.pdf.
2004
  1. Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, and Andrew Gordon. Secure Sessions for Web Services. In 2004 ACM Workshop on Secure Web Services (SWS), Washington DC, October 29, 2004. Available at http://moscova.inria.fr/~karthik/pubs/secure-sessions-sws04.pdf.
  2. Karthikeyan Bhargavan, Cédric Fournet, and Andrew Gordon. Verifying Policy-Based Security for Web Services. In 2004 ACM Conference on Computer and Communications Security (CCS 2004), pp 268-277, Washington DC, October 25-29, 2004. Available at http://moscova.inria.fr/~karthik/pubs/verifying-policy-based-security-ccs04.pdf.
  3. Ran Canetti and Jonathan Herzog. Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). Cryptology ePrint Archive, Report 2004/334, 2004. Available at http://eprint.iacr.org/2004/334
  4. Steve Kremer and Mark D. Ryan. Analysing the vulnerability of protocols to produce known-pair and chosen-text attacks. Electronic Notes in Theoretical Computer Science -- Special Issue for CONCUR'04 Workshop on Security Issues in Coordination Models, Languages and Systems (SecCo'04), 2004. 18 pages. Available at http://www.cs.bham.ac.uk/~mdr/research/papers/index.html
2005
  1. Alexey Gotsman, Fabio Massacci, Marco Pistore. Towards an Independent Semantics and Verification Technology for the HLPSL Specification Language. In Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA-2005), Electronic Notes in Theoretical Computer Science, volume 135, issue 1, pages 59-77, 2005. doi:10.1016/j.entcs.2005.06.004.
  2. Steve Kremer and Mark D. Ryan. Analysis of an Electronic Voting Protocol in the Applied Pi Calculus. In Proceedings of the European Symposium on Programming (ESOP'05), Lecture Notes in Computer Science series, volume 3444, pages 186-200, Springer Verlag, 2005. Available at http://www.cs.bham.ac.uk/~mdr/research/papers/index.html
  3. Kevin D. Lux, Michael J. May, Nayan L. Bhattad, and Carl A. Gunter. WSEmail: Secure Internet Messaging Based on Web Services. In International Conference on Web Services (ICWS'05). Available at http://seclab.web.cs.illinois.edu/wp-content/uploads/2011/03/LuxMBG05.pdf.
2006
  1. Karthikeyan Bhargavan, Cédric Fournet, and Andrew Gordon. Verified reference implementations of WS-Security protocols. In 3rd International Workshop on Web Services and Formal Methods (WS-FM 2006), Vienna, September 8-9, 2006. Springer LNCS 4184:88-106. Available at http://moscova.inria.fr/~karthik/pubs/verified-implementations-of-ws-star-wsfm06.pdf.
  2. Karthikeyan Bhargavan, Cédric Fournet, Andrew Gordon, and Stephen Tse. Verified interoperable implementations of security protocols. In 19th IEEE Computer Security Foundations Workshop (CSFW 2006), pages 139-152, Venice, Italy, July 2006. IEEE Computer Society. Available at http://moscova.inria.fr/~karthik/pubs/verified-interoperable-implementations-csfw06.pdf.
  3. Himanshu Khurana and Hyung-Seok Hahm. Certified Mailing Lists. In Proceedings of the ACM Symposium on Communication, Information, Computer and Communication Security (ASIACCS'06), Taipei, Taiwan, March 2006. Available at http://www.ncsa.uiuc.edu/People/hkhurana/AsiaCCS06.pdf.
  4. Jens Chr. Godskesen. Formal Verification of the ARAN Protocol Using the Applied Pi Calculus. In Sixth International IFIP WG 1.7 Workshop on Issues in the Theory of Security (WITS'06), 2006. Available here.
2007
  1. Richard Chang and Vitaly Shmatikov. Formal Analysis of Authentication in Bluetooth Device Pairing. In Proc. of LICS/ICALP Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA), Wroclaw, Poland, July 2007. Available at http://www.cs.utexas.edu/~shmat/abstracts.html#blue
  2. Zhengqin Luo, Xiaojuan Cai, Jun Pang, and Yuxin Deng. Analyzing an Electronic Cash Protocol Using Applied Pi Calculus. In Applied Cryptography and Network Security, 5th International Conference, ACNS 2007, Zhuhai, China. Lecture Notes in Computer Science, volume 4521, pages 87-103. Springer. Available at http://basics.sjtu.edu.cn/~yuxin/publications/ecash.ps.
2008
  1. Michael Backes, Catalin Hritcu, and Matteo Maffei. Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-calculus. In Proceedings of 21st IEEE Computer Security Foundations Symposium (CSF), June 2008. Available at http://www.infsec.cs.uni-sb.de/~backes/papers/index.html
  2. Michael Backes, Matteo Maffei, and Dominique Unruh. Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol. In Proceedings of 29th IEEE Symposium on Security and Privacy, May 2008. Technical report available at http://eprint.iacr.org/2007/289.
  3. Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, and Eugen Zalinescu. Cryptographically Verified Implementations for TLS. In Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS'08), pages 459-468, October 2008. Available at http://prosecco.inria.fr/personal/karthik/pubs/cryptographically-verified-implementations-for-tls-ccs08.pdf.
  4. Karthikeyan Bhargavan, Cédric Fournet, Andrew Gordon, and Nikhil Swamy. Verified implementations of the Information Card Federated Identity-Management Protocol. In ACM Symposium on Information, Computer and Communications Security (ASIACCS'08), pages 123-135, Tokyo, Japan, March 2008. Available at http://moscova.inria.fr/~karthik/pubs/verified-implementations-of-cardspace-asiaccs08.pdf.
  5. Karthikeyan Bhargavan, Cédric Fournet, Andrew Gordon, and Stephen Tse. Verified interoperable implementations of security protocols. ACM Transactions on Programming Languages and Systems, 31(1):5, 2008. Available at http://moscova.inria.fr/~karthik/pubs/verified-interoperable-implementations-toplas08.pdf.
  6. Ralf Küsters and Tomasz Truderung. Reducing Protocol Analysis with XOR to the XOR-free case in the Horn Theory Based Approach. In Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS'08), pages 129-138, October 2008. Available at http://www.infsec.uni-trier.de/publications/paper/KuestersTruderung-CCS-2008.pdf.
2009
  1. Liqun Chen and Mark D. Ryan. Attack, solution and verification for shared authorisation data in TCG TPM. In Proceedings of Sixth International Workshop on Formal Aspects in Security and Trust (FAST'09). LNCS, Springer, 2010. Available at http://www.cs.bham.ac.uk/~mdr/research/papers/pdf/09-FAST.pdf.
  2. Stéphanie Delaune, Steve Kremer, and Mark Ryan. Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security 17(4), pages 435-487, 2009. Available at http://www.lsv.ens-cachan.fr/~delaune/mes-publis.php?onlykey=DKR-jcs08.
  3. Gilberto Filé and Roberto Vigo. Expressive power of definite clauses for verifying authenticity. In 22nd IEEE Computer Security Foundations Symposium (CSF'09), pages 251-265, Port Jefferson, New-York, USA, July 2009. IEEE Computer Society. Available at http://doi.ieeecomputersociety.org/10.1109/CSF.2009.12.
  4. Ralf Küsters and Tomasz Truderung. Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation. In 22nd IEEE Computer Security Foundations Symposium (CSF'09), pages 157-171, Port Jefferson, New-York, USA, July 2009. IEEE Computer Society. Available at http://www.infsec.uni-trier.de/publications/paper/KuestersTruderung-CSF-2009.pdf.
  5. Gyesik Lee, Hisashi Oguma, Akira Yoshioka, Rie Shigetomi, Akira Otsuka and Hideki Imai. Formally Verifiable Features in Embedded Vehicular Security Systems. In First IEEE Vehicular Networking Conference, VNC 2009, Tokyo. Available at http://ropas.snu.ac.kr/~gslee/Publi/vnc2009.pdf.
  6. Frank S. Park, Chinmay Gangakhedkar, and Patrick Traynor. Leveraging Cellular Infrastructure to Improve Fraud Prevention. In 2009 Annual Computer Security Applications Conference (ACSAC-25). Available at http://www.acsac.org/2009/openconf/modules/request.php?module=oc_program&action=summary.php&id=220
2010
  1. Mayla Brusó, Konstantinos Chatzikokolakis and Jerry den Hartog. Formal verification of privacy for RFID systems. 23rd IEEE Computer Security Foundations Symposium, 2010. Available at http://www.win.tue.nl/~kostas/papers/rfid_privacy.pdf.
  2. Riccardo Bresciani and Andrew Butterfield. ProVerif Analysis of the ZRTP Protocol. International Journal for Infonomics (IJI), Volume 3, Issue 3, September 2010. Available at http://infonomics-society.org/IJI/ProVerif%20Analysis%20of%20the%20ZRTP%20Protocol.pdf.
  3. Stéphanie Delaune, Steve Kremer, Mark Ryan, and Graham Steel. 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), Pisa, Italy, September 2010, LNCS 6561, pages 111-125. Springer. Available at http://www.lsv.ens-cachan.fr/~delaune/mes-publis.php?onlykey=DKRS-fast10.
  4. Naipeng Dong, Hugo Jonker, and Jun Pang. Analysis of a receipt-free auction protocol in the applied pi calculus. In Proc. 7th Workshop on Formal Aspects in Security and Trust - FAST'10, Lecture Notes in Computer Science 6561, pp. 223-238. Springer-Verlag, 2011. Available at http://satoss.uni.lu/members/jun/papers/FAST10.pdf.
  5. Bo Meng. Automatic Verification of Security Properties of Remote Internet Voting Protocol in Symbolic Model. In Information Technology Journal 9(8):1521-1556, 2010. Available at http://docsdrive.com/pdfs/ansinet/itj/2010/1521-1556.pdf.
  6. Sebastian Mödersheim. Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases, CCS 2010. Available at http://www2.imm.dtu.dk/~samo/setabstraction.pdf.
  7. Ben Smyth, Mark D. Ryan, Steve Kremer, and Mounira Kourjieh. Towards automatic analysis of election verifiability properties. In Proceedings of the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS'10), pp. 146-163, Lecture Notes in Computer Science 6186, Springer, Paphos, Cyprus, October 2010. Available at http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SRKK-arspawits10.pdf.
2011
  1. Myrto Arapinis, Eike Ritter, and Mark D. Ryan. StatVerif: Verification of stateful processes. In 24th Computer Security Foundations Symposium (CSF'11), Cernay-la-Ville, France, June 2011. Available at http://www.cs.bham.ac.uk/~arapinmd/pdf/ARR11.pdf.
  2. Stéphanie Delaune, Steve Kremer, Mark Ryan, and Graham Steel. Formal analysis of protocols based on TPM state registers. In 24th Computer Security Foundations Symposium (CSF'11), Cernay-la-Ville, France, June 2011. Available at http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKRS-csf11.pdf.
  3. Wei Huang and Bo Meng. Automated Proof of Resistance of Denial of Service Attacks in Remote Internet Voting Protocol with Extended Applied Pi Calculus. In Information Technology Journal, 10(8):1468-1483, 2011. Available at http://www.scialert.net/abstract/index.php?doi=itj.2011.1468.1483.
  4. Bo Meng. Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied Pi Calculus with Proverif. In Information Technology Journal 10(2):293-334, 2011. Available at http://docsdrive.com/pdfs/ansinet/itj/2011/293-334.pdf.
  5. Gabriel Pedroza, Ludovic Apvrille, and Daniel Knorreck. AVATAR: A SysML Environment for the Formal Verification of Safety and Security Properties, In 11th IEEE Conference on Distributed Systems and New Technologies (NOTERE'2011), Paris, France, May 2011. Available at http://ttool.telecom-paristech.fr/docs/notere11_telecomparistech.pdf.
  6. Joeri de Ruiter and Erik Poll. Formal Analysis of the EMV Protocol Suite. In Theory of Security and Applications (TOSCA'11), March-April 2011. Available at http://www.cs.ru.nl/E.Poll/papers/emv.pdf.
  7. Ben Smyth, Mark Ryan and Liqun Chen. Formal analysis of anonymity in ECC-based Direct Anonymous Attestation schemes. In Proceedings of the Eighth International Workshop on Formal Aspects of Security and Trust (FAST'11). Available at http://www.cs.bham.ac.uk/~mdr/research/papers/pdf/11-ecc-daa.pdf
  8. Mihhail Aizatulin, Andrew Gordon, and Jan Jürjens. Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution. In CCS 2011. Available at http://users.mct.open.ac.uk/ma4962/files/extracting2011-full.pdf.
  9. Sebastian Mödersheim and Paolo Modesti. Verifying SeVeCom Using Set-based Abstraction. In 7th IEEE International Wireless Communications and Mobile Computing Conference (IWCMC 2011), Vehicular Communications Symposium, Istanbul, Turkey, 2011. Available at http://www2.imm.dtu.dk/~samo/sevecom.pdf.
2012
  1. Myrto Arapinis, Sergiu Bursuc and Mark Ryan. Privacy supporting cloud computing: ConfiChair, a case study. In Principles of Security and Trust (POST'12), LNCS 7215, Springer, 2012. Available at http://www.cs.bham.ac.uk/~mdr/research/papers/pdf/12-confichair.pdf
  2. Myrto Arapinis, Sergiu Bursuc and Mark Ryan. Reduction of equational theories for verification of trace equivalence: re-encryption, associativity and commutativity. In Principles of Security and Trust (POST'12), LNCS 7215, Springer, 2012. Available at http://www.cs.bham.ac.uk/~mdr/research/papers/pdf/12-renc.pdf
  3. Myrto Arapinis, Vincent Cheval, and Stéphanie Delaune. Verifying Privacy-Type Properties in a Modular Way, CSF 2012. Available at http://www.cs.bham.ac.uk/~arapinmd/pdf/ACD12.pdf.
  4. Sepideh Asadi and Hadi Shahriar Shahhoseini. Formal Security Analysis of Authentication in SNMPv3 Protocol by An Automated Tool. In Sixth International Symposium on Telecommunications (IST), pages 1060-1064, 2012. Available at http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6483143.
  5. Michael Backes, Alex Busenius, Catalin Hritcu. On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols. 4th NASA Formal Methods Symposium (NFM 2012), pages 371-387, April 2012. Available at http://www.infsec.cs.uni-saarland.de/~hritcu/publications/expi2java-full.pdf.
  6. Chetan Bansal, Karthikeyan Bhargavan, and Sergio Maffeis. Discovering Concrete Attacks on Website Authorization by Formal Analysis, CSF 2012. Available at http://prosecco.inria.fr/personal/karthik/pubs/discovering_concrete_attacks_csf12.pdf.
  7. Xihui Chen, Gabriele Lenzini, Sjouke Mauw and Jun Pang. A group signature based electronic toll pricing system. In Proc. 7th Conference on Availability, Reliability and Security - ARES'12, IEEE Computer Society, 2012. Available at http://satoss.uni.lu/members/jun/papers/ARES12.pdf.
  8. Maria Christofi and Aline Goujet. Formal Verification of the mERA-Based eServices with Trusted Third Party Protocol. In Information Security and Privacy Research, IFIP Advances in Information and Communication Technology, volume 376, 2012, pp 299-314. Available at http://link.springer.com/chapter/10.1007%2F978-3-642-30436-1_25.
  9. Véronique Cortier, Jan Degrieck, and Stéphanie Delaune. Analysing Routing Protocols: Four Nodes Topologies Are Sufficient. In Principles of Security and Trust (POST'12), LNCS 7215, Springer, 2012. Available at http://www.loria.fr/~cortier/Publications/b2hd-post12-routing.html.
  10. Véronique Cortier and Cyrille Wiedling. A formal analysis of the Norwegian e-voting protocol. In Principles of Security and Trust (POST'12), LNCS 7215, Springer 2012. Available at http://www.loria.fr/~cortier/Publications/b2hd-post12-vote.html.
  11. Naipeng Dong, Hugo Jonker, and Jun Pang. Formal analysis of privacy in an eHealth protocol. In Proc. 17th European Symposium on Research in Computer Security - ESORICS'12, Lecture Notes in Computer Science 7459, pp. 325-342. Springer-Verlag, 2012. Available at http://satoss.uni.lu/members/jun/papers/ESORICS12.pdf.
  12. H. M. N. Al Hamadi, C. Y. Yeun, M. J. Zemerly, M. A. Al-Qutayri, A. Gawanme. Verifying Mutual Authentication for the DLK Protocol using ProVerif tool. In International Journal for Information Security Research (IJISR), Volume 2, Issues 1/2, March/June 2012. Available at http://infonomics-society.org/IJISR/IJISR_Paper%203.pdf.
  13. Alisa Pankova and Peeter Laud. Symbolic Analysis of Cryptographic Protocols Containing Bilinear Pairings, CSF 2012. Available at http://research.cyber.ee/~peeter/research/csf12.pdf.
2013
  1. Guangdong Bai, Guozhu Meng, Jike Lei, Sai Sathyanarayan Venkatraman, Prateek Saxena, Jun Sun, Yang Liu and Jinsong Dong. AuthScan: Automatic Extraction of Web Authentication Protocols From Implementations. In 20th Annual Network & Distributed System Security Symposium (NDSS'13). Available at http://www.comp.nus.edu.sg/~prateeks/papers/AuthScan.pdf.
  2. Myrto Arapinis, Véronique Cortier, Steve Kremer, and Mark D. Ryan. Practical Everlasting Privacy. In Proceedings of the 2nd Conferences on Principles of Security and Trust (POST'13), pp. 21-40, Lecture Notes in Computer Science 7796, Springer, Rome, Italy, March 2013. Available at http://www.loria.fr/~skremer/Publications/b2hd-ACKR-post13.html.
  3. Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis. 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, 2013. Available at http://prosecco.inria.fr/personal/karthik/pubs/keys-to-the-cloud-post13.pdf.
  4. Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech. Formal Verification of e-Auction Protocols. In Proceedings of the 2nd Conferences on Principles of Security and Trust (POST'13), pp. 247-266, Lecture Notes in Computer Science 7796, Springer, Rome, Italy, March 2013. Available at http://www-verimag.imag.fr/~lakhnech/papers/post2013.pdf.
  5. Florian Böhl and Dominique Unruh. Symbolic Universal Composability. In 26th Computer Security Foundations Symposium (CSF'13), pages 257-271, June 2013. Available at http://www.cs.ut.ee/~unruh/publications/symbolic-uc.html.
  6. Morten Dahl and Ivan Damgård. Universally Composable Symbolic Analysis for Two-Party Protocols based on Homomorphic Encryption. Cryptology ePrint Archive: Report 2013/296. Available at http://eprint.iacr.org/2013/296.
  7. Aybek Mukhamedov, Andrew D. Gordon, Mark Ryan. Towards a Verified Reference Implementation of a Trusted Platform Module. In Security Protocols XVII, Lecture Notes in Computer Science, volume 7028, pp 69-81, 2013. Available at http://link.springer.com/chapter/10.1007/978-3-642-36213-2_11.
  8. Hongyuan Wang, Liehuang Zhu, Zhenghe Yang, and Lejian Liao. A new hierarchical and scalable group key exchange protocol with XOR operation. In: International Journal of Wireless and Mobile Computing, volume 6, number 4, pp. 355-361, 2013. Available at http://inderscience.metapress.com/content/v4240g035r75x14m/.
  9. Pierre Kleberger and Guilhem Moulin. Short Paper: Formal Verification of an Authorization Protocol for Remote Vehicle Diagnostics. In 2013 IEEE Vehicular Networking Conference, pp. 202-205, 2013. Available at http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6737613&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6737613.
  10. Kavitha Ammayappan. Seamless interoperation of LTE-UMTS-GSM requires flawless UMTS and GSM. In 2013 Second International Conference on Advanced Computing, Networking and Security, pp. 169-174, 2013. Available at http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6714158.
  11. Donglai Fu, Xinguang Peng, and Yuli Yang. Authentication of the Command TPM_CertifyKey in the Trusted Platform Module. In Telkomnika, Vol. 11, No. 2, February 2013, pp. 855~863. Available at http://www.iaesjournal.com/online/index.php/TELKOMNIKA/article/view/2034.
  12. Khaoula Marzouki, Amira Radhouani, and Narjes Ben Rajeb. Formal Verification of Secrecy, Coercion Resistance and Verifiability Properties for a Remote Electronic Voting Protocol. In International Journal of Information Security and Privacy, 7(2):57-85, 2013. Available at http://www.igi-global.com/article/formal-verification-of-secrecy-coercion-resistance-and-verifiability-properties-for-a-remote-electronic-voting-protocol/87425.
  13. Christoph Busold, Ahmed Taha, Christian Wachsmann, Alexandra Dmitrienko, Hervé Seudié, Majid Sobhani, and Ahmad-Reza Sadeghi. Smart keys for cyber-cars: secure smartphone-based NFC-enabled car immobilizer. In CODASPY '13 Proceedings of the third ACM conference on Data and application security and privacy, pages 233-242. Available at http://www.ukp.tu-darmstadt.de/fileadmin/user_upload/Group_TRUST/PubsPDF/codaspy086-busold.pdf.
2014
  1. Michael Backes, Esfandiar Mohammadi and Tim Ruffing. Computational Soundness Results for ProVerif: Bridging the Gap from Trace Properties to Uniformity. In Principles of Security and Trust (POST'14), Lecture Notes in Computer Science, volume 8414, pp. 42-62, 2014. Available at http://www.infsec.cs.uni-saarland.de/~mohammadi/paper/bridge.pdf.
  2. Piergiuseppe Bettassa Copet and Riccardo Sisto. Automated Formal Verification of Application-specific Security Properties. In Engineering Secure Software and Systems (ESSoS), Lecture Notes in Computer Science, volume 8364, pp 45-59, 2014. Available at http://link.springer.com/chapter/10.1007/978-3-319-04897-0_4.
  3. Qi Xie, Bin Hu, Xiao Tan, Mengjie Bao, and Xiuyuan Yu. Robust Anonymous Two-Factor Authentication Scheme for Roaming Service in Global Mobility Network. In Wireless Personal Communications, January 2014, Volume 74, Issue 2, pp 601-614. Available at http://link.springer.com/article/10.1007/s11277-013-1309-3.
  4. Jesus Diaz, David Arroyo, and Francisco B. Rodriguez. A formal methodology for integral security design and verification of network protocols. In Journal of Systems and Software, volume 89, March 2014, Pages 87-98. Available at http://www.sciencedirect.com/science/article/pii/S0164121213002355.
  5. Jesus Diaz, David Arroyo, and Francisco B. Rodriguez. On securing online registration protocols: Formal verification of a new proposal. In Knowledge-Based Systems, volume 59, March 2014, Pages 149-158. Available at http://www.sciencedirect.com/science/article/pii/S0950705114000227.
  6. S. W. Xu, H. G. Zhang, Z. Dai, X. F. Dai, J. D. Chen, "Modeling and Reasoning about States in Late Launch Based on Horn Clauses", Advanced Materials Research, Vols 915-916, pp. 1350-1356, Apr. 2014. http://www.scientific.net/AMR.915-916.1350.
  7. Li Li, Jun Pang, Yang Liu, Jun Sun, Jin Song Dong. Symbolic Analysis of an Electric Vehicle Charging Protocol. In Engineering of Complex Computer Systems (ICECCS), 2014 19th International Conference on, Aug. 2014. Available at http://dx.doi.org/10.1109/ICECCS.2014.11.
  8. Gang Shen, Xiaohong Li, Ruitao Feng, Guangquan Xu, Jing Hu, Zhiyong Feng. An Extended UML Method for the Verification of Security Protocols. In Engineering of Complex Computer Systems (ICECCS), 2014 19th International Conference on, Aug. 2014. Available at http://dx.doi.org/10.1109/ICECCS.2014.12.
  9. Adarsh Kumar, Krishna Gopal, Alok Aggarwal. Design and Analysis of Lightweight Trust Mechanism for Accessing Data in MANETs. In KSII Transactions on Internet and Information Systems (TIIS) Vol.8 No.3, 2014.3, 1119-1143 (25 pages). Available at http://www.dbpia.co.kr/Journal/ArticleDetail/3531952.
  10. Qi Xie, Bin Hu, Na Dong, Duncan S. Wong. Anonymous Three-Party Password-Authenticated Key Exchange Scheme for Telecare Medical Information Systems. In PLOS one. Available at http://dx.doi.org/10.1371/journal.pone.0102747.
  11. Qi Xie, Na Dong, Duncan S. Wong, and Bin Hu. Cryptanalysis and security enhancement of a robust two-factor authentication and key agreement protocol. In International Journal of Communication Systems, Oct. 2014. Available at http://dx.doi.org/10.1002/dac.2858.
  12. Li Xi, Dengguo Feng. Formal Analysis of DAA-Related APIs in TPM 2.0. In Network and System Security, Lecture Notes in Computer Science Volume 8792, 2014, pp 421-434. Available at http://link.springer.com/chapter/10.1007/978-3-319-11698-3_32.
  13. Changhee Hahn, Hyunsoo Kwon, Daeyoung Kim, Kyungtae Kang, Junbeom Hur. A Privacy Threat in 4th Generation Mobile Telephony and Its Countermeasure. In Wireless Algorithms, Systems, and Applications Lecture Notes in Computer Science Volume 8491, 2014, pp 624-635. Available at http://link.springer.com/chapter/10.1007/978-3-319-07782-6_56.
  14. Qi Xie, Wen-hao Liu, Sheng-bao Wang, Bin Hu, Na Dong, and Xiu-yuan Yu. Robust password and smart card based authentication scheme with smart card revocation. In Journal of Shanghai Jiaotong University (Science), August 2014, Volume 19, Issue 4, pp 418-424. Available at http://link.springer.com/article/10.1007/s12204-014-1518-2.
  15. Noomene Ben Henda, Karl Norrman. Formal Analysis of Security Procedures in LTE - A Feasibility Study. In Research in Attacks, Intrusions and Defenses, Lecture Notes in Computer Science Volume 8688, 2014, pp 341-361. Available at http://link.springer.com/chapter/10.1007/978-3-319-11379-1_17.
  16. Jannik Dreier, Hugo Jonker, Pascal Lafourcade. Secure Auctions without Cryptography. In Fun with Algorithms, Lecture Notes in Computer Science Volume 8496, 2014, pp 158-170. Available at http://link.springer.com/chapter/10.1007/978-3-319-07890-8_14.
  17. Ali Kassem, Pascal Lafourcade, and Yassine Lakhnech. Formal verification of e-reputation protocols. In Foundations and Practice of Security - 7th International Symposium, FPS 2014, Montréal, Canada, Lecture Notes in Computer Science. Springer, 2014. Available at http://sancy.univ-bpclermont.fr/~lafourcade/PAPERS/PDF/reputation_main.pdf.
  18. Alessandro Bruni, Michal Sojka, Flemming Nielson, Hanne Riis Nielson. Formal Security Analysis of the MaCAN Protocol. In Integrated Formal Methods, Lecture Notes in Computer Science Volume 8739, 2014, pp 241-255. Available at http://link.springer.com/chapter/10.1007/978-3-319-10181-1_15.
  19. Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, and Sergio Maffeis. Discovering concrete attacks on website authorization by formal analysis. Journal of Computer Security, 22(4):601-657, April 2014. Available at http://iospress.metapress.com/content/c1q6715h75m07r4n/?p=0374f48ea48047e7a718a6617c9b3bf3&pi=4.
2015
  1. Myrto Arapinis, Vincent Cheval and Stephanie Delaune. Composing security protocols: from confidentiality to privacy. 4th International Conference on Principles of Security and Trust (POST 2015), April 2015. Available at http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-post15.pdf.
  2. Tom Chothia, Ben Smyth and Christopher Staite. Automatically checking commitment protocols in ProVerif without false attacks. 4th International Conference on Principles of Security and Trust (POST 2015), April 2015. Available at http://bensmyth.com/publications/2015-automated-verification-of-secrecy-using-phases/.
  3. Jannik Dreier, Rosario Giustolisi, Ali Kassem, Pascal Lafourcade, Gabriele Lenzini. A Framework for Analyzing Verifiability in Traditional and Electronic Exams. In Information Security Practice and Experience, Lecture Notes in Computer Science Volume 9065, 2015, pp 514-529. Available at http://link.springer.com/chapter/10.1007/978-3-319-17533-1_35.
  4. Marouane Fazouane, Henning Kopp, Rens W. van der Heijden, Daniel Le Métayer, Frank Kargl. Formal Verification of Privacy Properties in Electric Vehicle Charging. In Engineering Secure Software and Systems Lecture Notes in Computer Science Volume 8978, 2015, pp 17-33. Available at http://link.springer.com/chapter/10.1007/978-3-319-15618-7_2.
  5. Alessandro Bruni, Sebastian Mödersheim, Flemming Nielson, Hanne Riis Nielson. Set-Pi: Set Membership Pi-Calculus. In Computer Security Foundations Symposium (CSF'15), pages 185-198. Available at http://www2.compute.dtu.dk/~albr/setpi.pdf.
  6. Michael Backes, Fabian Bendun, Matteo Maffei, Esfandiar Mohammadi, Kim Pecina. Symbolic Malleable Zero-Knowledge Proofs. In Computer Security Foundations Symposium (CSF'15), pages 412-480. Available at https://www.infsec.cs.uni-saarland.de/~mohammadi/paper/malleable_zk.pdf.
  7. Ben Smyth, Mark D. Ryan & Liqun Chen (2015) Formal analysis of privacy in Direct Anonymous Attestation schemes. Science of Computer Programming, 111(2). Available at http://www.bensmyth.com/publications/2012-Direct-Anonymous-Attestation-privacy-definition/.
2016
  1. Paolo Modesti. AnBx: Automatic Generation and Verification of Security Protocols Implementations. In Foundations and Practice of Security, 8th International Symposium, FPS 2015, Clermont-Ferrand, France, October 26-28, 2015, Revised Selected Papers. Volume 9482 of the series Lecture Notes in Computer Science pp 156-173. Available at http://www.dais.unive.it/~modesti/docs/fps2015.pdf.
  2. Sebastian A. Mödersheim and Alessandro Bruni. AIF-omega: Set-Based Protocol Abstraction with Countable Families. In Principles of Security and Trust (POST'16), LNCS volume 9635, pp 233-253. Available at http://www.imm.dtu.dk/~samo/aif-omega.pdf.
  3. Lucca Hirschi, David Baelde, and Stéphanie Delaune. A Method for Verifying Privacy-Type Properties: The Unbounded Case. In IEEE Symposium on Security and Privacy. Available at http://www.lsv.ens-cachan.fr/~hirschi/mes_publis.php?onlykey=HBD-sp16.
  4. Kim Thuat Nguyen, Nouha Oualha, and Maryline Laurent. Authenticated Key Agreement Mediated by a Proxy Re-encryptor for the Internet of Things. In ESORICS'16. Available at http://link.springer.com/chapter/10.1007/978-3-319-45741-3_18.

Tools

Courses on ProVerif

ProVerif is taught at the MPRI, course 2-30. Here is a list of some courses on ProVerif by other researchers:

If you have written a research paper or a tool using ProVerif, or teach a course on ProVerif, and want it to be added to this page, or if you want the reference to your paper/tool/course to be removed or corrected, please contact Bruno Blanchet.


Bruno Blanchet