Revision a875eac38e1131221330c4ab8025e18101496969 (click the page title to view the current version)

TLS Handshake Model

This example demonstrates modeling TLS Handshake Protocol.

Feature modeling

abstract final Feature
abstract final FeatureModel
TLSFeatures : FeatureModel
annonymousMode : Feature ?
clientAuthentication : Feature ?
abstract final Domain
enum ProtocolVersion = SSL2_0 | SSL3_0 | TLS1_0 | TLS1_1 | TLS1_2
enum HandshakeStatus = initiated | completed | failed
abstract Port
abstract final Message

Server side messages

serverHelloRequestMessage : Message
serverHelloMessage : Message
serverCertificateMessage : Message
serverKeyExchangeMessage : Message
serverCertificateRequestMessage : Message
serverHelloDoneMessage : Message
serverChangeCipherSpecMessage : Message
serverFinishedMessage : Message
protocolMismatch : Message

Client side messages

clientHelloMessage : Message
clientCertificateMessage : Message
clientKeyExchangeMessage : Message
certificateVerifyMessage : Message
clientChangeCipherSpecMessage : Message
clientFinishedMessage : Message

Application data

applicationDataMessage : Message

Nodes

abstract final Node : Domain
send : Port -> Message
receive : Port -> Message
protocolversion -> ProtocolVersion +
certificate ?
signing ?
abstract final Server : Node
abstract final Client : Node

connecting messages

Concrete client and server

OurServer : Server
[ protocolversion = SSL2_0, SSL3_0, TLS1_2 ]

The main protocol

Protocol : Domain
final client -> aClient
final server -> OurServer
handshakeStatus -> HandshakeStatus
xor channel
initial clientHello --> serverResponse
[ handshakeStatus = initiated ]
[ client.send = clientHelloMessage ]
xor serverResponse
[ handshakeStatus = initiated ]
[ initially serverHello || mismatch ]
mismatch --> fatalError
[ client.protocolversion.dref not in server.protocolversion.dref ]
[ server.send = protocolMismatch ]
serverHello --> serverCertificate || serverKeyExchange || certificateRequest || serverHelloDone
[ client.protocolversion.dref in server.protocolversion.dref ]
[ server.send = serverHelloMessage ]
[ serverHello -[not annonymousMode]--> serverCertificate ]
serverCertificate --> serverKeyExchange || certificateRequest || serverHelloDone
[ server.send = serverCertificateMessage ]
serverKeyExchange --> certificateRequest || serverHelloDone
[ server.send = serverKeyExchangeMessage ]
certificateRequest --> serverHelloDone
[ no annonymousMode && clientAuthentication ]
[ server.send = serverCertificateRequestMessage ]
serverHelloDone --> clientResponse
[ server.send = serverHelloDoneMessage ]
xor clientResponse
[ handshakeStatus = initiated ]
[ initially clientCertificate || clientKeyExchange ]
clientCertificate --> clientKeyExchange
[ no annonymousMode && clientAuthentication ]
[ client.send = clientCertificateMessage ]
clientKeyExchange --> certificateVerify || clientChangeCipherSpec
[ client.send = clientKeyExchangeMessage ]
certificateVerify --> clientChangeCipherSpec
[ client.certificate.signing ]
[ client.send = certificateVerifyMessage ]
clientChangeCipherSpec --> clientFinished
[ client.send = clientChangeCipherSpecMessage ]
clientFinished --> serverFinish
[ client.send = clientFinishedMessage ]
xor serverFinish --> serverFinished
[ handshakeStatus = initiated ]
initial serverChangeCipherSpec
[ server.send = serverChangeCipherSpecMessage ]
serverFinished --> dataTransfer
[ server.send = serverFinishedMessage ]
[ handshakeStatus = completed ]
dataTransfer -->> handshakeStatus = initiated
[ handshakeStatus = completed ]
[ client.send = applicationDataMessage ]
fatalError
[ handshakeStatus = failed ]