AIセキュリティポータル K Program
A Security Verification Framework of Cryptographic Protocols Using Machine Learning
Share
Abstract
We propose a security verification framework for cryptographic protocols using machine learning. In recent years, as cryptographic protocols have become more complex, research on automatic verification techniques has been focused on. The main technique is formal verification. However, the formal verification has two problems: it requires a large amount of computational time and does not guarantee decidability. We propose a method that allows security verification with computational time on the order of linear with respect to the size of the protocol using machine learning. In training machine learning models for security verification of cryptographic protocols, a sufficient amount of data, i.e., a set of protocol data with security labels, is difficult to collect from academic papers and other sources. To overcome this issue, we propose a way to create arbitrarily large datasets by automatically generating random protocols and assigning security labels to them using formal verification tools. Furthermore, to exploit structural features of protocols, we construct a neural network that processes a protocol along its series and tree structures. We evaluate the proposed method by applying it to verification of practical cryptographic protocols.
Deciding knowledge in security protocols under equational theories
Martín Abadi, Véronique Cortier
Published: 2006
On the symbolic reduction of processes with cryptographic functions
Roberto M Amadio, Denis Lugiez, Vincent Vanackere
Published: 2003
A formal analysis of 5g authentication
David Basin, Jannik Dreier, Lucca Hirschi, Saša Radomirovic, Ralf Sasse, Vincent Stettler
Published: 2018
Verified models and reference implementations for the tls 1.3 standard candidate
K. Bhargavan, B. Blanchet, N. Kobeissi
Published: 2017
A symbolic analysis of privacy for tls 1.3 with encrypted client hello
Karthikeyan Bhargavan, Vincent Cheval, Christopher Wood
Published: 2022
Automatic verification of security protocols in the symbolic model: The verifier proverif
Bruno Blanchet
Published: 2013
Composition theorems for cryptoverif and application to tls 1.3
Bruno Blanchet
Published: 2018
Proverif 2.04: Automatic cryptographic protocol verifier, user manual and tutorial
Bruno Blanchet, Ben Smyth, Vincent Cheval, Marc Sylvestre
Published: 2021
Protocols for authentication and key establishment Second Edition
Colin Boyd, Anish Mathuria, Douglas Stebila
Published: 2019
Language models are few-shot learners
T. B. Brown, B. Mann, N. Ryder, M. Subbiah, J. Kaplan, P. Dhariwal, A. Neelakantan, P. Shyam, G. Sastry, A. Askell, S. Agarwal, A. Herbert-Voss, G. Krueger, T. Henighan, R. Child, A. Ramesh, D. M. Ziegler, J. Wu, C. Winter, C. Hesse, M. Chen, E. Sigler, M. Litwin, S. Gray, B. Chess, J. Clark, C. Berner, S. McCandlish, A. Radford, I. Sutskever, D. Amodei
Published: 2020
Deepsec: Deciding equivalence properties in security protocols theory and practice
Vincent Cheval, Steve Kremer, Itsaka Rakotonirina
Published: 2018
Decidability of trace equivalence for protocols with nonces
Rémy Chrétien, Véronique Cortier, Stéphanie Delaune
Published: 2015
Computing knowledge in security protocols under convergent equational theories
¸Stefan Ciobâca, Stéphanie Delaune, Steve Kremer
Published: 2009
Computing knowledge in security protocols under convergent equational theories
¸Stefan Ciobâca, Stéphanie Delaune, Steve Kremer
Published: 2012
Tree automata with one memory set constraints and cryptographic protocols
Hubert Comon, Véronique Cortier
Published: 2005
Efficient decision procedures for message deducibility and static equivalence
Bruno Conchinha, David Basin, Carlos Caleiro
Published: 2010
The scyther tool: Verification, falsification, and analysis of security protocols
Cas Cremers
Published: 2008
Component-based formal analysis of 5g-aka: Channel assumptions and session confusion
Cas Cremers, Martin Dehnel-Wild
Published: 2019
Component-based formal analysis of 5g-aka: Channel assumptions and session confusion
Cas Cremers, Martin Dehnel-Wild
Published: 2019
A comprehensive symbolic analysis of tls 1.3
Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, Thyla van der Merwe
Published: 2017
Automated analysis and verification of tls 1.3: 0-rtt, resumption and delayed authentication
Cas Cremers, Marko Horvat, Sam Scott, Thyla van der Merwe
Published: 2016
Implementing and proving the tls 1.3 record layer
Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Karthikeyan Bhargavan, Jianyang Pan, Jean Karim Zinzindohoue
Published: 2017
A security model and fully verified implementation for the ietf quic record layer
Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou
Published: 2021
On the security of public key protocols
Danny Dolev, Andrew Yao
Published: 1983
Multiset rewriting and the complexity of bounded security protocols
Nancy Durgin, Patrick Lincoln, John Mitchell, Andre Scedrov
Published: 2004
Deep residual learning for image recognition
Kaiming He, Xiangyu Zhang, Shaoqing Ren, Jian Sun
Published: 2016
Denoising diffusion probabilistic models
Jonathan Ho, Ajay Jain, Pieter Abbeel
Published: 2020
Long Short-Term Memory
Sepp Hochreiter, Jürgen Schmidhuber
Published: 1997
Verifpal: Cryptographic protocol analysis for the real world
Nadim Kobeissi, Georgio Nicolas, Mukesh Tiwari
Published: 2020
Improving techniques for proving undecidability of checking cryptographic protocols
Zhiyao Liang, Rakesh M Verma
Published: 2008
A machine learning-based scheme for the security analysis of authentication and key agreement protocols
Zhuo Ma, Yang Liu, Zhuzhu Wang, Haoran Ge, Meng Zhao
Published: 2020
The tamarin prover for the symbolic analysis of security protocols
Simon Meier, Benedikt Schmidt, Cas Cremers, David Basin
Published: 2013
Protocol insecurity with a finite number of sessions and composed keys is np-complete
Michaël Rusinowitch, Mathieu Turuani
Published: 2003
Iso: Information technology - security techniques - key management - part 3: Mechanisms using asymmetric techniques iso/iec 11770-3
International Standard
Published: 2015
Improved semantic representations from tree-structured long short-term memory networks
Kai Sheng Tai, Richard Socher, Christopher D. Manning
Published: 2015
Decidability and complexity results for security protocols
Ferucio Laurentiu Tiplea, Constantin Enea, Catalin V Bîrjoveanu
Published: 2005
Formal analysis of v2x revocation protocols
Jorden Whitefield, Liqun Chen, Frank Kargl, Andrew Paverd, Steve Schneider, Helen Treharne, Stephan Wesemeyer
Published: 2017
A novel machine learning-based approach for security analysis of authentication and key agreement protocols
Behnam Zahednejad, Lishan Ke, Jing Li
Published: 2020
Formal verification of 5g-eap-tls authentication protocol
Jingjing Zhang, Qiang Wang, Lin Yang, Tao Feng
Published: 2019
Formal analysis of 5g eap-tls authentication protocol using proverif
Jingjing Zhang, Lin Yang, Weipeng Cao, Qiang Wang
Published: 2020
Formal analysis of quic handshake protocol using proverif
Jingjing Zhang, Lin Yang, Xianming Gao, Gaigai Tang, Jiyong Zhang, Qiang Wang
Published: 2020
Share