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 https://bhargavan.info/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 https://bhargavan.info/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 https://bhargavan.info/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 https://doi.org/10.1109/ICWS.2005.138.
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 https://bhargavan.info/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 https://bhargavan.info/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 https://dl.acm.org/doi/10.1145/1128817.1128828.
  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 https://doi.org/10.1007/978-3-540-72738-5_6.
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 https://ieeexplore.ieee.org/document/4556687
  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 https://bhargavan.info/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 https://bhargavan.info/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 https://bhargavan.info/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 https://sec.uni-stuttgart.de/_media/publications/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 https://people.irisa.fr/Stephanie.Delaune/PUBLICATIONS-HTML/b2hd-DKR-jcs08.html.
  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 https://sec.uni-stuttgart.de/_media/publications/KuestersTruderung-CSF-2009.pdf.
  5. Peeter Laud and Meelis Roos. Formal Analysis of the Estonian Mobile-ID Protocol. In Nordic Conference on Secure IT Systems (NordSec'09), pages 271-286. Available at https://doi.org/10.1007/978-3-642-04766-4_19.
  6. 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 https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=5416378.
  7. 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 https://doi.org/10.1109/ACSAC.2009.40
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 https://doi.org/10.1109/CSF.2010.13.
  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 https://www.researchgate.net/profile/Andrew_Butterfield/publication/229051596_ProVerif_Analysis_of_the_ZRTP_Protocol/links/02bfe5130ac0e06d36000000/ProVerif-Analysis-of-the-ZRTP-Protocol.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 https://people.irisa.fr/Stephanie.Delaune/PUBLICATIONS-HTML/b2hd-DKRS-fast10.html.
  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 https://markryan.eu/research/statverif/files/11-state-appi.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 https://doi.org/10.1145/2046707.2046745.
  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 https://doi.org/10.1109/CSF.2012.16.
  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 https://catalin-hritcu.github.io/publications/expi2java-nfm2012.pdf.
  6. Chetan Bansal, Karthikeyan Bhargavan, and Sergio Maffeis. Discovering Concrete Attacks on Website Authorization by Formal Analysis, CSF 2012. Available at https://bhargavan.info/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 https://members.loria.fr/VCortier/files/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 https://members.loria.fr/VCortier/files/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/wp-content/uploads/ijisr/volume-3-2013/Verifying-Mutual-Authentication-for-the-DLK-Protocol-using-ProVerif-tool.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 https://impillar.github.io/files/ndss2013authscan.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 https://members.loria.fr/SKremer/files/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 https://bhargavan.info/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://kodu.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://dx.doi.org/10.1504/IJWMC.2013.056550.
  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 https://doi.org/10.1109/VNC.2013.6737613.
  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 https://www.researchgate.net/publication/275414959_Authentication_of_the_Command_TPM_CertifyKey_in_the_Trusted_Platform_Module.
  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 https://doi.org/10.1145/2435349.2435382.
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 https://doi.org/10.1007/978-3-642-54792-8_3.
  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 https://doi.org/10.3837/tiis.2014.03.024.
  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 https://sancy.iut.uca.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 https://hal.inria.fr/hal-01102202/.
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. Giampaolo Bella, Rosario Giustolisi, Gabriele Lenzini, and Peter Y. A. Ryan. A Secure Exam Protocol Without Trusted Parties. In: IFIP International Information Security and Privacy Conference (SEC 2015), IFIP Advances in Information and Communication Technology book series (IFIPAICT), volume 455, pp. 495-509. Available at https://link.springer.com/chapter/10.1007/978-3-319-18467-8_33.
  5. 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.
  6. 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 https://doi.org/10.1109/CSF.2015.20.
  7. 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://doi.org/10.1109/CSF.2015.35.
  8. 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. Sergiu Bursuc. Secure Two-Party Computation in Applied Pi-Calculus: Models and Verification. In: Trustworthy Global Computing. LNCS, volume 9533, pp. 1-15. Springer. Available at http://link.springer.com/chapter/10.1007%2F978-3-319-28766-9_1.
  3. 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.
  4. 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 https://people.irisa.fr/Stephanie.Delaune/PUBLICATIONS-HTML/b2hd-HBD-sp16.html.
  5. Michael Denzel, Alessandro Bruni, and Mark D. Ryan. Smart-Guard: Defending User Input from Malware. In: 2016 Intl IEEE Conferences on Ubiquitous Intelligence & Computing, Advanced and Trusted Computing, Scalable Computing and Communications, Cloud and Big Data Computing, Internet of People, and Smart World Congress (UIC/ATC/ScalCom/CBDCom/IoP/SmartWorld). Available at https://doi.org/10.1109/UIC-ATC-ScalCom-CBDCom-IoP-SmartWorld.2016.0089.
  6. 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.
  7. Maxime Puys, Marie-Laure Potet, and Pascal Lafourcade. Formal Analysis of Security Properties on the OPC-UA SCADA Protocol. In: International Conference on Computer Safety, Reliability, and Security (SAFECOMP 2016). LNCS, volume 9922. Springer. Available at https://link.springer.com/chapter/10.1007/978-3-319-45477-1_6.
  8. Joeri de Ruiter, Richard J. Thomas, and Tom Chothia. A Formal Security Analysis of ERTMS Train to Trackside Protocols. In: International Conference on Reliability, Safety, and Security of Railway Systems (RSSRail 2016). LNCS, volume 9707, pp. 53-68. Available at https://link.springer.com/chapter/10.1007/978-3-319-33951-1_4.
  9. Hideki Sakurada, Kazuki Yoneyama, Yoshikazu Hanatani, Maki Yoshida. Analyzing and fixing the QACCE security of QUIC. In: Security Standardisation Research. LNCS, volume 10074, pp. 1--31. Springer. Available at http://link.springer.com/chapter/10.1007%2F978-3-319-49100-4_1.
  10. Park, S., Won, J.-J., Yoon, J., Hoon Kim, K., Han, T. A tiny hypervisor-based trusted geolocation framework with minimized TPM operations. Journal of Systems and Software, volume 122, dec. 2016, pp. 202-214. Available at http://dx.doi.org/10.1016/j.jss.2016.09.026.
  11. Amol H. Shinde and A. J. Umbarkar. Analysis of Cryptographic Protocols AKI, ARPKI and OPT using ProVerif and AVISPA. In: I. J. Computer Network and Information Security, 2016, 3, 34-40. Published Online March 2016 in MECS (http://www.mecs-press.org/) DOI: 10.5815/ijcnis.2016.03.05.
  12. Jintian Lu, Jinli Zhang, Jing Li, Zhongyu Wan, and Bo Meng. Automatic Verification of Security of OpenID Connect Protocol with ProVerif. In: International Conference on P2P, Parallel, Grid, Cloud and Internet Computing (3PGCIC 2016). Lecture Notes on Data Engineering and Communications Technologies (LNDECT), volume 1, pp. 209-220. Available at https://link.springer.com/chapter/10.1007/978-3-319-49109-7_20.
  13. Caimei Wang, Yan Xiong, Wenchao Huang, Huihua Xia, and Jianmeng Huang. Formal Analysis of Selective Disclosure Attribute-Based Credential System in Applied Pi Calculus. In: 2016 IEEE Trustcom/BigDataSE/ISPA. Available at https://ieeexplore.ieee.org/abstract/document/7846927/.
2017
  1. Murat Moran and Dan S. Wallach. Verification of STAR-Vote and Evaluation of FDR and ProVerif. In IFM 2017: Integrated Formal Methods pp 422-436. Available at https://link.springer.com/chapter/10.1007/978-3-319-66845-1_28.
  2. Thibaud Antignac, Mukelabai Mukelabai, and Gerardo Schneider. Specification, design, and verification of an accountability-aware surveillance protocol. In: SAC'17, Proceedings of the Symposium on Applied Computing, pages 1372-1378. Available at https://dl.acm.org/citation.cfm?id=3019826.
  3. Narjes Ben Rajeb, Mouhebeddine Berrima, Matthieu Giraud, and Pascal Lafourcade. Formal Analyze of a Private Access Control Protocol to a Cloud Storage. In: 14th International Conference on Security and Cryptography SECRYPT 2017. Available at https://hal.archives-ouvertes.fr/hal-01689790/.
  4. Letitia W. Li, Florian Lugou, and Ludovic Apvrille. "Security-aware Modeling and Analysis for HW/SW Partitioning." MODELSWARD. 2017. Available at https://pdfs.semanticscholar.org/ff99/b12c05da220b898a24d51f2f77db69d81f7a.pdf.
  5. Caimei Wang, Yan Xiong, Wenchao Huang, Huihua Xia, Jianmeng Huang, and Cheng Su. A Verified Secure Protocol Model of OAuth Dynamic Client Registration. In: 3rd International Conference on Big Data Computing and Communications (BIGCOM 2017). Available at https://ieeexplore.ieee.org/abstract/document/8113053/.
  6. Jayana C. Kaneriya, Jalpa Khamar, and Avani Dadhania. Verification of Security Protocols Using ProVerif. In: International Journal of Engineering Development and Research, Volume 5, Issue 2. Available at https://www.ijedr.org/papers/IJEDR1702065.pdf.
  7. Abisha D. Perlustration on Authentication Protocols in 4G (LTE/LTE-A) Using ProVerif. In: Journal of Network Security Computer Networks, vol. 3, No 1,2,3 (2017). Available at http://matjournals.in/index.php/JONSCN/article/view/1892.
  8. Jintian Lu, Lili Yao, Xudong He, and Bo Meng. Improvement of OpenID Connect protocol and its security analysis. In: Journal of Computer Applications. Available at http://en.cnki.com.cn/Article_en/CJFDTOTAL-JSJY201705023.htm.
  9. Weijin Wang, Jingbin Liu, Yu Qin, and Dengguo Feng. Formal Analysis of a TTP-Free Blacklistable Anonymous Credentials System. In: International Conference on Information and Communications Security (ICICS 2017), LNCS, volume 10631, pp. 3-16. Available at https://link.springer.com/chapter/10.1007/978-3-319-89500-0_1.
  10. Dai Watanabe, Hisao Sakazaki, and Kunihiko Miyazaki. Representative System and Security Message Transmission using Re-encryption Scheme Based on Symmetric-key Cryptography. In: Journal of Information Processing, vol 25, pp. 67-74, Jan. 2017. Available at https://www.jstage.jst.go.jp/article/ipsjjip/25/0/25_67/_article/-char/ja/.
  11. He X., Tian J. (2017) A Trusted VM Live Migration Protocol in IaaS. In: Xu M., Qin Z., Yan F., Fu S. (eds) Trusted Computing and Information Security. CTCIS 2017. Communications in Computer and Information Science, vol 704. Springer, Singapore. Available at https://doi.org/10.1007/978-981-10-7080-8_4.
  12. Piergiuseppe Bettassa Copet, Guido Marchetto, Riccardo Sisto, and Luciana Costa. Formal verification of LTE-UMTS and LTE–LTE handover procedures. Computer Standards & Interfaces, Volume 50, February 2017, Pages 92-106. Available at https://iris.polito.it/retrieve/handle/11583/2659528/150510/paper.pdf and https://www.sciencedirect.com/science/article/abs/pii/S092054891630071X.
2018
  1. V. Cheval, V. Cortier and M. Turuani. A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. In Proceedings of the 31th IEEE Computer Security Foundations Symposium (CSF'18). Available at https://chevalvi.gitlabpages.inria.fr/chevalvi/files/CCT-csf18.pdf
  2. Charlie Jacomme and Steve Kremer. An extensive formal analysis of multi-factor authentication protocols. In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'18). See https://members.loria.fr/SKremer/files/Publications/b2hd-JK-csf18.html
  3. Cheng Shi and Kazuki Yoneyama. Verification of LINE Encryption Version 1.0 Using ProVerif. In International Workshop on Security, IWSEC 2018: Advances in Information and Computer Security. LNCS, volume 11049, pp. 158-173, available at https://link.springer.com/chapter/10.1007/978-3-319-97916-8_11.
  4. Anongporn Salaiwarakul. A Secure Fingerprint Authentication Protocol. In: Journal of Telecommunication, Electronic, and Computer Engineering, Vol 10, No 1-5. Available at https://jtec.utem.edu.my/jtec/article/view/3627.
  5. Sandipa Roy, Santanub Chatterjee, and Gautamb Mahapatra. An efficient biometric based remote user authentication scheme for secure internet of things environment. In: Journal of Intelligent & Fuzzy Systems, vol. 34, no. 3, pp. 1403-1410, 2018. Available at https://content.iospress.com/articles/journal-of-intelligent-and-fuzzy-systems/ifs169435.
  6. Majid R Alshammari and Khaled M Elleithy. Efficient Key Distribution Protocol for Wireless Sensor Networks. In: Computing and Communication Workshop and Conference (CCWC), 2018 IEEE 8th Annual (pp. 980-985). IEEE. Available at https://www.researchgate.net/profile/Khaled_Elleithy/publication/323563608_Efficient_key_distribution_protocol_for_wireless_sensor_networks/links/5ab2826e458515ecebeebfad/Efficient-key-distribution-protocol-for-wireless-sensor-networks.pdf.
  7. Khalid Mahmood, Shehzad Ashraf Chaudhry, Husnain Naqvi, Saru Kumari, Xiong Li, Arun Kumar Sangaiah. An elliptic curve cryptography based lightweight authentication scheme for smart grid communication. In: Future Generation Computer Systems, Volume 81, April 2018, Pages 557-565. Available at https://www.sciencedirect.com/science/article/pii/S0167739X17309263.
  8. Olivier Pereira, Florentin Rochet, and Cyrille Wiedling. Formal Analysis of the FIDO 1.x Protocol. In: International Symposium on Foundations and Practice of Security (FPS 2017), LNCS, volume 10723, pp. 68-82, Feb. 2018. Available at https://link.springer.com/chapter/10.1007/978-3-319-75650-9_5.
  9. Alessandro Bruni, Thorvald Sahl Jørgensen, Theis Grønbech Petersen and Carsten Schürmann. Formal Verification of Ephemeral Diffie-Hellman Over COSE (EDHOC). In: Security Standardisation Research, 4th International Conference, SSR 2018. LNCS, volume 11322, pp. 21-36. Available at https://link.springer.com/chapter/10.1007/978-3-030-04762-7_2.
  10. Iness Ben Guirat and Harry Halpin. Formal verification of the W3C Web Authentication Protocol. In Proceedings of the 5th Annual Symposium and Bootcamp on Hot Topics in the Science of Security - HoTSoS '18, 2018. Available at https://doi.org/10.1145/3190619.3190640 and https://hal.inria.fr/hal-01966563.
  11. Riccardo Sisto, Piergiuseppe Bettassa Copet, Matteo Avalle, and Alfredo Pironti. Formally sound implementations of security protocols with JavaSPI. Formal Aspects of Computing 30, pages 279–317 (2018). Available at https://iris.polito.it/retrieve/handle/11583/2695975/181376/AuthorsPostPrint.pdf and https://link.springer.com/article/10.1007/s00165-017-0449-8.
  12. Hiroyuki Okazaki, Yuichi Futa, and Kenichi Arai. Suitable Symbolic Models for Cryptographic Verification of Secure Protocols in ProVerif. In 2018 International Symposium on Information Theory and Its Applications (ISITA). IEEE. Available at https://doi.org/10.23919/ISITA.2018.8664273.
  13. Ridhwan Dewoprabowo, Muhammad Arzaki, and Yanti Rusmawati. Formal Verification of Divide and Conquer Key Distribution Protocol Using ProVerif and TLA+. In 2018 International Conference on Advanced Computer Science and Information Systems (ICACSIS). Available at https://doi.org/10.1109/ICACSIS.2018.8618173.
  14. S. Usha, S. Kuppuswami, and M. Karthik. A New Enhanced Authentication Mechanism Using Session Key Agreement Protocol. In Cybernetics and information technologies, Volume 18, No 4, Bulgarian academy of sciences, Sofia, 2018. Available at https://doi.org/10.2478/cait-2018-0048.
  15. Lili Yao, Jiabing Liu, Dejun Wang, Jing Li, and Bo Meng. Formal Analysis of SDN Authentication Protocol with Mechanized Protocol Verifier in the Symbolic Model. In International Journal of Network Security, Vol.20, No.6, PP.1125-1136, Nov. 2018. Available at https://doi.org/10.6633/IJNS.201811_20(6).13.
  16. Marwa Chaieb, Souheib Yousfi, Pascal Lafourcade, and Riadh Robbana. Verify-Your-Vote: A Verifiable Blockchain-Based Online Voting Protocol. In European, Mediterranean, and Middle Eastern Conference on Information Systems (EMCIS 2018), pp. 16--30, Lecture Notes in Business Information Processing,volume 341, Springer. Available at https://doi.org/10.1007/978-3-030-11395-7_2.
2019
  1. Nadim Kobeissi, Georgio Nicolas, and Karthikeyan Bhargavan. Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols. In 4th IEEE European Symposium on Security and Privacy (EuroS&P'19). Available at https://eprint.iacr.org/2018/766.
  2. Lucca Hirschi and Cas Cremers. Improving Automated Symbolic Analysis of Ballot Secrecy for E-voting Protocols: A Method Based on Sufficient Conditions. In 4th IEEE European Symposium on Security and Privacy (EuroS&P'19). Available at https://members.loria.fr/LHirschi/pdfs/EuroSP19_evoting.pdf
  3. V. Cortier, A. Filipiak, and J. Lallemand. BeleniosVS: Secrecy and Verifiability Against a Corrupted Voting Device. In 32nd IEEE Computer Security Foundations Symposium (CSF'19). Available at https://members.loria.fr/VCortier/files/Publications/b2hd-beleniosVS-CSF19.html
  4. Di Long Li and Alwen Tiu. Combining ProVerif and Automated Theorem Provers for Security Protocol Verification. In CADE 2019: Automated Deduction - CADE 27, pp. 354-365. Long version available at https://github.com/darrenldl/ProVerif-ATP/blob/master/paper/CADE-27_paper-42_Di_Long_Li_and_Alwen_Tiu_full.pdf.
  5. Pietro Tedeschi, Savio Sciancalepore, Areej Eliyan, and Roberto Di Pietro. "LiKe: Lightweight Certificateless Key Agreement for Secure IoT Communications." IEEE Internet of Things Journal 7, no. 1 (2019): 621-638. Available at https://www.researchgate.net/profile/Pietro_Tedeschi/publication/337274918_LiKe_Lightweight_Certificateless_Key_Agreement_for_Secure_IoT_Communications/links/5dce4c55a6fdcc7e1381be16/LiKe-Lightweight-Certificateless-Key-Agreement-for-Secure-IoT-Communications.pdf
  6. Togo Yoshimura, Kenichi Arai, Hiroyuki Okazaki, and Yuichi Futa. Formalization of Security Requirements and Attack Models for Cryptographic Hash Functions in ProVerif. In Proceedings of the International Conference on Security and Management (SAM). Available at https://www.proquest.com/openview/f129bf4648500186ead69b86438290e4/1?cbl=1976342.
  7. Kaouthar Chetioui, Ghizlane Orhanou, Hicham Bensaid, Ilias Cherkaoui, and Youness Chibi. Formal Verification of Confidentiality in DNSSEC and E-DNSSEC Protocols using pi-calculus and ProVerif. In Procedia Computer Science, Volume 160, 2019, Pages 752-757. Special issue The 10th International Conference on Emerging Ubiquitous Systems and Pervasive Networks (EUSPN-2019) / The 9th International Conference on Current and Future Trends of Information and Communication Technologies in Healthcare (ICTH-2019) / Affiliated Workshops. Available at https://doi.org/10.1016/j.procs.2019.11.015.
  8. Jintian Lu, Xudong He, Yitong Yang, Dejun Wang, and Bo Meng. Automatic Verification of Security of Identity Federation Security Protocol Based on SAML2.0 with ProVerif in the Symbolic Model. In International Journal of Network Security. Available at http://isrc.ccs.asia.edu.tw/~vdoi/upload/JID190002/2019/1816-3548-2019-00011.pdf.
  9. A. Jabbari and J. B. Mohasefi. Improvement in new three-party-authenticated key agreement scheme based on chaotic maps without password table. In Nonlinear Dynamics, volume 95, pages 3177–3191 (2019). Available at https://doi.org/10.1007/s11071-018-04748-y.
  10. Jawad Iftikhar, Sajid Hussain, Khwaja Mansoor, Zeeshan Ali, and Shehzad Ashraf Chaudhry. Symmetric-Key Multi-Factor Biometric Authentication Scheme. In 2019 2nd International Conference on Communication, Computing and Digital systems (C-CODE). Available at https://doi.org/10.1109/C-CODE.2019.8680999.
  11. Chien-Ming Chen, King-Hang Wang, Kuo-Hui Yeh, Bin Xiang, and Tsu-Yang Wu. Attacks and solutions on a three-party password-based authenticated key exchange protocol for wireless communications. In Journal of Ambient Intelligence and Humanized Computing, volume 10, pages 3133–3142 (2019). Available at https://doi.org/10.1007/s12652-018-1029-3.
  12. R. Ameur-Boulifa, F. Lugou, and L. Apvrille. SysML Model Transformation for Safety and Security Analysis. In: Hamid, B., Gallina, B., Shabtai, A., Elovici, Y., Garcia-Alfaro, J. (eds) Security and Safety Interplay of Intelligent Software Systems. CSITS ISSA 2018 2018. Lecture Notes in Computer Science(), vol 11552. Springer, Cham. Available at https://doi.org/10.1007/978-3-030-16874-2_3.
  13. Wenzheng Liu, Xiaofeng Wang, and Wei Peng. Secure Remote Multi-Factor Authentication Scheme Based on Chaotic Map Zero-Knowledge Proof for Crowdsourcing Internet of Things. In IEEE Access, Volume: 8. Available at https://doi.org/10.1109/ACCESS.2019.2962912.
  14. Lu Zhou, Xiong Li, Kuo-Hui Yeh, Chunhua Su, Wayne Chiu. Lightweight IoT-based authentication scheme in cloud computing circumstance. In Future Generation Computer Systems, Volume 91, February 2019, Pages 244-251. Available at https://doi.org/10.1016/j.future.2018.08.038.
  15. Mamoon M. Saeed, Rashid A. Saeed, and Elsadig Saeid. Preserving Privacy of Paging Procedure in 5thG Using Identity-Division Multiplexing. In 2019 First International Conference of Intelligent Computing and Engineering (ICOICE). Available at https://doi.org/10.1109/ICOICE48418.2019.9035167.
2020
  1. Ahmed Aziz, Pietro Tedeschi, Savio Sciancalepore, and Roberto Di Pietro. "SecureAIS-Securing Pairwise Vessels Communications." IEEE Conference on Communications and Network Security (CNS) IEEE, 2020. Available at https://www.researchgate.net/publication/341287012_SecureAIS_-_Securing_Pairwise_Vessels_Communications
  2. Cheng Shi and Kazuki Yoneyama. Formal Verification of Fair Exchange based on Bitcoin Smart Contracts. Indocrypt 2020. Available at https://link.springer.com/chapter/10.1007/978-3-030-65277-7_5
  3. Ed Kamya Kiyemba Edris, Mahdi Aiash, and Jonathan Kok-Keong Loo. Network Service Federated Identity (NSFId) Protocol for Service Authorization in 5G Network. In 2020 Fifth International Conference on Fog and Mobile Edge Computing (FMEC), Paris, France, 2020, pp. 128-135. Available at http://dx.doi.org/10.1109/FMEC49853.2020.9144706
  4. Ed Kamya Kiyemba Edris, Mahdi Aiash, and Jonathan Kok-Keong Loo. Formal Verification and Analysis of Primary Authentication based on 5G-AKA Protocol. In 2020 Seventh International Conference on Software Defined Systems (SDS), Paris, France, 2020, pp. 256-261. Available at http://dx.doi.org/10.1109/SDS49854.2020.9143899
  5. Muhammad Usama Sardar, Do Le Quoc, Christof Fetzer, Towards Formalization of Enhanced Privacy ID (EPID)-based Remote Attestation in Intel SGX, Euromicro Conference on Digital System Design (DSD), Portorož, Slovenia, 26-28 August 2020. Available at https://www.researchgate.net/publication/342833256_Towards_Formalization_of_Enhanced_Privacy_ID_EPID-based_Remote_Attestation_in_Intel_SGX
  6. Jingjing Zhang, Lin Yang, Weipeng Cao, Qiang Wang. Formal Analysis of 5G EAP-TLS Authentication Protocol Using Proverif. In IEEE Access, volume 8. Available at https://doi.org/10.1109/ACCESS.2020.2969474
  7. Jingjing Zhang, Lin Yang, Xianming Gao, Qiang Wang. Formal analysis of QUIC handshake protocol using ProVerif. In 2020 7th IEEE International Conference on Cyber Security and Cloud Computing (CSCloud)/2020 6th IEEE International Conference on Edge Computing and Scalable Cloud (EdgeCom). Available at https://doi.org/10.1109/CSCloud-EdgeCom49738.2020.00030.
  8. Takehiko Mieno, Togo Yoshimura, Hiroyuki Okazaki, Yuichi Futa, and Kenichi Arai. Formal Verification of Merkle–Damgård Construction in ProVerif. In 2020 International Symposium on Information Theory and Its Applications (ISITA), IEEE. Available at https://ieeexplore.ieee.org/abstract/document/9366163.
  9. Ryoga Noguchi, Yoshikazu Hanatani, and Kazuki Yoneyama. Verification of Group Key Management of IEEE 802.21 using ProVerif. In APKC '20: Proceedings of the 7th ACM Workshop on ASIA Public-Key Cryptography, October 2020, ages 19–27. Available at https://doi.org/10.1145/3384940.3388960.
  10. Rong Zhu, Xiaoxi He, Jiahong Xie, Zongjie Zhang, and Ping Wang. An Improved RFID-based Authentication Protocol for Rail Transit. In 2020 IEEE 14th International Conference on Big Data Science and Engineering (BigDataSE). Available at https://doi.org/10.1109/BigDataSE50710.2020.00017.
  11. Tsu-Yang Wu, Zhiyuan Lee, Mohammad S. Obaidat, Saru Kumari, Sachin Kumar, and Chien-Ming Chen. An Authenticated Key Exchange Protocol for Multi-Server Architecture in 5G Networks. In IEEE Access, volume: 8. Available at https://doi.org/10.1109/ACCESS.2020.2969986.
  12. Sarah Naveed, Aiman Sultan, and Khwaja Mansoor. An Enhanced SIP Authentication Protocol for Preserving User Privacy. In 2020 International Conference on Cyber Warfare and Security (ICCWS). Available at https://doi.org/10.1109/ICCWS48432.2020.9292398.
  13. Yilong Zheng, Shunfang Hu, Liangxiong Wei, Yanru Chen, Hao Wang, Yanbing Yang, Yang Li, Bingjie Xu, Wei Huang, and Liangyin Chen. Design and Analysis of a Security-Enhanced Three-Party Authenticated Key Agreement Protocol Based on Chaotic Maps. In IEEE Access, volume: 8. Available at https://doi.org/10.1109/ACCESS.2020.2979251.
  14. Eman Elemam, Ayman M. Bahaa-Eldin, Nabil H. Shaker, Mohamed Sobh. Formal verification for a PMQTT protocol. In Egyptian Informatics Journal, Volume 21, Issue 3, September 2020, Pages 169-182. Available at https://doi.org/10.1016/j.eij.2020.01.001.
  15. Mehmood Hassan, Aiman Sultan, Ali Afzal Awan, Shahzaib Tahir, and Imran Ihsan. An Enhanced and Secure Multiserver-based User Authentication Protocol. In 2020 International Conference on Cyber Warfare and Security (ICCWS). Available at https://doi.org/10.1109/ICCWS48432.2020.9292383.
  16. Malik Muhammad Sohail, Mehmood Hassan, Khwaja Mansoor, Anwar Ghani, and Khwaja Jawad. An Improved Authentication Protocol for Global Mobility Network (GLOMONET). In 2020 17th International Bhurban Conference on Applied Sciences and Technology (IBCAST), IEEE. Available at https://doi.org/10.1109/IBCAST47879.2020.9044490.
  17. Xueping Zhu, Yanxing Li, and Yuan Lei. A Forwarding Secrecy Based Lightweight Authentication Scheme for Intelligent Logistics. In 2020 IEEE International Conference on Advances in Electrical Engineering and Computer Applications (AEECA). Available at https://doi.org/10.1109/AEECA49918.2020.9213520.
  18. Devender Kumar, Harsh Kumar Singh, and Chhahat Ahlawat. A secure three-factor authentication scheme for wireless sensor networks using ECC. In Journal of Discrete Mathematical Sciences and Cryptography, Volume 23, 2020 - Issue 4. Available at https://doi.org/10.1080/09720529.2019.1627072.
2021
  1. Muhammad Usama Sardar, Rasha Faqeh, and Christof Fetzer. Formal Foundations for Intel SGX Data Center Attestation Primitives. In: International Conference on Formal Engineering Methods (ICFEM), March 2021, Singapore. Available at https://www.researchgate.net/publication/343826554_Formal_Foundations_for_Intel_SGX_Data_Center_Attestation_Primitives.
  2. Muhammad Usama Sardar, Saidgani Musaev, Christof Fetzer. Demystifying Attestation in Intel Trust Domain Extensions via Formal Verification, IEEE Access, 2021. Available at https://www.researchgate.net/publication/351699567_Demystifying_Attestation_in_Intel_Trust_Domain_Extensions_via_Formal_Verification.
  3. Alexander Dax and Robert Künnemann. On the Soundness of Infrastructure Adversaries. In: 2021 IEEE 34th Computer Security Foundations Symposium (CSF). Available at https://doi.ieeecomputersociety.org/10.1109/CSF51468.2021.00039.
  4. Pietro Tedeschi, Savio Sciancalepore, and Roberto Di Pietro. ARID: Anonymous Remote IDentification of Unmanned Aerial Vehicles. In Annual Computer Security Applications Conference (ACSAC'21). Association for Computing Machinery, New York, NY, USA, 207–218. Available at https://doi.org/10.1145/3485832.3485834.
  5. Ed Kamya Kiyemba Edris, Mahdi Aiash, and Jonathan Loo. Formal Verification of Authentication and Service Authorization Protocols in 5G-Enabled Device-to-Device Communications Using ProVerif. In Electronics 2021, 10(13), 1608. Available at https://doi.org/10.3390/electronics10131608.
  6. Ernest-YongYi Yap, Ji-Jian Chin, and Alwyn Goh. Verifying MQV-Based Protocols Using ProVerif. In IT Convergence and Security. LNEE, volume 782, pp 55–63. Springer. Available at https://doi.org/10.1007/978-981-16-4118-3_6.
  7. Dexian Chang, Ning Zhu, and Yingjie Yang. Security Analysis of SDN Access Control Protocol Based on ProVerif. In 2021 IEEE 3rd International Conference on Civil Aviation Safety and Information Technology (ICCASIT). Available at https://doi.org/10.1109/ICCASIT53235.2021.9633403.
  8. Thomas Haines and Rajeev Goré. Improved Verifiability for BeleniosVS. In Sixth International Joint Conference on Electronic Voting E-Vote-ID 2021. 5-8 October 2021. Available at https://eprint.iacr.org/2021/1071.
  9. Muktar Yahuza, Mohd Yamani Idna Idris, Ainuddin Wahid Abdul Wahab, Tarak Nandy, Ismail Bin Ahmedy, and Roziana Ramli. An Edge Assisted Secure Lightweight Authentication Technique for Safe Communication on the Internet of Drones Network. In IEEE Access, volume 9. Available at https://doi.org/10.1109/ACCESS.2021.3060420.
  10. Tsu-Yang Wu, Yu-Qi Lee, Chien-Ming Chen, Yuan Tian, and Najla Abdulrahman Al-Nabhan. An enhanced pairing-based authentication scheme for smart grid communications. In Journal of Ambient Intelligence and Humanized Computing, 2021. Available at https://doi.org/10.1007/s12652-020-02740-2.
  11. Hussam Al-Hamadi, Nida Nasir, Chan Yeob Yeun, and Ernesto Damiani. A Verified Protocol for Secure Autonomous and Cooperative Public Transportation in Smart Cities. In 2021 IEEE International Conference on Communications Workshops (ICC Workshops). Available at https://doi.org/10.1109/ICCWorkshops50388.2021.9473591.
  12. Jingjing Zhang, Lin Yang, Xianming Gao, Gaigai Tang, Jiyong Zhang, and Qiang Wang. Formal Analysis of QUIC Handshake Protocol Using Symbolic Model Checking. In IEEE Access, volume 9. Available at https://doi.org/10.1109/ACCESS.2021.3052578.
  13. Megha Ajit, Sriram Sankaran, and Kurunandan Jain. Formal Verification of 5G EAP-AKA protocol. In 2021 31st International Telecommunication Networks and Applications Conference (ITNAC). Available at https://doi.org/10.1109/ITNAC53136.2021.9652163.
  14. Ajay Kumar, Kumar Abhishek, Kunjal Shah, Suyel Namasudra, and Seifedine Kadry. A novel elliptic curve cryptography-based system for smart grid communication. In International Journal of Web and Grid Services, Vol. 17, No. 4. Available at https://doi.org/10.1504/IJWGS.2021.118398.
  15. Yue Zheng and Chip-Hong Chang. Secure Mutual Authentication and Key-Exchange Protocol between PUF-Embedded IoT Endpoints. In 2021 IEEE International Symposium on Circuits and Systems (ISCAS). Available at https://doi.org/10.1109/ISCAS51556.2021.9401135.
  16. Katharina Hofer-Schmitz. A Formal Analysis of EnOcean’s Teach-in and Authentication. In ARES 21: Proceedings of the 16th International Conference on Availability, Reliability and Security. Available at https://doi.org/10.1145/3465481.3470097.
  17. Ed Kamya Kiyemba Edris, Mahdi Aiash, Jonathan Kok-Keong Loo, and Mohammad Shadi Alhakeem. Formal verification of secondary authentication protocol for 5G secondary authentication. In International Journal of Security and Networks, Vol. 16, No. 4. Available at https://doi.org/10.1504/IJSN.2021.119379.
  18. Jiabing Liu, Xudong He, Huoye Tang, Dejun Wang, and Bo Meng. A Novel Privacy-preserving User Authentication Protocol for Big Data Environment. In International Journal of Network Security, Vol.23, No.3, PP.436-448, May 2021. Available at https://doi.org/10.6633/IJNS.202105_23(3).08.
  19. Lijun Xiao, Songyou Xie, Dezhi Han, Wei Liang, Jun Guo, and Wen-Kuang Chou. A lightweight authentication scheme for telecare medical information system. In Connection Science, Volume 33, 2021 - Issue 3. Available at https://doi.org/10.1080/09540091.2021.1889976.
  20. Aiman Sultan, Mehmood Hassan, Khwaja Mansoor, and Syed Saddam Ahmed. Securing IoT Enabled RFID Based Object Tracking Systems: A Symmetric Cryptography Based Authentication Protocol for Efficient Smart Object Tracking. In 2021 International Conference on Communication Technologies (ComTech), IEEE. Available at https://doi.org/10.1109/ComTech52583.2021.9616967.
  21. Gayathri Karthick, Glenford Mapp, Florian Kammueller, and Mahdi Aiash. Modeling and verifying a resource allocation algorithm for secure service migration for commercial cloud systems. In Computational Intelligence, Volume 38, Issue 3, Special Issue: AI and Machine Learning for Smart Cities - Part 2. Intelligent Optimization Methods and their Applications - Part 2, June 2022, Pages 811-828. Available at https://doi.org/10.1111/coin.12421.
  22. Zisang Xu, Cheng Xu, Jianbo Xu, and Xiangwei Meng. A computationally efficient authentication and key agreement scheme for multi-server switching in WBAN. In International Journal of Sensor Networks, Vol. 35, No. 3. Available at https://doi.org/10.1504/IJSNET.2021.113839.
  23. Shehzad AshrafChaudhry. Correcting “PALK: Password-based anonymous lightweight key agreement framework for smart grid”. In International Journal of Electrical Power & Energy Systems, Volume 125, February 2021, 106529. Available at https://doi.org/10.1016/j.ijepes.2020.106529.
  24. Tsu-Yang Wu, Lei Yang, Zhiyuan Lee, Chien-Ming Chen, Jeng-Shyang Pan, and SK Hafizul Islam. Improved ECC-Based Three-Factor Multiserver Authentication Scheme. In Security and Communication Networks, Volume 2021, Article ID 6627956. Available at https://doi.org/10.1155/2021/6627956.
  25. Wei Liang, Songyou Xie, Jiahong Cai, Chong Wang, Yujie Hong, and Xiaoyan Kui. Novel private data access control scheme suitable for mobile edge computing. In China Communications, Volume: 18, Issue: 11, November 2021. Available at https://doi.org/10.23919/JCC.2021.11.007.
2022
  1. P. Tedeschi, S. Sciancalepore and R. Di Pietro, "PPCA - Privacy-Preserving Collision Avoidance for Autonomous Unmanned Aerial Vehicles," in IEEE Transactions on Dependable and Secure Computing, doi: 10.1109/TDSC.2022.3159837.
  2. Jianliang Wu, Ruoyu Wu, Dongyan Xu, Dave (Jing) Tian, and Antonio Bianchi. Formal Model-Driven Discovery of Bluetooth Protocol Design Vulnerabilities. In 2022 IEEE Symposium on Security and Privacy, pages 2285-2303. doi: 10.1109/SP46214.2022.00051. Available at https://friends.cs.purdue.edu/pubs/SP22_BT_formal.pdf
  3. P. Tedeschi, S. Bakiras and R. D. Pietro, "SpreadMeNot: A Provably Secure and Privacy-Preserving Contact Tracing Protocol," in IEEE Transactions on Dependable and Secure Computing, 2022, doi: 10.1109/TDSC.2022.3186153. Available at https://www.researchgate.net/publication/361523428_SpreadMeNot_A_Provably_Secure_and_Privacy-Preserving_Contact_Tracing_Protocol.
  4. Vincent Cheval, Charlie Jacomme, Steve Kremer, and Robert Künnemann. SAPIC+: protocol verifiers of the world, unite! In USENIX Security Symposium (USENIX Security), 2022. Available at https://publications.cispa.saarland/3707/.
  5. Jiangyuan Yao, Chunxiang Xu, Deshun Li, Shengjun Lin, and Xingcan Cao. Formal Verification of Security Protocols: ProVerif and Extensions. In International Conference on Artificial Intelligence and Security (ICAIS 2022), pp 500–512. LNCS, volume 13339, Springer. Available at https://doi.org/10.1007/978-3-031-06788-4_42.
  6. Roberto Metere and Luca Arnaboldi. Automating cryptographic protocol language generation from structured specifications. In FormaliSE '22: Proceedings of the IEEE/ACM 10th International Conference on Formal Methods in Software Engineering, May 2022, pages 91–101. Available at https://doi.org/10.1145/3524482.3527654.
  7. Baasansuren Bat-Erdene, Yuping Yan, Mohammed B. M. Kamel, and Peter Ligeti. Security Verification of Key Exchange in Ciphertext-Policy Attribute Based Encryption. In 2022 7th International Conference on Signal and Image Processing (ICSIP). Available at https://doi.org/10.1109/ICSIP55141.2022.9887218.
  8. Shion Maeda, Misato Nakabayashi, and Tetsuya Okuda. Architecture Design and Security Evaluation of Secure Optical Transport Network Using Formal Verification. In 2022 IEEE 46th Annual Computers, Software, and Applications Conference (COMPSAC). Available at https://doi.org/10.1109/COMPSAC54236.2022.00288
  9. Mamoon M. Saeed, Mohammad Kamrul Hasan, Rosilah Hassan, Rania Mokhtar, Rashid A. Saeed, Elsadig Saeid, and Manoj Gupta. Preserving Privacy of User Identity Based on Pseudonym Variable in 5G. In Computers, Materials & Continua, 2022, 70(3), 5551-5568. Available at https://doi.org/10.32604/cmc.2022.017338.
  10. Munayfah Alanazi and Shadi Nashwan. Secure and Anonymous Three-Factor Authentication Scheme for Remote Healthcare Systems. In Computer Systems Science and Engineering 2022, 42(2), 703-725. Available at https://doi.org/10.32604/csse.2022.022962.
  11. Munefah Alshammari and Shadi Nashwan. Fully Authentication Services Scheme for NFC Mobile Payment Systems. In Intelligent Automation & Soft Computing 2022, 32(1), 401-428. Available at https://doi.org/10.32604/iasc.2022.022065.
  12. Marwah Yaseen, Mohammed B. M. Kamel, and Peter Ligeti. Security Analysis and Deployment Measurement of Transport Layer Security Protocol. In: Singh, P.K., Singh, Y., Chhabra, J.K., Illés, Z., Verma, C. (eds) Recent Innovations in Computing. Lecture Notes in Electrical Engineering, vol 855. Springer, Singapore. Available at https://doi.org/10.1007/978-981-16-8892-8_55.
  13. Mahin Mohammadi, Reza Rawassizadeh, Abbas Sheikhtaheri. A consumer-centered security framework for sharing health data in social networks. In Journal of Information Security and Applications, Volume 69, September 2022, 103303. Available at https://doi.org/10.1016/j.jisa.2022.103303.
  14. Mahdieh Ebrahimi, Majid Bayat, Behnam Zahednejad. A Privacy Preserving Mutual Authentication Scheme Suitable for IoT-Based Medical Systems. In The ISC International Journal of Information Security, Volume 14, Issue 1, January 2022, , Pages 57-68. Available at https://www.isecure-journal.com/article_135754.html.

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