Revision c8d3843b62b5381cb55b5ba8f7650f97a834ee61 (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