A formal TLS handshake model in LNT

Josip Bozic, Lina Marsso, Radu Mateescu, Franz Wotawa

Research output: Contribution to journalConference articleResearchpeer-review

Abstract

Testing of network services represents one of the biggest challenges in cyber security. Because new vulnerabilities are detected on a regular basis, more research is needed. These faults have their roots in the software development cycle or because of intrinsic leaks in the system specification. Conformance testing checks whether a system behaves according to its specification. Here model-based testing provides several methods for automated detection of shortcomings. The formal specification of a system behavior represents the starting point of the testing process. In this paper, a widely used cryptographic protocol is specified and tested for conformance with a test execution framework. The first empirical results are presented and discussed.

Original languageEnglish
Pages (from-to)1-40
Number of pages40
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume268
DOIs
Publication statusPublished - 23 Mar 2018
Event3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018 - Thessaloniki, Greece
Duration: 20 Apr 2018 → …

Fingerprint

Testing
Specifications
Software engineering
Network protocols
Formal specification

ASJC Scopus subject areas

  • Software

Cite this

A formal TLS handshake model in LNT. / Bozic, Josip; Marsso, Lina; Mateescu, Radu; Wotawa, Franz.

In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 268, 23.03.2018, p. 1-40.

Research output: Contribution to journalConference articleResearchpeer-review

@article{46ed6c3fffdc4486887006f69453afe8,
title = "A formal TLS handshake model in LNT",
abstract = "Testing of network services represents one of the biggest challenges in cyber security. Because new vulnerabilities are detected on a regular basis, more research is needed. These faults have their roots in the software development cycle or because of intrinsic leaks in the system specification. Conformance testing checks whether a system behaves according to its specification. Here model-based testing provides several methods for automated detection of shortcomings. The formal specification of a system behavior represents the starting point of the testing process. In this paper, a widely used cryptographic protocol is specified and tested for conformance with a test execution framework. The first empirical results are presented and discussed.",
author = "Josip Bozic and Lina Marsso and Radu Mateescu and Franz Wotawa",
year = "2018",
month = "3",
day = "23",
doi = "10.4204/EPTCS.268.1",
language = "English",
volume = "268",
pages = "1--40",
journal = "Electronic Proceedings in Theoretical Computer Science",
issn = "2075-2180",
publisher = "National ICT Australia Ltd",

}

TY - JOUR

T1 - A formal TLS handshake model in LNT

AU - Bozic, Josip

AU - Marsso, Lina

AU - Mateescu, Radu

AU - Wotawa, Franz

PY - 2018/3/23

Y1 - 2018/3/23

N2 - Testing of network services represents one of the biggest challenges in cyber security. Because new vulnerabilities are detected on a regular basis, more research is needed. These faults have their roots in the software development cycle or because of intrinsic leaks in the system specification. Conformance testing checks whether a system behaves according to its specification. Here model-based testing provides several methods for automated detection of shortcomings. The formal specification of a system behavior represents the starting point of the testing process. In this paper, a widely used cryptographic protocol is specified and tested for conformance with a test execution framework. The first empirical results are presented and discussed.

AB - Testing of network services represents one of the biggest challenges in cyber security. Because new vulnerabilities are detected on a regular basis, more research is needed. These faults have their roots in the software development cycle or because of intrinsic leaks in the system specification. Conformance testing checks whether a system behaves according to its specification. Here model-based testing provides several methods for automated detection of shortcomings. The formal specification of a system behavior represents the starting point of the testing process. In this paper, a widely used cryptographic protocol is specified and tested for conformance with a test execution framework. The first empirical results are presented and discussed.

UR - http://www.scopus.com/inward/record.url?scp=85048371971&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.268.1

DO - 10.4204/EPTCS.268.1

M3 - Conference article

VL - 268

SP - 1

EP - 40

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

ER -