Formal Specification of Cryptographic Security Protocols (암호화 보안 프로토콜의 정형명세)

Lee Gye-Sik (이계식)

doi:10.34163/jkits.2019.14.6.014

Formal Specification of Cryptographic Security Protocols

Journal of Knowledge Information Technology and Systems
Abbr : JKITS
2019, 14(6), pp.711-718
DOI : 10.34163/jkits.2019.14.6.014
Publisher : Korea Knowledge Information Technology Society
Research Area : Interdisciplinary Studies > Interdisciplinary Research
Received : November 21, 2019
Accepted : December 7, 2019
Published : December 31, 2019

Lee Gye-Sik ¹

¹한경대학교

Accredited

ABSTRACT

We introduce a way of formal specification of cryptographic security protocols. We demonstrate how to use formal methods in verifying cryptographic security protocols. Each step of the verification is explained with a concrete example, the Needham-Schroeder public-key protocol. The style of describing the syntax is similar to that of the tool Scyther. It is simple and intuitive to use for the specification of security protocols. Our description corresponds also to the basic concepts of the tool ProVerif. Specifications of cryptographic security protocols are represented at the most abstract level: Messages are terms constructed from symbols and the attacker is modeled as a formal process. A formal language L = (V, C, R, F) for public-key protocols consists of a set V of variables for received messages, a set C of local constant symbols, a set R of role name symbols, and a set F of function symbols. Then a protocol describes the behavior of each of the roles such as initiator, responder, key server, etc. In the specification, the behavior of each role is formalized as a transition system describing how to create messages, how to react to the received messages, and how to manipulate messages. Among many security properties, we illustrate how to formally handle secrecy and authentication.

KEYWORDS

Cryptographic security protocols, Formal specifications, Automatic verification, Formal methods, Scyther, ProVerif

Citation status

* References for papers published after 2023 are currently being built.

[confproc] C. Cremers / 2008 / The Scyther tool: verification, falsification, and analysis of security protocols / Conference on Computer-Aided Verification (CAV)

[book] C. Cremers / 2012 / Information Security and Cryptography / Springer : 1~155

[journal] B. T. Nguyen / 2018 / Abstraction for security protocol verification / Journal of Computer Security 26(4) : 459~508

[journal] B. Blanchet / 2009 / Automatic verification of correspondences for security protocols / Journal of Computer Security 17(4) : 363~434

[other] B. Blanchet / 2013 / Automatic verification of security protocols in the symbolic model: the verifier ProVerif / Foundations of Security Analysis and Design (FOSAD) : 54~87

[confproc] N. Kobeissi / 2017 / Automatic verification for secure messaging protocols and their implementations: a symbolic and computational approach / EuroS&P 2017 : 435~450

[confproc] H. Oguma / 2008 / New attestation based security architecture for in-vehicle communication / GLOBECOM : 1909~1914

[confproc] G. Lee / 2009 / Formally verifiable features in embedded vehicular security systems / IEEE Vehicular Networking Conference (VNC) : 1~7

[confproc] T. Ohki / 2017 / Theoretical vulnerabilities in map speaker adaptation / ICASSP : 2042~2046

[journal] S. Delaune / 2008 / Symbolic protocol analysis for monoidal equational theories / Information and Computation 206(2-4) : 312~351

[confproc] R. Küsters / 2008 / Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach / ACM Conference on Computer and Communications Security : 129~138

[journal] G. Lowe / 1995 / An attack on the Needham-Schroeder public key authentication protocol / Information Processing Letters 56(3) : 131~136

[confproc] G. Lowe / 1997 / A hierarchy of authentication specifications / IEEE Computer Security Foundations Workshop : 31~44

[journal] P. J. Hopcroft / 2004 / Analysing a stream authentication protocol using model checking / International Journal of Information Security 3(1) : 2~13

[journal] M. Avalle, A / 2014 / Formal verification of security protocol implementations: a survey / Formal Aspects of Computing 26(1) : 99~123

This paper was written with support from the National Research Foundation of Korea.

KJCKorea
Journal Central

Journal of Knowledge Information Technology and Systems 2023 KCI Impact Factor : 0.89

Formal Specification of Cryptographic Security Protocols

ABSTRACT

KEYWORDS

Citation status

* References for papers published after 2023 are currently being built.

Journal of Knowledge Information Technology and Systems 2023 KCI Impact Factor : 0.89

Formal Specification of Cryptographic Security Protocols

ABSTRACT

KEYWORDS

Statistics

Tools

Issue List

Citation status

KCI Citation Counts (1)

REFERENCES (15) * References for papers published after 2023 are currently being built.

Search PDF

Citation

* References for papers published after 2023 are currently being built.