---
title: TLS Handshake Model
categories: behavioral
...

This example demonstrates modeling TLS Handshake Protocol.

```{.clafer .links}
```

# Feature modeling

```clafer
abstract final Feature
abstract final FeatureModel

TLSFeatures : FeatureModel
    annonymousMode : Feature ?
    clientAuthentication : Feature ?
```

```clafer
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

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

## Client side messages

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

## Application data
```clafer
applicationDataMessage : Message
```

## Nodes

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


abstract final Server : Node

abstract final Client : Node
```

##  connecting messages 

```clafer
[Server.send = Client.receive]
[Server.receive = Client.send]
```

## Concrete client and server

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

aClient : Client
    [ certificate ]
    [ protocolversion = TLS1_2 ]
```

## The main protocol

```clafer
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]
```