From 1eaf8f73c314e2cacd24271e6fdcd7d7a7f006a0 Mon Sep 17 00:00:00 2001 From: Kenny Root Date: Wed, 22 Jul 2026 21:06:12 -0700 Subject: [PATCH 1/4] test(sftp): add rekey during SFTP tests --- .../client/sftp/SftpClientIntegrationTest.kt | 60 ++++++++++++++++++- 1 file changed, 58 insertions(+), 2 deletions(-) diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/sftp/SftpClientIntegrationTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/sftp/SftpClientIntegrationTest.kt index b6037997..5ea18fa0 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/sftp/SftpClientIntegrationTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/sftp/SftpClientIntegrationTest.kt @@ -1,6 +1,6 @@ /* * ConnectBot SSH Library - * Copyright 2025 Kenny Root + * Copyright 2025-2026 Kenny Root * * Licensed under the Apache License, Version 2.0 (the "License"); * you may not use this file except in compliance with the License. @@ -17,7 +17,9 @@ package org.connectbot.sshlib.client.sftp +import kotlinx.coroutines.delay import kotlinx.coroutines.runBlocking +import kotlinx.coroutines.withTimeout import org.connectbot.sshlib.HostKeyVerifier import org.connectbot.sshlib.PublicKey import org.connectbot.sshlib.SftpClient @@ -78,7 +80,10 @@ class SftpClientIntegrationTest { override suspend fun verify(key: PublicKey): Boolean = true } - private suspend fun openSftp(): Pair { + private suspend fun openSftp( + rekeyIntervalMs: Long = 3_600_000L, + rekeyBytesLimit: Long = 1_073_741_824L, + ): Pair { val host = opensshContainer.host val port = opensshContainer.getMappedPort(22) @@ -86,6 +91,8 @@ class SftpClientIntegrationTest { this.host = host this.port = port this.hostKeyVerifier = acceptAllVerifier + this.rekeyIntervalMs = rekeyIntervalMs + this.rekeyBytesLimit = rekeyBytesLimit } val client = SshClient(config) @@ -296,6 +303,55 @@ class SftpClientIntegrationTest { } } + @Test + fun `SFTP write continues across byte limit rekey`() = runBlocking { + val (client, sftp) = openSftp( + rekeyIntervalMs = Long.MAX_VALUE, + rekeyBytesLimit = 256L * 1024, + ) + val remoteDirectory = sftp.realpath(".").getOrThrow().trimEnd('/') + val testPath = "$remoteDirectory/sftp-rekey-write-${System.currentTimeMillis()}.bin" + try { + withTimeout(30_000) { + val handle = sftp.open( + testPath, + setOf(SftpOpenFlag.WRITE, SftpOpenFlag.CREATE, SftpOpenFlag.TRUNCATE), + ).getOrThrow() + val chunk = ByteArray(32 * 1024) { (it % 251).toByte() } + repeat(64) { index -> + sftp.write(handle, index.toLong() * chunk.size, chunk).getOrThrow() + } + sftp.close(handle).getOrThrow() + + val attrs = sftp.stat(testPath).getOrThrow() + assertEquals(2L * 1024 * 1024, attrs.size, "All data should be written across rekey") + } + } finally { + sftp.remove(testPath) + sftp.close() + client.disconnect() + } + } + + @Test + fun `SFTP operation completes after interval rekey while idle`() = runBlocking { + val (client, sftp) = openSftp( + rekeyIntervalMs = 1_000L, + rekeyBytesLimit = Long.MAX_VALUE, + ) + try { + val remoteDirectory = sftp.realpath(".").getOrThrow() + delay(2_500L) + withTimeout(10_000L) { + val handle = sftp.opendir(remoteDirectory).getOrThrow() + sftp.close(handle).getOrThrow() + } + } finally { + sftp.close() + client.disconnect() + } + } + @Test fun `should set file attributes`() = runBlocking { val (client, sftp) = openSftp() From 8a606f7301777bcbaa837eeceec71b8e60bc4a7d Mon Sep 17 00:00:00 2001 From: Kenny Root Date: Wed, 22 Jul 2026 21:06:17 -0700 Subject: [PATCH 2/4] chore(tla+): prove Terrapin is mitigated Move packet ignore out of implicit guards to the state machine to explicitly part of the model. Then add a focused test to make sure that Terrapin is mitigated in strict kex and a test to make sure that Terrapin seven-step attack is modeled correctly in non-strict. --- sshlib/build.gradle.kts | 73 ++++- .../connectbot/sshlib/client/SshConnection.kt | 49 +-- .../sshlib/protocol/SshClientStateMachine.kt | 168 +++++++++-- .../protocol/SshStateMachineFormalModel.kt | 99 ++++++- .../SshConnectionPacketClassificationTest.kt | 41 +++ .../protocol/SshClientStateMachineTest.kt | 104 ++++++- .../protocol/SshStateMachineTlaGenerator.kt | 102 +++++++ .../resources/tla/SshClientStateMachine.cfg | 5 + .../resources/tla/SshClientStateMachine.tla | 40 ++- .../tla/SshClientStateMachineGenerated.tla | 280 +++++++++++++++++- sshlib/src/test/resources/tla/SshTerrapin.tla | 218 ++++++++++++++ .../resources/tla/SshTerrapinNonStrict.cfg | 8 + .../test/resources/tla/SshTerrapinStrict.cfg | 9 + 13 files changed, 1132 insertions(+), 64 deletions(-) create mode 100644 sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionPacketClassificationTest.kt create mode 100644 sshlib/src/test/resources/tla/SshTerrapin.tla create mode 100644 sshlib/src/test/resources/tla/SshTerrapinNonStrict.cfg create mode 100644 sshlib/src/test/resources/tla/SshTerrapinStrict.cfg diff --git a/sshlib/build.gradle.kts b/sshlib/build.gradle.kts index b3dffa06..2ad46101 100644 --- a/sshlib/build.gradle.kts +++ b/sshlib/build.gradle.kts @@ -16,6 +16,7 @@ import com.vanniktech.maven.publish.DeploymentValidation import org.jetbrains.kotlin.gradle.dsl.JvmTarget +import java.io.ByteArrayOutputStream plugins { alias(libs.plugins.kotlin.jvm) @@ -139,6 +140,76 @@ tasks.register("checkSftpStateMachineTla") { } } +val checkSshTerrapinStrictTla = tasks.register("checkSshTerrapinStrictTla") { + group = "verification" + description = "Proves that strict KEX prevents the modeled Terrapin prefix truncation attack" + mainClass.set("tlc2.TLC") + workingDir(tlaModelDirectory) + args( + "-workers", + "1", + "-metadir", + tlaStateDirectory.get().dir("terrapin-strict").asFile.absolutePath, + "-config", + "SshTerrapinStrict.cfg", + "SshTerrapin.tla", + ) + jvmArgs("-XX:+UseParallelGC") + doFirst { + val jarPath = tla2toolsJar.orNull + ?: throw GradleException( + "Set -Ptla2toolsJar=/path/to/tla2tools.jar or TLA2TOOLS_JAR to run TLC", + ) + classpath = files(jarPath) + } +} + +val terrapinCounterexampleOutput = ByteArrayOutputStream() +val checkSshTerrapinNonStrictTla = tasks.register("checkSshTerrapinNonStrictTla") { + group = "verification" + description = "Requires TLC to find the modeled Terrapin counterexample without failing the build" + mainClass.set("tlc2.TLC") + workingDir(tlaModelDirectory) + args( + "-workers", + "1", + "-metadir", + tlaStateDirectory.get().dir("terrapin-non-strict").asFile.absolutePath, + "-config", + "SshTerrapinNonStrict.cfg", + "SshTerrapin.tla", + ) + jvmArgs("-XX:+UseParallelGC") + standardOutput = terrapinCounterexampleOutput + errorOutput = terrapinCounterexampleOutput + isIgnoreExitValue = true + doFirst { + terrapinCounterexampleOutput.reset() + val jarPath = tla2toolsJar.orNull + ?: throw GradleException( + "Set -Ptla2toolsJar=/path/to/tla2tools.jar or TLA2TOOLS_JAR to run TLC", + ) + classpath = files(jarPath) + } + doLast { + val output = terrapinCounterexampleOutput.toString(Charsets.UTF_8) + logger.lifecycle(output) + val exitValue = executionResult.get().exitValue + if (exitValue == 0 || "Invariant NoTerrapin is violated" !in output) { + throw GradleException( + "Expected TLC to find the non-strict Terrapin counterexample; exit=$exitValue", + ) + } + logger.lifecycle("Expected non-strict Terrapin counterexample found; treating it as success.") + } +} + +tasks.register("checkSshTerrapinTla") { + group = "verification" + description = "Checks strict Terrapin resistance and the expected non-strict counterexample" + dependsOn(checkSshTerrapinStrictTla, checkSshTerrapinNonStrictTla) +} + tasks.register("generateTla") { group = "verification" description = "Regenerates all TLA+ formal models (SSH and SFTP)" @@ -148,7 +219,7 @@ tasks.register("generateTla") { tasks.register("checkTla") { group = "verification" description = "Checks all TLA+ formal models (SSH and SFTP) with TLC" - dependsOn("checkSshStateMachineTla", "checkSftpStateMachineTla") + dependsOn("checkSshStateMachineTla", "checkSftpStateMachineTla", "checkSshTerrapinTla") } java { diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt index 62ebb4fd..a8aa63c8 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt @@ -156,6 +156,10 @@ internal fun boundRemotePacketSize(packetSize: Long): Int? = when { else -> minOf(packetSize, 32L * 1024L).toInt() } +internal fun isKeyExchangeMessage(messageId: Int): Boolean = messageId == SshEnums.MessageType.SSH_MSG_KEXINIT.id().toInt() || + messageId == SshEnums.MessageType.SSH_MSG_NEWKEYS.id().toInt() || + messageId in 30..49 + private sealed interface PendingProtection { fun installOutbound(packetIO: PacketIO) fun installInbound(packetIO: PacketIO) @@ -296,7 +300,7 @@ class SshConnection( override fun sendVersion() = this@SshConnection.sendVersion() override fun receiveVersion(banner: IdBanner) = this@SshConnection.receiveVersion(banner) override suspend fun sendKexInit() = this@SshConnection.sendKexInit() - override fun receiveKexInit(msg: SshMsgKexinit) = this@SshConnection.receiveKexInit(msg) + override fun receiveKexInit(msg: SshMsgKexinit, initialExchange: Boolean) = this@SshConnection.receiveKexInit(msg, initialExchange) override suspend fun sendKexExchangeInit() = this@SshConnection.sendKexExchangeInit() override suspend fun receiveKexDhReply(msg: SshMsgKexdhReply) = this@SshConnection.receiveKexDhReply(msg) override suspend fun receiveKexEcdhReply(msg: SshMsgKexEcdhReply) = this@SshConnection.receiveKexEcdhReply(msg) @@ -312,8 +316,8 @@ class SshConnection( override fun rekeyStarted() = this@SshConnection.rekeyStarted() override fun rekeyComplete() = this@SshConnection.rekeyComplete() override suspend fun sendKexDhGexInit() = this@SshConnection.sendKexDhGexInit() - override suspend fun sendNewKeys() = this@SshConnection.sendNewKeys() - override fun receiveNewKeys() = this@SshConnection.receiveNewKeys() + override suspend fun sendNewKeys(resetSequenceNumber: Boolean) = this@SshConnection.sendNewKeys(resetSequenceNumber) + override fun receiveNewKeys(resetSequenceNumber: Boolean) = this@SshConnection.receiveNewKeys(resetSequenceNumber) override fun activateEncryption() = this@SshConnection.activateEncryption() override suspend fun sendClientExtInfo() = this@SshConnection.sendClientExtInfo() override suspend fun sendServiceRequest(service: String) = this@SshConnection.sendServiceRequest(service) @@ -366,7 +370,6 @@ class SshConnection( private var negotiatedMacS2C: String? = null private var negotiatedCompressionC2S: String? = null private var negotiatedCompressionS2C: String? = null - private var strictKexEnabled: Boolean = false private var serverAdvertisesExtInfo: Boolean = false private var serverExtInfoReceivedCount: Int = 0 private var clientExtInfoSent: Boolean = false @@ -1216,7 +1219,7 @@ class SshConnection( writePacket(SshEnums.MessageType.SSH_MSG_KEXINIT.id().toInt(), kexInitPayload) } - private fun receiveKexInit(msg: SshMsgKexinit) { + private fun receiveKexInit(msg: SshMsgKexinit, initialExchange: Boolean): Boolean { logger.info("Received KEX_INIT from server") val serverKexAlgs = msg.kexAlgorithms().entries().data() @@ -1237,17 +1240,17 @@ class SshConnection( logger.debug(" Server compression c->s: $serverCompC2S") logger.debug(" Server compression s->c: $serverCompS2C") - val localKexAlgorithms = if (isRekeying) kexAlgorithms else initialKexAlgorithms + val localKexAlgorithms = if (initialExchange) initialKexAlgorithms else kexAlgorithms val clientKexList = parseNameList(localKexAlgorithms) val serverKexList = serverKexAlgs.filter { it.isNotEmpty() } val clientKexStrict = "kex-strict-c-v00@openssh.com" in clientKexList val serverKexStrict = "kex-strict-s-v00@openssh.com" in serverKexList - strictKexEnabled = clientKexStrict && serverKexStrict - if (strictKexEnabled) { + val strictKexNegotiated = clientKexStrict && serverKexStrict + if (strictKexNegotiated) { logger.info(" Strict KEX enabled") } - if (!isRekeying) { + if (initialExchange) { serverAdvertisesExtInfo = "ext-info-s" in serverKexList if (serverAdvertisesExtInfo) { logger.info(" Server advertises EXT_INFO support") @@ -1298,8 +1301,11 @@ class SshConnection( ?: throw SshException("No matching compression algorithm (c->s). Client: $compressionAlgorithms, Server: $serverCompC2S") negotiatedCompressionS2C = clientCompList.firstOrNull { it in serverCompS2C } ?: throw SshException("No matching compression algorithm (s->c). Client: $compressionAlgorithms, Server: $serverCompS2C") + logger.info(" Negotiated compression c->s: $negotiatedCompressionC2S") logger.info(" Negotiated compression s->c: $negotiatedCompressionS2C") + + return strictKexNegotiated } private suspend fun sendKexExchangeInit() { @@ -1518,7 +1524,7 @@ class SshConnection( ) } - private suspend fun sendNewKeys() { + private suspend fun sendNewKeys(resetSequenceNumber: Boolean) { logger.info("Sending NEW_KEYS") prepareEncryption() try { @@ -1530,7 +1536,7 @@ class SshConnection( protection.installOutbound(packetIO) packetIO.enableSendCompression(pendingSendCompressor, pendingCompressionImmediate) pendingSendCompressor = null - if (strictKexEnabled) { + if (resetSequenceNumber) { packetIO.resetSendSequenceNumber() } outboundPacketController.completeKex() @@ -1620,14 +1626,14 @@ class SshConnection( } } - private fun receiveNewKeys() { + private fun receiveNewKeys(resetSequenceNumber: Boolean) { logger.info("Received NEW_KEYS from server") val protection = pendingProtection ?: throw SshException("No staged packet protection") protection.installInbound(packetIO) packetIO.enableReceiveCompression(pendingReceiveCompressor, pendingCompressionImmediate) pendingReceiveCompressor = null - if (strictKexEnabled) { + if (resetSequenceNumber) { packetIO.resetReceiveSequenceNumber() } } @@ -2352,6 +2358,13 @@ class SshConnection( logger.debug("Received packet: $msgType") withContext(stateMachineDispatcher) { + if (!isKeyExchangeMessage(msgType.id().toInt())) { + val description = "Non-KEX packet $msgType is forbidden during strict initial key exchange" + if (!stateMachine.authorizeNonKexPacket(description)) { + throw ProtocolViolationException(description, responseSent = true) + } + } + if (isRekeying && stateMachine.isKexInProgress() && msgType.id().toInt() >= SSH_MSG_USERAUTH_REQUEST_ID) { if (packetsReceivedDuringRekey.size >= MAX_REKEY_IN_FLIGHT_PACKETS) { throw ProtocolViolationException("Too many higher-layer packets received during key exchange") @@ -2374,6 +2387,10 @@ class SshConnection( requireAccepted(stateMachine.requestRekey(), msgType) } requireAccepted(stateMachine.receiveKexInit(kexInit), msgType) + if (stateMachine.isDisconnected()) { + val description = "SSH_MSG_KEXINIT was not the first packet during strict initial key exchange" + throw ProtocolViolationException(description, responseSent = true) + } } SshEnums.MessageType.SSH_MSG_NEWKEYS -> { @@ -2386,16 +2403,10 @@ class SshConnection( } SshEnums.MessageType.SSH_MSG_IGNORE -> { - if (strictKexEnabled && stateMachine.isKexInProgress()) { - throw ProtocolViolationException("SSH_MSG_IGNORE is forbidden during strict key exchange") - } requireAccepted(stateMachine.receiveIgnore(), msgType) } SshEnums.MessageType.SSH_MSG_DEBUG -> { - if (strictKexEnabled && stateMachine.isKexInProgress()) { - throw ProtocolViolationException("SSH_MSG_DEBUG is forbidden during strict key exchange") - } requireAccepted(stateMachine.receiveDebug(packet.body() as SshMsgDebug), msgType) } diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachine.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachine.kt index 68af679b..fe7e3241 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachine.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachine.kt @@ -63,11 +63,17 @@ internal class SshClientStateMachine( private val parsedPacket = setOf(SshEventOrigin.PARSED_PACKET) private val localCommand = setOf(SshEventOrigin.LOCAL_COMMAND) private val rekeying = SshFormalGuard.Fact(SshBooleanFact.REKEYING) + private val strictKex = SshFormalGuard.Fact(SshBooleanFact.STRICT_KEX_ENABLED) + private val nonKexBeforeInitialKexInit = SshFormalGuard.Fact(SshBooleanFact.NON_KEX_BEFORE_INITIAL_KEX_INIT) + private var strictKexEnabled = false + private var receivedNonKexBeforeInitialKexInit = false private sealed class SshEvent : Event { object Connect : SshEvent() data class ReceiveVersion(val banner: IdBanner) : SshEvent() - data class ReceiveKexInit(val msg: SshMsgKexinit) : SshEvent() + data class ReceiveInitialStrictKexInit(val msg: SshMsgKexinit) : SshEvent() + data class ReceiveInitialNonStrictKexInit(val msg: SshMsgKexinit) : SshEvent() + data class ReceiveRekeyKexInit(val msg: SshMsgKexinit) : SshEvent() sealed class ReceiveKex : SshEvent() { data class DhReply(val msg: SshMsgKexdhReply) : ReceiveKex() data class EcdhReply(val msg: SshMsgKexEcdhReply) : ReceiveKex() @@ -100,6 +106,7 @@ internal class SshClientStateMachine( data class ReceiveGlobalRequest(val msg: SshMsgGlobalRequest) : SshEvent() data class ReceiveDebug(val msg: SshMsgDebug) : SshEvent() object ReceiveIgnore : SshEvent() + data class ReceiveNonKexPacket(val description: String) : SshEvent() object AuthorizeAuthenticationPacket : SshEvent() object AuthorizeAuthenticatedPacket : SshEvent() object AuthorizeConnectionPacket : SshEvent() @@ -300,13 +307,69 @@ internal class SshClientStateMachine( onEntry { callbacks.onStateEnter("WaitKexInit") } onExit { callbacks.onStateExit("WaitKexInit") } - formalTransition( - id = SshTransitionId.RECEIVE_KEX_INIT, + formalTransition( + id = SshTransitionId.RECORD_NON_KEX_BEFORE_INITIAL_KEX_INIT, + guard = !rekeying, + origins = parsedPacket, + effects = setOf(SshEffect.RECORD_NON_KEX_BEFORE_INITIAL_KEX_INIT), + ) { + receivedNonKexBeforeInitialKexInit = true + } + + formalTransition( + id = SshTransitionId.RECEIVE_INITIAL_STRICT_KEX_INIT, + targetState = waitKex, + guard = !rekeying and !nonKexBeforeInitialKexInit, + origins = parsedPacket, + effects = setOf( + SshEffect.RECEIVE_KEX_INIT, + SshEffect.ENABLE_STRICT_KEX, + SshEffect.CLEAR_NON_KEX_BEFORE_INITIAL_KEX_INIT, + SshEffect.SEND_KEX_EXCHANGE_INIT, + ), + ) { + strictKexEnabled = true + receivedNonKexBeforeInitialKexInit = false + callbacks.sendKexExchangeInit() + } + formalTransition( + id = SshTransitionId.REJECT_STRICT_KEX_INIT_NOT_FIRST, + targetState = disconnected, + guard = !rekeying and nonKexBeforeInitialKexInit, + origins = parsedPacket, + effects = setOf( + SshEffect.RECEIVE_KEX_INIT, + SshEffect.ENABLE_STRICT_KEX, + SshEffect.SEND_PROTOCOL_ERROR, + SshEffect.DISCONNECT, + ), + ) { + strictKexEnabled = true + callbacks.sendProtocolError("SSH_MSG_KEXINIT was not the first packet during strict initial key exchange") + } + formalTransition( + id = SshTransitionId.RECEIVE_INITIAL_NON_STRICT_KEX_INIT, targetState = waitKex, + guard = !rekeying, + origins = parsedPacket, + effects = setOf( + SshEffect.RECEIVE_KEX_INIT, + SshEffect.NEGOTIATE_NON_STRICT_KEX, + SshEffect.CLEAR_NON_KEX_BEFORE_INITIAL_KEX_INIT, + SshEffect.SEND_KEX_EXCHANGE_INIT, + ), + ) { + strictKexEnabled = false + receivedNonKexBeforeInitialKexInit = false + callbacks.sendKexExchangeInit() + } + formalTransition( + id = SshTransitionId.RECEIVE_REKEY_KEX_INIT, + targetState = waitKex, + guard = rekeying, origins = parsedPacket, effects = setOf(SshEffect.RECEIVE_KEX_INIT, SshEffect.SEND_KEX_EXCHANGE_INIT), ) { - callbacks.receiveKexInit(it.event.msg) callbacks.sendKexExchangeInit() } } @@ -315,23 +378,41 @@ internal class SshClientStateMachine( onEntry { callbacks.onStateEnter("WaitKex") } onExit { callbacks.onStateExit("WaitKex") } + formalTransition( + id = SshTransitionId.REJECT_NON_KEX_WAIT_KEX, + targetState = disconnected, + guard = strictKex and !rekeying, + origins = parsedPacket, + effects = setOf(SshEffect.SEND_PROTOCOL_ERROR, SshEffect.DISCONNECT), + ) { callbacks.sendProtocolError(it.event.description) } + formalTransition( id = SshTransitionId.RECEIVE_KEX_DH_REPLY, targetState = waitNewKeys, origins = parsedPacket, - effects = setOf(SshEffect.RECEIVE_KEX_DH_REPLY, SshEffect.SEND_NEW_KEYS), + effects = setOf( + SshEffect.RECEIVE_KEX_DH_REPLY, + SshEffect.SEND_NEW_KEYS, + SshEffect.ACTIVATE_OUTBOUND_PROTECTION, + SshEffect.RESET_OUTBOUND_SEQUENCE, + ), ) { callbacks.receiveKexDhReply(it.event.msg) - callbacks.sendNewKeys() + callbacks.sendNewKeys(strictKexEnabled) } formalTransition( id = SshTransitionId.RECEIVE_KEX_ECDH_REPLY, targetState = waitNewKeys, origins = parsedPacket, - effects = setOf(SshEffect.RECEIVE_KEX_ECDH_REPLY, SshEffect.SEND_NEW_KEYS), + effects = setOf( + SshEffect.RECEIVE_KEX_ECDH_REPLY, + SshEffect.SEND_NEW_KEYS, + SshEffect.ACTIVATE_OUTBOUND_PROTECTION, + SshEffect.RESET_OUTBOUND_SEQUENCE, + ), ) { callbacks.receiveKexEcdhReply(it.event.msg) - callbacks.sendNewKeys() + callbacks.sendNewKeys(strictKexEnabled) } formalTransition( id = SshTransitionId.RECEIVE_KEX_DH_GEX_GROUP, @@ -351,14 +432,27 @@ internal class SshClientStateMachine( onEntry { callbacks.onStateEnter("WaitKexDhGexInit") } onExit { callbacks.onStateExit("WaitKexDhGexInit") } + formalTransition( + id = SshTransitionId.REJECT_NON_KEX_WAIT_KEX_DH_GEX_INIT, + targetState = disconnected, + guard = strictKex and !rekeying, + origins = parsedPacket, + effects = setOf(SshEffect.SEND_PROTOCOL_ERROR, SshEffect.DISCONNECT), + ) { callbacks.sendProtocolError(it.event.description) } + formalTransition( id = SshTransitionId.RECEIVE_KEX_DH_GEX_REPLY, targetState = waitNewKeys, origins = parsedPacket, - effects = setOf(SshEffect.RECEIVE_KEX_DH_GEX_REPLY, SshEffect.SEND_NEW_KEYS), + effects = setOf( + SshEffect.RECEIVE_KEX_DH_GEX_REPLY, + SshEffect.SEND_NEW_KEYS, + SshEffect.ACTIVATE_OUTBOUND_PROTECTION, + SshEffect.RESET_OUTBOUND_SEQUENCE, + ), ) { callbacks.receiveKexDhGexReply(it.event.msg) - callbacks.sendNewKeys() + callbacks.sendNewKeys(strictKexEnabled) } formalTransition( id = SshTransitionId.UNEXPECTED_KEX_INIT_WAIT_KEX_DH_GEX_INIT, @@ -372,6 +466,14 @@ internal class SshClientStateMachine( onEntry { callbacks.onStateEnter("WaitNewKeys") } onExit { callbacks.onStateExit("WaitNewKeys") } + formalTransition( + id = SshTransitionId.REJECT_NON_KEX_WAIT_NEW_KEYS, + targetState = disconnected, + guard = strictKex and !rekeying, + origins = parsedPacket, + effects = setOf(SshEffect.SEND_PROTOCOL_ERROR, SshEffect.DISCONNECT), + ) { callbacks.sendProtocolError(it.event.description) } + formalTransition( id = SshTransitionId.RECEIVE_INITIAL_NEW_KEYS, targetState = waitService, @@ -379,12 +481,14 @@ internal class SshClientStateMachine( origins = parsedPacket, effects = setOf( SshEffect.RECEIVE_NEW_KEYS, + SshEffect.ACTIVATE_INBOUND_PROTECTION, + SshEffect.RESET_INBOUND_SEQUENCE, SshEffect.ACTIVATE_ENCRYPTION, SshEffect.SEND_CLIENT_EXT_INFO, SshEffect.SEND_SERVICE_REQUEST, ), ) { - callbacks.receiveNewKeys() + callbacks.receiveNewKeys(strictKexEnabled) callbacks.activateEncryption() callbacks.sendClientExtInfo() callbacks.sendServiceRequest("ssh-userauth") @@ -394,9 +498,15 @@ internal class SshClientStateMachine( targetState = postAuthHistory, guard = rekeying, origins = parsedPacket, - effects = setOf(SshEffect.RECEIVE_NEW_KEYS, SshEffect.ACTIVATE_ENCRYPTION, SshEffect.REKEY_COMPLETE), + effects = setOf( + SshEffect.RECEIVE_NEW_KEYS, + SshEffect.ACTIVATE_INBOUND_PROTECTION, + SshEffect.RESET_INBOUND_SEQUENCE, + SshEffect.ACTIVATE_ENCRYPTION, + SshEffect.REKEY_COMPLETE, + ), ) { - callbacks.receiveNewKeys() + callbacks.receiveNewKeys(strictKexEnabled) callbacks.activateEncryption() callbacks.rekeyComplete() } @@ -468,7 +578,9 @@ internal class SshClientStateMachine( this.targetState = targetState metaInfo = meta if (guard != SshFormalGuard.Always) { - this.guard = { guard.evaluate(callbacks) } + this.guard = { + guard.evaluate(callbacks, strictKexEnabled, receivedNonKexBeforeInitialKexInit) + } } } if (action != null) { @@ -480,7 +592,18 @@ internal class SshClientStateMachine( suspend fun receiveVersion(banner: IdBanner): Boolean = process(SshEvent.ReceiveVersion(banner)) - suspend fun receiveKexInit(msg: SshMsgKexinit): Boolean = process(SshEvent.ReceiveKexInit(msg)) + suspend fun receiveKexInit(msg: SshMsgKexinit): Boolean { + if (!isWaitingForKexInit()) return false + + val initialExchange = !callbacks.isRekeying() + val strictKexNegotiated = callbacks.receiveKexInit(msg, initialExchange) + val event = when { + !initialExchange -> SshEvent.ReceiveRekeyKexInit(msg) + strictKexNegotiated -> SshEvent.ReceiveInitialStrictKexInit(msg) + else -> SshEvent.ReceiveInitialNonStrictKexInit(msg) + } + return process(event) + } suspend fun receiveKexDhReply(msg: SshMsgKexdhReply): Boolean = process(SshEvent.ReceiveKex.DhReply(msg)) @@ -527,6 +650,11 @@ internal class SshClientStateMachine( suspend fun receiveIgnore(): Boolean = process(SshEvent.ReceiveIgnore) + suspend fun authorizeNonKexPacket(description: String): Boolean { + process(SshEvent.ReceiveNonKexPacket(description)) + return !isDisconnected() + } + suspend fun authorizeAuthenticationPacket(): Boolean = process(SshEvent.AuthorizeAuthenticationPacket) suspend fun authorizeAuthenticatedPacket(): Boolean = process(SshEvent.AuthorizeAuthenticatedPacket) @@ -549,6 +677,10 @@ internal class SshClientStateMachine( fun isWaitingForKexInit(): Boolean = stateMachine.activeStates().any { it.name == "WaitKexInit" } + fun isDisconnected(): Boolean = stateMachine.activeStates().any { it.name == "Disconnected" } + + fun isStrictKexEnabled(): Boolean = strictKexEnabled + internal fun formalModel(): SshStateMachineFormalModel = stateMachine.toSshFormalModel() private suspend fun process(event: SshEvent): Boolean = stateMachine.processEvent(event) == ProcessingResult.PROCESSED @@ -558,7 +690,7 @@ internal interface SshClientCallbacks { fun sendVersion() fun receiveVersion(banner: IdBanner) suspend fun sendKexInit() - fun receiveKexInit(msg: SshMsgKexinit) + fun receiveKexInit(msg: SshMsgKexinit, initialExchange: Boolean): Boolean suspend fun sendKexExchangeInit() suspend fun receiveKexDhReply(msg: SshMsgKexdhReply) suspend fun receiveKexEcdhReply(msg: SshMsgKexEcdhReply) @@ -570,8 +702,8 @@ internal interface SshClientCallbacks { fun rekeyStarted() fun rekeyComplete() suspend fun sendKexDhGexInit() - suspend fun sendNewKeys() - fun receiveNewKeys() + suspend fun sendNewKeys(resetSequenceNumber: Boolean) + fun receiveNewKeys(resetSequenceNumber: Boolean) fun activateEncryption() suspend fun sendClientExtInfo() suspend fun sendServiceRequest(service: String) diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshStateMachineFormalModel.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshStateMachineFormalModel.kt index 504a5e0b..1becab45 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshStateMachineFormalModel.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshStateMachineFormalModel.kt @@ -50,7 +50,14 @@ internal enum class SshTransitionId { AUTHORIZE_CONNECTION_PACKET, CONNECT, RECEIVE_VERSION, - RECEIVE_KEX_INIT, + RECORD_NON_KEX_BEFORE_INITIAL_KEX_INIT, + REJECT_NON_KEX_WAIT_KEX, + REJECT_NON_KEX_WAIT_KEX_DH_GEX_INIT, + REJECT_NON_KEX_WAIT_NEW_KEYS, + REJECT_STRICT_KEX_INIT_NOT_FIRST, + RECEIVE_INITIAL_STRICT_KEX_INIT, + RECEIVE_INITIAL_NON_STRICT_KEX_INIT, + RECEIVE_REKEY_KEX_INIT, RECEIVE_KEX_DH_REPLY, RECEIVE_KEX_ECDH_REPLY, RECEIVE_KEX_DH_GEX_GROUP, @@ -76,11 +83,16 @@ internal enum class SshEventOrigin { internal enum class SshEffect { ACTIVATE_ENCRYPTION, + ACTIVATE_INBOUND_PROTECTION, + ACTIVATE_OUTBOUND_PROTECTION, AUTHENTICATION_FAILURE, AUTHENTICATION_SUCCESS, + CLEAR_NON_KEX_BEFORE_INITIAL_KEX_INIT, DEBUG, DISCONNECT, IGNORE, + ENABLE_STRICT_KEX, + NEGOTIATE_NON_STRICT_KEX, RECEIVE_CHANNEL_FAILURE, RECEIVE_CHANNEL_OPEN_CONFIRMATION, RECEIVE_CHANNEL_OPEN_FAILURE, @@ -95,8 +107,11 @@ internal enum class SshEffect { RECEIVE_USERAUTH_BANNER, RECEIVE_USERAUTH_INFO_REQUEST, RECEIVE_VERSION, + RECORD_NON_KEX_BEFORE_INITIAL_KEX_INIT, REKEY_COMPLETE, REKEY_STARTED, + RESET_INBOUND_SEQUENCE, + RESET_OUTBOUND_SEQUENCE, SEND_CHANNEL_OPEN, SEND_CHANNEL_REQUEST, SEND_CLIENT_EXT_INFO, @@ -115,22 +130,38 @@ internal enum class SshBooleanFact( val tlaName: String, ) { AUTH_REQUEST_PENDING("authRequestPending"), + NON_KEX_BEFORE_INITIAL_KEX_INIT("nonKexBeforeInitialKexInit"), REKEYING("rekeying"), + STRICT_KEX_ENABLED("strictKex"), ; - fun evaluate(callbacks: SshClientCallbacks): Boolean = when (this) { + fun evaluate( + callbacks: SshClientCallbacks, + strictKexEnabled: Boolean, + nonKexBeforeInitialKexInit: Boolean, + ): Boolean = when (this) { AUTH_REQUEST_PENDING -> callbacks.isAuthenticationRequestPending() + NON_KEX_BEFORE_INITIAL_KEX_INIT -> nonKexBeforeInitialKexInit REKEYING -> callbacks.isRekeying() + STRICT_KEX_ENABLED -> strictKexEnabled } } internal sealed interface SshFormalGuard { - fun evaluate(callbacks: SshClientCallbacks): Boolean + fun evaluate( + callbacks: SshClientCallbacks, + strictKexEnabled: Boolean, + nonKexBeforeInitialKexInit: Boolean, + ): Boolean fun renderTla(): String data object Always : SshFormalGuard { - override fun evaluate(callbacks: SshClientCallbacks) = true + override fun evaluate( + callbacks: SshClientCallbacks, + strictKexEnabled: Boolean, + nonKexBeforeInitialKexInit: Boolean, + ) = true override fun renderTla() = "TRUE" } @@ -138,7 +169,11 @@ internal sealed interface SshFormalGuard { data class Fact( val fact: SshBooleanFact, ) : SshFormalGuard { - override fun evaluate(callbacks: SshClientCallbacks) = fact.evaluate(callbacks) + override fun evaluate( + callbacks: SshClientCallbacks, + strictKexEnabled: Boolean, + nonKexBeforeInitialKexInit: Boolean, + ) = fact.evaluate(callbacks, strictKexEnabled, nonKexBeforeInitialKexInit) override fun renderTla() = fact.tlaName } @@ -146,14 +181,34 @@ internal sealed interface SshFormalGuard { data class Not( val expression: SshFormalGuard, ) : SshFormalGuard { - override fun evaluate(callbacks: SshClientCallbacks) = !expression.evaluate(callbacks) + override fun evaluate( + callbacks: SshClientCallbacks, + strictKexEnabled: Boolean, + nonKexBeforeInitialKexInit: Boolean, + ) = !expression.evaluate(callbacks, strictKexEnabled, nonKexBeforeInitialKexInit) override fun renderTla() = "~(${expression.renderTla()})" } + + data class And( + val left: SshFormalGuard, + val right: SshFormalGuard, + ) : SshFormalGuard { + override fun evaluate( + callbacks: SshClientCallbacks, + strictKexEnabled: Boolean, + nonKexBeforeInitialKexInit: Boolean, + ) = left.evaluate(callbacks, strictKexEnabled, nonKexBeforeInitialKexInit) && + right.evaluate(callbacks, strictKexEnabled, nonKexBeforeInitialKexInit) + + override fun renderTla() = "(${left.renderTla()}) /\\ (${right.renderTla()})" + } } internal operator fun SshFormalGuard.not(): SshFormalGuard = SshFormalGuard.Not(this) +internal infix fun SshFormalGuard.and(other: SshFormalGuard): SshFormalGuard = SshFormalGuard.And(this, other) + internal data class SshFormalTransitionMeta( val id: SshTransitionId, val eventClass: KClass, @@ -318,8 +373,16 @@ internal data class SshStateMachineFormalModel( } }, variable("packetWasParsed", "FALSE") { "(origin' = ${quote(SshEventOrigin.PARSED_PACKET.tlaName)})" }, - variable("effects", "{}") { renderSet(it.effects.mapTo(sortedSetOf()) { effect -> effect.tlaName }) }, + variable("effects", "{}", ::renderEffectsUpdate), variable("rekeying", "FALSE", ::renderRekeyingUpdate), + FormalVariable("strictKex", "FALSE") { meta -> + when { + SshEffect.ENABLE_STRICT_KEX in meta.effects -> "strictKex' = TRUE" + SshEffect.NEGOTIATE_NON_STRICT_KEX in meta.effects -> "strictKex' = FALSE" + else -> "strictKex' = strictKex" + } + }, + variable("nonKexBeforeInitialKexInit", "FALSE", ::renderNonKexBeforeInitialKexInitUpdate), variable("authenticationEstablished", "FALSE", ::renderAuthenticationEstablishedUpdate), variable("initialNewKeysActive", "FALSE", ::renderInitialNewKeysActiveUpdate), variable("authRequestPending", "FALSE", ::renderAuthRequestPendingUpdate), @@ -464,8 +527,26 @@ internal data class SshStateMachineFormalModel( else -> "rekeying" } + private fun renderEffectsUpdate(meta: SshFormalTransitionMeta): String { + val resetEffects = meta.effects.intersect(STRICT_KEX_SEQUENCE_RESET_EFFECTS) + val regularEffects = meta.effects - resetEffects + val renderedRegularEffects = renderSet(regularEffects.mapTo(sortedSetOf()) { it.tlaName }) + if (resetEffects.isEmpty()) return renderedRegularEffects + + val renderedStrictEffects = renderSet(meta.effects.mapTo(sortedSetOf()) { it.tlaName }) + return "IF strictKex THEN $renderedStrictEffects ELSE $renderedRegularEffects" + } + private fun renderAuthenticationEstablishedUpdate(meta: SshFormalTransitionMeta): String = if (SshEffect.AUTHENTICATION_SUCCESS in meta.effects) "TRUE" else "authenticationEstablished" + private fun renderNonKexBeforeInitialKexInitUpdate(meta: SshFormalTransitionMeta): String = if (SshEffect.RECORD_NON_KEX_BEFORE_INITIAL_KEX_INIT in meta.effects) { + "TRUE" + } else if (SshEffect.CLEAR_NON_KEX_BEFORE_INITIAL_KEX_INIT in meta.effects) { + "FALSE" + } else { + "nonKexBeforeInitialKexInit" + } + private fun renderInitialNewKeysActiveUpdate(meta: SshFormalTransitionMeta): String = if (SshEffect.ACTIVATE_ENCRYPTION in meta.effects) "TRUE" else "initialNewKeysActive" private fun renderAuthRequestPendingUpdate(meta: SshFormalTransitionMeta): String = when { @@ -513,6 +594,10 @@ internal data class SshStateMachineFormalModel( SshTransitionId.AUTHENTICATION_FAILURE, SshTransitionId.AUTHORIZE_AUTHENTICATION_PACKET, ) + private val STRICT_KEX_SEQUENCE_RESET_EFFECTS = setOf( + SshEffect.RESET_INBOUND_SEQUENCE, + SshEffect.RESET_OUTBOUND_SEQUENCE, + ) private val CHANNEL_VARIABLE_NAMES = setOf( "channels", "previousChannels", diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionPacketClassificationTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionPacketClassificationTest.kt new file mode 100644 index 00000000..0354fc38 --- /dev/null +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionPacketClassificationTest.kt @@ -0,0 +1,41 @@ +/* + * ConnectBot SSH Library + * Copyright 2026 Kenny Root + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package org.connectbot.sshlib.client + +import org.connectbot.sshlib.protocol.SshEnums +import kotlin.test.Test +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class SshConnectionPacketClassificationTest { + @Test + fun `only transport key exchange messages bypass the strict kex gate`() { + assertTrue(isKeyExchangeMessage(SshEnums.MessageType.SSH_MSG_KEXINIT.id().toInt())) + assertTrue(isKeyExchangeMessage(SshEnums.MessageType.SSH_MSG_NEWKEYS.id().toInt())) + assertTrue(isKeyExchangeMessage(30)) + assertTrue(isKeyExchangeMessage(49)) + + assertFalse(isKeyExchangeMessage(SshEnums.MessageType.SSH_MSG_IGNORE.id().toInt())) + assertFalse(isKeyExchangeMessage(SshEnums.MessageType.SSH_MSG_DEBUG.id().toInt())) + assertFalse(isKeyExchangeMessage(SshEnums.MessageType.SSH_MSG_EXT_INFO.id().toInt())) + assertFalse(isKeyExchangeMessage(SshEnums.MessageType.SSH_MSG_SERVICE_ACCEPT.id().toInt())) + assertFalse(isKeyExchangeMessage(SshEnums.MessageType.SSH_MSG_DISCONNECT.id().toInt())) + assertFalse(isKeyExchangeMessage(29)) + assertFalse(isKeyExchangeMessage(50)) + } +} diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachineTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachineTest.kt index e5c9b797..abcf2e73 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachineTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachineTest.kt @@ -20,6 +20,7 @@ package org.connectbot.sshlib.protocol import kotlinx.coroutines.test.runTest import java.lang.reflect.Modifier import kotlin.test.Test +import kotlin.test.assertEquals import kotlin.test.assertFalse import kotlin.test.assertTrue @@ -104,6 +105,95 @@ class SshClientStateMachineTest { assertTrue(machine.authorizeAuthenticatedPacket()) } + @Test + fun `strict kex sequence resets remain enabled across rekey`() = runTest { + val callbacks = RecordingCallbacks().apply { strictKexNegotiated = true } + val machine = SshClientStateMachine(callbacks) + + assertTrue(machine.connect()) + assertTrue(machine.receiveVersion(IdBanner())) + assertTrue(machine.receiveKexInit(SshMsgKexinit())) + assertTrue(machine.receiveKexEcdhReply(SshMsgKexEcdhReply())) + assertTrue(machine.receiveNewKeys()) + assertTrue(machine.receiveServiceAccept("ssh-userauth")) + assertTrue(machine.beginAuthentication()) + assertTrue(machine.authenticationSuccess()) + + callbacks.strictKexNegotiated = false + assertTrue(machine.requestRekey()) + assertTrue(machine.receiveKexInit(SshMsgKexinit())) + assertTrue(machine.receiveKexEcdhReply(SshMsgKexEcdhReply())) + assertTrue(machine.receiveNewKeys()) + + assertTrue(machine.isStrictKexEnabled()) + assertEquals(listOf(true, true), callbacks.outboundSequenceResets) + assertEquals(listOf(true, true), callbacks.inboundSequenceResets) + assertEquals(listOf(true, false), callbacks.initialKexExchanges) + } + + @Test + fun `strict initial kex rejects every non-kex packet after kex init`() = runTest { + val callbacks = RecordingCallbacks().apply { strictKexNegotiated = true } + val machine = SshClientStateMachine(callbacks) + + assertTrue(machine.connect()) + assertTrue(machine.receiveVersion(IdBanner())) + assertTrue(machine.receiveKexInit(SshMsgKexinit())) + + assertFalse(machine.authorizeNonKexPacket("unexpected non-KEX packet")) + assertTrue("sendProtocolError:unexpected non-KEX packet" in callbacks.actions) + assertFalse(machine.receiveIgnore()) + } + + @Test + fun `strict kex retrospectively rejects a kex init that was not first`() = runTest { + val callbacks = RecordingCallbacks().apply { strictKexNegotiated = true } + val machine = SshClientStateMachine(callbacks) + + assertTrue(machine.connect()) + assertTrue(machine.receiveVersion(IdBanner())) + assertTrue(machine.authorizeNonKexPacket("early IGNORE")) + assertTrue(machine.receiveIgnore()) + assertTrue(machine.receiveKexInit(SshMsgKexinit())) + + assertTrue(machine.isDisconnected()) + assertTrue( + "sendProtocolError:SSH_MSG_KEXINIT was not the first packet during strict initial key exchange" in callbacks.actions, + ) + } + + @Test + fun `non-strict initial kex allows non-kex packet handling`() = runTest { + val callbacks = RecordingCallbacks() + val machine = SshClientStateMachine(callbacks) + + assertTrue(machine.connect()) + assertTrue(machine.receiveVersion(IdBanner())) + assertTrue(machine.authorizeNonKexPacket("early IGNORE")) + assertTrue(machine.receiveIgnore()) + assertTrue(machine.receiveKexInit(SshMsgKexinit())) + assertTrue(machine.authorizeNonKexPacket("IGNORE during non-strict KEX")) + } + + @Test + fun `strict rekey allows non-kex packet handling`() = runTest { + val callbacks = RecordingCallbacks().apply { strictKexNegotiated = true } + val machine = SshClientStateMachine(callbacks) + + assertTrue(machine.connect()) + assertTrue(machine.receiveVersion(IdBanner())) + assertTrue(machine.receiveKexInit(SshMsgKexinit())) + assertTrue(machine.receiveKexEcdhReply(SshMsgKexEcdhReply())) + assertTrue(machine.receiveNewKeys()) + assertTrue(machine.receiveServiceAccept("ssh-userauth")) + assertTrue(machine.beginAuthentication()) + assertTrue(machine.authenticationSuccess()) + + assertTrue(machine.requestRekey()) + assertTrue(machine.authorizeNonKexPacket("IGNORE during rekey")) + assertTrue(machine.receiveIgnore()) + } + @Test fun `a second kex init during key exchange is fatal`() = runTest { val callbacks = RecordingCallbacks() @@ -134,6 +224,10 @@ class SshClientStateMachineTest { val actions = mutableListOf() var rekeying = false var authenticationRequestPending = false + var strictKexNegotiated = false + val initialKexExchanges = mutableListOf() + val outboundSequenceResets = mutableListOf() + val inboundSequenceResets = mutableListOf() override fun sendVersion() { actions += "sendVersion" @@ -144,8 +238,10 @@ class SshClientStateMachineTest { override suspend fun sendKexInit() { actions += "sendKexInit" } - override fun receiveKexInit(msg: SshMsgKexinit) { + override fun receiveKexInit(msg: SshMsgKexinit, initialExchange: Boolean): Boolean { actions += "receiveKexInit" + initialKexExchanges += initialExchange + return strictKexNegotiated } override suspend fun sendKexExchangeInit() { actions += "sendKexExchangeInit" @@ -178,11 +274,13 @@ class SshClientStateMachineTest { override suspend fun sendKexDhGexInit() { actions += "sendKexDhGexInit" } - override suspend fun sendNewKeys() { + override suspend fun sendNewKeys(resetSequenceNumber: Boolean) { actions += "sendNewKeys" + outboundSequenceResets += resetSequenceNumber } - override fun receiveNewKeys() { + override fun receiveNewKeys(resetSequenceNumber: Boolean) { actions += "receiveNewKeys" + inboundSequenceResets += resetSequenceNumber } override fun activateEncryption() { actions += "activateEncryption" diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt index d9ccdb62..24579fe5 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt @@ -97,6 +97,96 @@ class SshStateMachineFormalModelTest { assertTrue(transitions.getValue(SshTransitionId.RECEIVE_REKEY_NEW_KEYS).meta.targetIsHistory) } + @Test + fun `strict kex negotiation and directional protection are explicit effects`() { + val transitions = createFormalModel().transitions.associateBy { it.meta.id } + + assertEquals( + "(~(rekeying)) /\\ (~(nonKexBeforeInitialKexInit))", + transitions.getValue(SshTransitionId.RECEIVE_INITIAL_STRICT_KEX_INIT).meta.guard.renderTla(), + ) + assertTrue( + SshEffect.ENABLE_STRICT_KEX in + transitions.getValue(SshTransitionId.RECEIVE_INITIAL_STRICT_KEX_INIT).meta.effects, + ) + assertTrue( + SshEffect.NEGOTIATE_NON_STRICT_KEX in + transitions.getValue(SshTransitionId.RECEIVE_INITIAL_NON_STRICT_KEX_INIT).meta.effects, + ) + assertEquals( + "rekeying", + transitions.getValue(SshTransitionId.RECEIVE_REKEY_KEX_INIT).meta.guard.renderTla(), + ) + assertTrue( + SshEffect.ENABLE_STRICT_KEX !in + transitions.getValue(SshTransitionId.RECEIVE_REKEY_KEX_INIT).meta.effects, + ) + assertTrue( + SshEffect.ACTIVATE_OUTBOUND_PROTECTION in + transitions.getValue(SshTransitionId.RECEIVE_KEX_ECDH_REPLY).meta.effects, + ) + assertTrue( + SshEffect.RESET_OUTBOUND_SEQUENCE in + transitions.getValue(SshTransitionId.RECEIVE_KEX_ECDH_REPLY).meta.effects, + ) + assertTrue( + SshEffect.ACTIVATE_INBOUND_PROTECTION in + transitions.getValue(SshTransitionId.RECEIVE_REKEY_NEW_KEYS).meta.effects, + ) + assertTrue( + SshEffect.RESET_INBOUND_SEQUENCE in + transitions.getValue(SshTransitionId.RECEIVE_REKEY_NEW_KEYS).meta.effects, + ) + } + + @Test + fun `strict initial kex rejection is declared by runtime transitions`() { + val transitions = createFormalModel().transitions.associateBy { it.meta.id } + val rejectionIds = setOf( + SshTransitionId.REJECT_NON_KEX_WAIT_KEX, + SshTransitionId.REJECT_NON_KEX_WAIT_KEX_DH_GEX_INIT, + SshTransitionId.REJECT_NON_KEX_WAIT_NEW_KEYS, + ) + + rejectionIds.forEach { id -> + val transition = transitions.getValue(id).meta + assertEquals("(strictKex) /\\ (~(rekeying))", transition.guard.renderTla()) + assertEquals(setOf(SshEffect.SEND_PROTOCOL_ERROR, SshEffect.DISCONNECT), transition.effects) + assertEquals("Disconnected", transition.targetStateName) + } + + val firstPacket = transitions.getValue(SshTransitionId.REJECT_STRICT_KEX_INIT_NOT_FIRST).meta + assertEquals( + "(~(rekeying)) /\\ (nonKexBeforeInitialKexInit)", + firstPacket.guard.renderTla(), + ) + assertEquals( + setOf( + SshEffect.RECEIVE_KEX_INIT, + SshEffect.ENABLE_STRICT_KEX, + SshEffect.SEND_PROTOCOL_ERROR, + SshEffect.DISCONNECT, + ), + firstPacket.effects, + ) + } + + @Test + fun `focused Terrapin model checks strict safety and expects non-strict counterexample`() { + val model = Files.readString(Path.of("src/test/resources/tla/SshTerrapin.tla")) + val strictConfig = Files.readString(Path.of("src/test/resources/tla/SshTerrapinStrict.cfg")) + val nonStrictConfig = Files.readString(Path.of("src/test/resources/tla/SshTerrapinNonStrict.cfg")) + + assertTrue("InjectUnauthenticatedIgnore ==" in model) + assertTrue("DropExtInfo ==" in model) + assertTrue("TerrapinSucceeded ==" in model) + assertTrue("NoTerrapin == ~TerrapinSucceeded" in model) + assertTrue("StrictKex = TRUE" in strictConfig) + assertTrue("StrictKex = FALSE" in nonStrictConfig) + assertTrue("INVARIANT NoTerrapin" in strictConfig) + assertTrue("INVARIANT NoTerrapin" in nonStrictConfig) + } + @Test fun `authentication requests are explicit formal side effects`() { val transitions = createFormalModel().transitions.associateBy { it.meta.id } @@ -147,6 +237,18 @@ class SshStateMachineFormalModelTest { assertTrue("INVARIANT GlobalChannelMutationIsDisconnectCascade" in config) } + @Test + fun `TLC explores strict and non-strict key exchange`() { + val rendered = createFormalModel().renderTla() + val config = Files.readString(Path.of("src/test/resources/tla/SshClientStateMachine.cfg")) + + assertTrue("strictKex' = TRUE" in rendered) + assertTrue("strictKex' = FALSE" in rendered) + assertTrue("IF strictKex THEN" in rendered) + assertTrue("INVARIANT StrictKexProtectionSwitchesResetSequenceNumbers" in config) + assertTrue("PROPERTY StrictKexIsSticky" in config) + } + @Test fun `checked in TLA model matches KStateMachine declaration`() { val expected = Files.readString(Path.of("src/test/resources/tla/SshClientStateMachineGenerated.tla")) diff --git a/sshlib/src/test/resources/tla/SshClientStateMachine.cfg b/sshlib/src/test/resources/tla/SshClientStateMachine.cfg index c3d5b9da..9adfa49f 100644 --- a/sshlib/src/test/resources/tla/SshClientStateMachine.cfg +++ b/sshlib/src/test/resources/tla/SshClientStateMachine.cfg @@ -27,10 +27,15 @@ INVARIANT NoHigherLayerPacketsSentDuringKex INVARIANT AuthenticationRequestIsGuarded INVARIANT AuthenticationRequestResponseClearsPending INVARIANT KexEventsAreStrictlySequenced +INVARIANT StrictKexProtectionSwitchesResetSequenceNumbers +INVARIANT StrictInitialKexRejectsNonKexPackets +INVARIANT StrictKexInitMustBeFirst +INVARIANT AcceptedInitialKexPacketOrderClearsHistory INVARIANT UserAuthenticationRequiresInitialNewKeys INVARIANT UnexpectedKexInitIsFatal PROPERTY AuthenticationNeverDowngrades PROPERTY DisconnectedIsTerminal +PROPERTY StrictKexIsSticky CHECK_DEADLOCK FALSE diff --git a/sshlib/src/test/resources/tla/SshClientStateMachine.tla b/sshlib/src/test/resources/tla/SshClientStateMachine.tla index 1f88d492..c42c96d1 100644 --- a/sshlib/src/test/resources/tla/SshClientStateMachine.tla +++ b/sshlib/src/test/resources/tla/SshClientStateMachine.tla @@ -44,6 +44,8 @@ TypeOK == /\ packetWasParsed \in BOOLEAN /\ effects \subseteq Effects /\ rekeying \in BOOLEAN + /\ strictKex \in BOOLEAN + /\ nonKexBeforeInitialKexInit \in BOOLEAN /\ authenticationEstablished \in BOOLEAN /\ initialNewKeysActive \in BOOLEAN /\ authRequestPending \in BOOLEAN @@ -123,6 +125,8 @@ ModelView == packetWasParsed, effects, rekeying, + strictKex, + nonKexBeforeInitialKexInit, authenticationEstablished, initialNewKeysActive, authRequestPending, @@ -194,7 +198,8 @@ AuthenticationRequestResponseClearsPending == ~authRequestPending KexEventsAreStrictlySequenced == - /\ event = "ReceiveKexInit" => + /\ event \in {"ReceiveInitialStrictKexInit", "ReceiveInitialNonStrictKexInit", "ReceiveRekeyKexInit"} /\ + "Disconnect" \notin effects => /\ previousState = "WaitKexInit" /\ state = "WaitKex" /\ "SendKexExchangeInit" \in effects @@ -202,6 +207,8 @@ KexEventsAreStrictlySequenced == /\ previousState = "WaitKex" /\ state = "WaitNewKeys" /\ "SendNewKeys" \in effects + /\ "ActivateOutboundProtection" \in effects + /\ (strictKex => "ResetOutboundSequence" \in effects) /\ event = "ReceiveKex.DhGexGroup" => /\ previousState = "WaitKex" /\ state = "WaitKexDhGexInit" @@ -210,9 +217,40 @@ KexEventsAreStrictlySequenced == /\ previousState = "WaitKexDhGexInit" /\ state = "WaitNewKeys" /\ "SendNewKeys" \in effects + /\ "ActivateOutboundProtection" \in effects + /\ (strictKex => "ResetOutboundSequence" \in effects) /\ event = "ReceiveNewKeys" => /\ previousState = "WaitNewKeys" /\ "ActivateEncryption" \in effects + /\ "ActivateInboundProtection" \in effects + /\ (strictKex => "ResetInboundSequence" \in effects) + +StrictKexProtectionSwitchesResetSequenceNumbers == + strictKex => + /\ ("ActivateOutboundProtection" \in effects => "ResetOutboundSequence" \in effects) + /\ ("ActivateInboundProtection" \in effects => "ResetInboundSequence" \in effects) + +StrictKexIsSticky == + [] (strictKex => [] strictKex) + +StrictInitialKexRejectsNonKexPackets == + event = "ReceiveNonKexPacket" /\ previousState \in {"WaitKex", "WaitKexDhGexInit", "WaitNewKeys"} => + /\ strictKex + /\ state = "Disconnected" + /\ "SendProtocolError" \in effects + /\ "Disconnect" \in effects + +StrictKexInitMustBeFirst == + event = "ReceiveInitialStrictKexInit" /\ "Disconnect" \in effects => + /\ strictKex + /\ nonKexBeforeInitialKexInit + /\ previousState = "WaitKexInit" + /\ state = "Disconnected" + +AcceptedInitialKexPacketOrderClearsHistory == + event \in {"ReceiveInitialStrictKexInit", "ReceiveInitialNonStrictKexInit"} /\ "Disconnect" \notin effects => + /\ state = "WaitKex" + /\ ~nonKexBeforeInitialKexInit UserAuthenticationRequiresInitialNewKeys == event = "BeginAuthentication" \/ "StartAuthentication" \in effects \/ "SendUserauthRequest" \in effects => diff --git a/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla b/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla index 3bdf542e..3222634a 100644 --- a/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla +++ b/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla @@ -1,7 +1,7 @@ ---- MODULE SshClientStateMachineGenerated ---- \* Generated from SshClientStateMachine. Do not edit. -\* Model SHA-256: 882c266edfb2fed9a28f79bc2ce7a5d343d87371ecfc9c9ca2ff42c467ed0a5f -\* Lifecycle states: 11; transitions: 36. +\* Model SHA-256: a34440960298ca1cd17a21377130492c5d394fe258e172479153503aaf3b61c0 +\* Lifecycle states: 11; transitions: 43. \* TLC distinct states count full variable valuations, not lifecycle nodes. EXTENDS Naturals @@ -10,16 +10,16 @@ CONSTANT MaxChannels ChannelIDs == 1..MaxChannels ChannelAttemptIDs == 0..(MaxChannels + 1) -VARIABLES state, previousState, history, event, origin, packetWasParsed, effects, rekeying, authenticationEstablished, initialNewKeysActive, authRequestPending, previousAuthRequestPending, previousChannels, activeChannel, channelEvent, channelOrigin, channels, channelEffects +VARIABLES state, previousState, history, event, origin, packetWasParsed, effects, rekeying, strictKex, nonKexBeforeInitialKexInit, authenticationEstablished, initialNewKeysActive, authRequestPending, previousAuthRequestPending, previousChannels, activeChannel, channelEvent, channelOrigin, channels, channelEffects -vars == <> +vars == <> States == {"Authenticated", "Authenticating", "AuthenticationReady", "Disconnected", "Unconnected", "WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys", "WaitService", "WaitVersion"} PostAuthenticatedStates == {"Authenticated", "Authenticating", "AuthenticationReady"} KexStates == {"WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys"} -Events == {"AuthenticationFailure", "AuthenticationSuccess", "AuthorizeAuthenticatedPacket", "AuthorizeAuthenticationPacket", "AuthorizeConnectionPacket", "AuthorizeExtInfo", "BeginAuthentication", "Connect", "Disconnect", "OpenChannel", "ReceiveChannelFailure", "ReceiveChannelOpenConfirmation", "ReceiveChannelOpenFailure", "ReceiveChannelSuccess", "ReceiveDebug", "ReceiveGlobalRequest", "ReceiveIgnore", "ReceiveKex.DhGexGroup", "ReceiveKex.DhGexReply", "ReceiveKex.DhReply", "ReceiveKex.EcdhReply", "ReceiveKexInit", "ReceiveNewKeys", "ReceiveServiceAccept", "ReceiveUserauthBanner", "ReceiveUserauthInfoRequest", "ReceiveVersion", "RekeyStarted", "SendChannelRequest", "UnexpectedKexInit"} +Events == {"AuthenticationFailure", "AuthenticationSuccess", "AuthorizeAuthenticatedPacket", "AuthorizeAuthenticationPacket", "AuthorizeConnectionPacket", "AuthorizeExtInfo", "BeginAuthentication", "Connect", "Disconnect", "OpenChannel", "ReceiveChannelFailure", "ReceiveChannelOpenConfirmation", "ReceiveChannelOpenFailure", "ReceiveChannelSuccess", "ReceiveDebug", "ReceiveGlobalRequest", "ReceiveIgnore", "ReceiveInitialNonStrictKexInit", "ReceiveInitialStrictKexInit", "ReceiveKex.DhGexGroup", "ReceiveKex.DhGexReply", "ReceiveKex.DhReply", "ReceiveKex.EcdhReply", "ReceiveNewKeys", "ReceiveNonKexPacket", "ReceiveRekeyKexInit", "ReceiveServiceAccept", "ReceiveUserauthBanner", "ReceiveUserauthInfoRequest", "ReceiveVersion", "RekeyStarted", "SendChannelRequest", "UnexpectedKexInit"} Origins == {"Internal", "LocalCommand", "ParsedPacket", "Timer"} -Effects == {"ActivateEncryption", "AuthenticationFailure", "AuthenticationSuccess", "Debug", "Disconnect", "Ignore", "ReceiveChannelFailure", "ReceiveChannelOpenConfirmation", "ReceiveChannelOpenFailure", "ReceiveChannelSuccess", "ReceiveGlobalRequest", "ReceiveKexDhGexReply", "ReceiveKexDhReply", "ReceiveKexEcdhReply", "ReceiveKexInit", "ReceiveNewKeys", "ReceiveServiceAccept", "ReceiveUserauthBanner", "ReceiveUserauthInfoRequest", "ReceiveVersion", "RekeyComplete", "RekeyStarted", "SendChannelOpen", "SendChannelRequest", "SendClientExtInfo", "SendKexDhGexInit", "SendKexExchangeInit", "SendKexInit", "SendNewKeys", "SendProtocolError", "SendServiceRequest", "SendUserauthRequest", "SendVersion", "StartAuthentication"} +Effects == {"ActivateEncryption", "ActivateInboundProtection", "ActivateOutboundProtection", "AuthenticationFailure", "AuthenticationSuccess", "ClearNonKexBeforeInitialKexInit", "Debug", "Disconnect", "EnableStrictKex", "Ignore", "NegotiateNonStrictKex", "ReceiveChannelFailure", "ReceiveChannelOpenConfirmation", "ReceiveChannelOpenFailure", "ReceiveChannelSuccess", "ReceiveGlobalRequest", "ReceiveKexDhGexReply", "ReceiveKexDhReply", "ReceiveKexEcdhReply", "ReceiveKexInit", "ReceiveNewKeys", "ReceiveServiceAccept", "ReceiveUserauthBanner", "ReceiveUserauthInfoRequest", "ReceiveVersion", "RecordNonKexBeforeInitialKexInit", "RekeyComplete", "RekeyStarted", "ResetInboundSequence", "ResetOutboundSequence", "SendChannelOpen", "SendChannelRequest", "SendClientExtInfo", "SendKexDhGexInit", "SendKexExchangeInit", "SendKexInit", "SendNewKeys", "SendProtocolError", "SendServiceRequest", "SendUserauthRequest", "SendVersion", "StartAuthentication"} ChannelStates == {"BOTH_EOF", "CLOSED", "CLOSE_SENT", "LOCAL_EOF", "OPEN", "OPENING", "REMOTE_EOF", "Unallocated"} ChannelEvents == {"AcceptRemoteOpen", "AllocateLocalOpen", "OpenConfirmed", "OpenFailed", "ReceiveClose", "ReceiveData", "ReceiveEof", "ReceiveRequest", "ReceiveWindowAdjust", "SendClose", "SendData", "SendEof", "SendRequest"} @@ -174,7 +174,7 @@ AttemptChannelOperation == ELSE /\ channels' = channels /\ channelEffects' = {} - /\ UNCHANGED <> + /\ UNCHANGED <> Init == /\ state = "Unconnected" @@ -185,6 +185,8 @@ Init == /\ packetWasParsed = FALSE /\ effects = {} /\ rekeying = FALSE + /\ strictKex = FALSE + /\ nonKexBeforeInitialKexInit = FALSE /\ authenticationEstablished = FALSE /\ initialNewKeysActive = FALSE /\ authRequestPending = FALSE @@ -206,6 +208,8 @@ AUTHENTICATION_FAILURE == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"AuthenticationFailure"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE @@ -227,6 +231,8 @@ AUTHENTICATION_SUCCESS == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"AuthenticationSuccess"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = TRUE /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE @@ -248,6 +254,8 @@ AUTHORIZE_AUTHENTICATED_PACKET == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -269,6 +277,8 @@ AUTHORIZE_AUTHENTICATION_PACKET == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE @@ -290,6 +300,8 @@ AUTHORIZE_CONNECTION_PACKET == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -311,6 +323,8 @@ AUTHORIZE_POST_AUTH_EXT_INFO == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -332,6 +346,8 @@ AUTHORIZE_SERVICE_EXT_INFO == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -354,6 +370,8 @@ BEGIN_AUTHENTICATION == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"SendUserauthRequest"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = TRUE @@ -375,6 +393,8 @@ CONNECT == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"SendVersion"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -396,6 +416,8 @@ DISCONNECT == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"Disconnect"} /\ rekeying' = FALSE + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE @@ -417,6 +439,8 @@ OPEN_CHANNEL == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"SendChannelOpen"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -438,6 +462,8 @@ RECEIVE_CHANNEL_FAILURE == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveChannelFailure"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -459,6 +485,8 @@ RECEIVE_CHANNEL_OPEN_CONFIRMATION == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveChannelOpenConfirmation"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -480,6 +508,8 @@ RECEIVE_CHANNEL_OPEN_FAILURE == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveChannelOpenFailure"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -501,6 +531,8 @@ RECEIVE_CHANNEL_SUCCESS == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveChannelSuccess"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -522,6 +554,8 @@ RECEIVE_DEBUG == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"Debug"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -543,6 +577,8 @@ RECEIVE_GLOBAL_REQUEST == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveGlobalRequest"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -564,6 +600,8 @@ RECEIVE_IGNORE == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"Ignore"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -584,8 +622,10 @@ RECEIVE_INITIAL_NEW_KEYS == /\ event' = "ReceiveNewKeys" /\ origin' = "ParsedPacket" /\ packetWasParsed' = (origin' = "ParsedPacket") - /\ effects' = {"ActivateEncryption", "ReceiveNewKeys", "SendClientExtInfo", "SendServiceRequest"} + /\ effects' = IF strictKex THEN {"ActivateEncryption", "ActivateInboundProtection", "ReceiveNewKeys", "ResetInboundSequence", "SendClientExtInfo", "SendServiceRequest"} ELSE {"ActivateEncryption", "ActivateInboundProtection", "ReceiveNewKeys", "SendClientExtInfo", "SendServiceRequest"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = TRUE /\ authRequestPending' = authRequestPending @@ -597,6 +637,54 @@ RECEIVE_INITIAL_NEW_KEYS == /\ channels' = channels /\ channelEffects' = {} +RECEIVE_INITIAL_NON_STRICT_KEX_INIT == + /\ state \in {"WaitKexInit"} + /\ ~(rekeying) + /\ state' = "WaitKex" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveInitialNonStrictKexInit" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ClearNonKexBeforeInitialKexInit", "NegotiateNonStrictKex", "ReceiveKexInit", "SendKexExchangeInit"} + /\ rekeying' = rekeying + /\ strictKex' = FALSE + /\ nonKexBeforeInitialKexInit' = FALSE + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_INITIAL_STRICT_KEX_INIT == + /\ state \in {"WaitKexInit"} + /\ (~(rekeying)) /\ (~(nonKexBeforeInitialKexInit)) + /\ state' = "WaitKex" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveInitialStrictKexInit" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"ClearNonKexBeforeInitialKexInit", "EnableStrictKex", "ReceiveKexInit", "SendKexExchangeInit"} + /\ rekeying' = rekeying + /\ strictKex' = TRUE + /\ nonKexBeforeInitialKexInit' = FALSE + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + RECEIVE_KEX_DH_GEX_GROUP == /\ state \in {"WaitKex"} /\ state' = "WaitKexDhGexInit" @@ -607,6 +695,8 @@ RECEIVE_KEX_DH_GEX_GROUP == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"SendKexDhGexInit"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -626,8 +716,10 @@ RECEIVE_KEX_DH_GEX_REPLY == /\ event' = "ReceiveKex.DhGexReply" /\ origin' = "ParsedPacket" /\ packetWasParsed' = (origin' = "ParsedPacket") - /\ effects' = {"ReceiveKexDhGexReply", "SendNewKeys"} + /\ effects' = IF strictKex THEN {"ActivateOutboundProtection", "ReceiveKexDhGexReply", "ResetOutboundSequence", "SendNewKeys"} ELSE {"ActivateOutboundProtection", "ReceiveKexDhGexReply", "SendNewKeys"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -647,8 +739,10 @@ RECEIVE_KEX_DH_REPLY == /\ event' = "ReceiveKex.DhReply" /\ origin' = "ParsedPacket" /\ packetWasParsed' = (origin' = "ParsedPacket") - /\ effects' = {"ReceiveKexDhReply", "SendNewKeys"} + /\ effects' = IF strictKex THEN {"ActivateOutboundProtection", "ReceiveKexDhReply", "ResetOutboundSequence", "SendNewKeys"} ELSE {"ActivateOutboundProtection", "ReceiveKexDhReply", "SendNewKeys"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -668,8 +762,10 @@ RECEIVE_KEX_ECDH_REPLY == /\ event' = "ReceiveKex.EcdhReply" /\ origin' = "ParsedPacket" /\ packetWasParsed' = (origin' = "ParsedPacket") - /\ effects' = {"ReceiveKexEcdhReply", "SendNewKeys"} + /\ effects' = IF strictKex THEN {"ActivateOutboundProtection", "ReceiveKexEcdhReply", "ResetOutboundSequence", "SendNewKeys"} ELSE {"ActivateOutboundProtection", "ReceiveKexEcdhReply", "SendNewKeys"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -681,16 +777,19 @@ RECEIVE_KEX_ECDH_REPLY == /\ channels' = channels /\ channelEffects' = {} -RECEIVE_KEX_INIT == +RECEIVE_REKEY_KEX_INIT == /\ state \in {"WaitKexInit"} + /\ rekeying /\ state' = "WaitKex" /\ previousState' = state /\ history' = history - /\ event' = "ReceiveKexInit" + /\ event' = "ReceiveRekeyKexInit" /\ origin' = "ParsedPacket" /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveKexInit", "SendKexExchangeInit"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -711,8 +810,10 @@ RECEIVE_REKEY_NEW_KEYS == /\ event' = "ReceiveNewKeys" /\ origin' = "ParsedPacket" /\ packetWasParsed' = (origin' = "ParsedPacket") - /\ effects' = {"ActivateEncryption", "ReceiveNewKeys", "RekeyComplete"} + /\ effects' = IF strictKex THEN {"ActivateEncryption", "ActivateInboundProtection", "ReceiveNewKeys", "RekeyComplete", "ResetInboundSequence"} ELSE {"ActivateEncryption", "ActivateInboundProtection", "ReceiveNewKeys", "RekeyComplete"} /\ rekeying' = FALSE + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = TRUE /\ authRequestPending' = authRequestPending @@ -734,6 +835,8 @@ RECEIVE_SERVICE_ACCEPT == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveServiceAccept", "StartAuthentication"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -755,6 +858,8 @@ RECEIVE_USERAUTH_BANNER_AUTHENTICATING == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveUserauthBanner"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -776,6 +881,8 @@ RECEIVE_USERAUTH_BANNER_READY == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveUserauthBanner"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -797,6 +904,8 @@ RECEIVE_USERAUTH_INFO_REQUEST == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveUserauthInfoRequest"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -818,6 +927,8 @@ RECEIVE_VERSION == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveVersion", "SendKexInit"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -829,6 +940,126 @@ RECEIVE_VERSION == /\ channels' = channels /\ channelEffects' = {} +RECORD_NON_KEX_BEFORE_INITIAL_KEX_INIT == + /\ state \in {"WaitKexInit"} + /\ ~(rekeying) + /\ state' = state + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveNonKexPacket" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"RecordNonKexBeforeInitialKexInit"} + /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = TRUE + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +REJECT_NON_KEX_WAIT_KEX == + /\ state \in {"WaitKex"} + /\ (strictKex) /\ (~(rekeying)) + /\ state' = "Disconnected" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveNonKexPacket" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"Disconnect", "SendProtocolError"} + /\ rekeying' = FALSE + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = FALSE + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = [c \in ChannelIDs |-> IF channels[c] = "Unallocated" THEN "Unallocated" ELSE "CLOSED"] + /\ channelEffects' = {} + +REJECT_NON_KEX_WAIT_KEX_DH_GEX_INIT == + /\ state \in {"WaitKexDhGexInit"} + /\ (strictKex) /\ (~(rekeying)) + /\ state' = "Disconnected" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveNonKexPacket" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"Disconnect", "SendProtocolError"} + /\ rekeying' = FALSE + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = FALSE + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = [c \in ChannelIDs |-> IF channels[c] = "Unallocated" THEN "Unallocated" ELSE "CLOSED"] + /\ channelEffects' = {} + +REJECT_NON_KEX_WAIT_NEW_KEYS == + /\ state \in {"WaitNewKeys"} + /\ (strictKex) /\ (~(rekeying)) + /\ state' = "Disconnected" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveNonKexPacket" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"Disconnect", "SendProtocolError"} + /\ rekeying' = FALSE + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = FALSE + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = [c \in ChannelIDs |-> IF channels[c] = "Unallocated" THEN "Unallocated" ELSE "CLOSED"] + /\ channelEffects' = {} + +REJECT_STRICT_KEX_INIT_NOT_FIRST == + /\ state \in {"WaitKexInit"} + /\ (~(rekeying)) /\ (nonKexBeforeInitialKexInit) + /\ state' = "Disconnected" + /\ previousState' = state + /\ history' = history + /\ event' = "ReceiveInitialStrictKexInit" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = (origin' = "ParsedPacket") + /\ effects' = {"Disconnect", "EnableStrictKex", "ReceiveKexInit", "SendProtocolError"} + /\ rekeying' = FALSE + /\ strictKex' = TRUE + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = FALSE + /\ previousAuthRequestPending' = authRequestPending + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = [c \in ChannelIDs |-> IF channels[c] = "Unallocated" THEN "Unallocated" ELSE "CLOSED"] + /\ channelEffects' = {} + REKEY_STARTED == /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady"} /\ state' = "WaitKexInit" @@ -839,6 +1070,8 @@ REKEY_STARTED == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"RekeyStarted", "SendKexInit"} /\ rekeying' = TRUE + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -861,6 +1094,8 @@ REPEAT_BEGIN_AUTHENTICATION == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"SendUserauthRequest"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = TRUE @@ -882,6 +1117,8 @@ SEND_CHANNEL_REQUEST == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"SendChannelRequest"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending @@ -903,6 +1140,8 @@ UNEXPECTED_KEX_INIT_WAIT_KEX == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"Disconnect", "SendProtocolError"} /\ rekeying' = FALSE + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE @@ -924,6 +1163,8 @@ UNEXPECTED_KEX_INIT_WAIT_KEX_DH_GEX_INIT == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"Disconnect", "SendProtocolError"} /\ rekeying' = FALSE + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE @@ -945,6 +1186,8 @@ UNEXPECTED_KEX_INIT_WAIT_NEW_KEYS == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"Disconnect", "SendProtocolError"} /\ rekeying' = FALSE + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE @@ -976,17 +1219,24 @@ Next == \/ RECEIVE_GLOBAL_REQUEST \/ RECEIVE_IGNORE \/ RECEIVE_INITIAL_NEW_KEYS + \/ RECEIVE_INITIAL_NON_STRICT_KEX_INIT + \/ RECEIVE_INITIAL_STRICT_KEX_INIT \/ RECEIVE_KEX_DH_GEX_GROUP \/ RECEIVE_KEX_DH_GEX_REPLY \/ RECEIVE_KEX_DH_REPLY \/ RECEIVE_KEX_ECDH_REPLY - \/ RECEIVE_KEX_INIT + \/ RECEIVE_REKEY_KEX_INIT \/ RECEIVE_REKEY_NEW_KEYS \/ RECEIVE_SERVICE_ACCEPT \/ RECEIVE_USERAUTH_BANNER_AUTHENTICATING \/ RECEIVE_USERAUTH_BANNER_READY \/ RECEIVE_USERAUTH_INFO_REQUEST \/ RECEIVE_VERSION + \/ RECORD_NON_KEX_BEFORE_INITIAL_KEX_INIT + \/ REJECT_NON_KEX_WAIT_KEX + \/ REJECT_NON_KEX_WAIT_KEX_DH_GEX_INIT + \/ REJECT_NON_KEX_WAIT_NEW_KEYS + \/ REJECT_STRICT_KEX_INIT_NOT_FIRST \/ REKEY_STARTED \/ REPEAT_BEGIN_AUTHENTICATION \/ SEND_CHANNEL_REQUEST diff --git a/sshlib/src/test/resources/tla/SshTerrapin.tla b/sshlib/src/test/resources/tla/SshTerrapin.tla new file mode 100644 index 00000000..9a069779 --- /dev/null +++ b/sshlib/src/test/resources/tla/SshTerrapin.tla @@ -0,0 +1,218 @@ +---- MODULE SshTerrapin ---- +EXTENDS Naturals + +\* Focused server-to-client Terrapin abstraction; the opposite direction is symmetric. +\* Protected packets authenticate only when their sequence number matches receiverSeq. +\* InjectUnauthenticatedIgnore includes strict KEX's retrospective "KEXINIT first" check. +\* Cryptographic keys, bytes, and forgery are intentionally outside this control-flow model. + +CONSTANT StrictKex + +Phases == {"InitialKex", "Encrypted", "Aborted"} +Packets == {"Empty", "ExtInfo", "ServiceAccept"} +SequenceNumbers == 0..2 + +VARIABLES phase, + senderSeq, + receiverSeq, + wirePacket, + wireSeq, + injectedIgnore, + extInfoSent, + extInfoReceived, + extInfoDropped, + serviceSent, + serviceAccepted + +vars == <> + +Init == + /\ phase = "InitialKex" + /\ senderSeq = 0 + /\ receiverSeq = 0 + /\ wirePacket = "Empty" + /\ wireSeq = 0 + /\ injectedIgnore = FALSE + /\ extInfoSent = FALSE + /\ extInfoReceived = FALSE + /\ extInfoDropped = FALSE + /\ serviceSent = FALSE + /\ serviceAccepted = FALSE + +InjectUnauthenticatedIgnore == + /\ phase = "InitialKex" + /\ injectedIgnore = FALSE + /\ injectedIgnore' = TRUE + /\ IF StrictKex + THEN + /\ phase' = "Aborted" + /\ receiverSeq' = receiverSeq + ELSE + /\ phase' = phase + /\ receiverSeq' = receiverSeq + 1 + /\ UNCHANGED <> + +CompleteInitialKex == + /\ phase = "InitialKex" + /\ phase' = "Encrypted" + /\ IF StrictKex + THEN + /\ senderSeq' = 0 + /\ receiverSeq' = 0 + ELSE + /\ UNCHANGED <> + /\ UNCHANGED <> + +SendExtInfo == + /\ phase = "Encrypted" + /\ wirePacket = "Empty" + /\ extInfoSent = FALSE + /\ senderSeq < 2 + /\ wirePacket' = "ExtInfo" + /\ wireSeq' = senderSeq + /\ senderSeq' = senderSeq + 1 + /\ extInfoSent' = TRUE + /\ UNCHANGED <> + +ReceiveExtInfo == + /\ phase = "Encrypted" + /\ wirePacket = "ExtInfo" + /\ wirePacket' = "Empty" + /\ IF wireSeq = receiverSeq + THEN + /\ receiverSeq' = receiverSeq + 1 + /\ extInfoReceived' = TRUE + /\ phase' = phase + ELSE + /\ receiverSeq' = receiverSeq + /\ extInfoReceived' = extInfoReceived + /\ phase' = "Aborted" + /\ UNCHANGED <> + +DropExtInfo == + /\ phase = "Encrypted" + /\ wirePacket = "ExtInfo" + /\ wirePacket' = "Empty" + /\ extInfoDropped' = TRUE + /\ UNCHANGED <> + +SendServiceAccept == + /\ phase = "Encrypted" + /\ wirePacket = "Empty" + /\ extInfoSent + /\ serviceSent = FALSE + /\ senderSeq < 2 + /\ wirePacket' = "ServiceAccept" + /\ wireSeq' = senderSeq + /\ senderSeq' = senderSeq + 1 + /\ serviceSent' = TRUE + /\ UNCHANGED <> + +ReceiveServiceAccept == + /\ phase = "Encrypted" + /\ wirePacket = "ServiceAccept" + /\ wirePacket' = "Empty" + /\ IF wireSeq = receiverSeq + THEN + /\ receiverSeq' = receiverSeq + 1 + /\ serviceAccepted' = TRUE + /\ phase' = phase + ELSE + /\ receiverSeq' = receiverSeq + /\ serviceAccepted' = serviceAccepted + /\ phase' = "Aborted" + /\ UNCHANGED <> + +Next == + \/ InjectUnauthenticatedIgnore + \/ CompleteInitialKex + \/ SendExtInfo + \/ ReceiveExtInfo + \/ DropExtInfo + \/ SendServiceAccept + \/ ReceiveServiceAccept + +Spec == Init /\ [][Next]_vars + +TypeOK == + /\ StrictKex \in BOOLEAN + /\ phase \in Phases + /\ senderSeq \in SequenceNumbers + /\ receiverSeq \in SequenceNumbers + /\ wirePacket \in Packets + /\ wireSeq \in SequenceNumbers + /\ injectedIgnore \in BOOLEAN + /\ extInfoSent \in BOOLEAN + /\ extInfoReceived \in BOOLEAN + /\ extInfoDropped \in BOOLEAN + /\ serviceSent \in BOOLEAN + /\ serviceAccepted \in BOOLEAN + +TerrapinSucceeded == + /\ extInfoDropped + /\ extInfoReceived = FALSE + /\ serviceAccepted + /\ phase # "Aborted" + +NoTerrapin == ~TerrapinSucceeded + +StrictInjectionAborts == + StrictKex /\ injectedIgnore => phase = "Aborted" + +==== diff --git a/sshlib/src/test/resources/tla/SshTerrapinNonStrict.cfg b/sshlib/src/test/resources/tla/SshTerrapinNonStrict.cfg new file mode 100644 index 00000000..152a46c3 --- /dev/null +++ b/sshlib/src/test/resources/tla/SshTerrapinNonStrict.cfg @@ -0,0 +1,8 @@ +SPECIFICATION Spec + +CONSTANT StrictKex = FALSE + +INVARIANT TypeOK +INVARIANT NoTerrapin + +CHECK_DEADLOCK FALSE diff --git a/sshlib/src/test/resources/tla/SshTerrapinStrict.cfg b/sshlib/src/test/resources/tla/SshTerrapinStrict.cfg new file mode 100644 index 00000000..d497e94a --- /dev/null +++ b/sshlib/src/test/resources/tla/SshTerrapinStrict.cfg @@ -0,0 +1,9 @@ +SPECIFICATION Spec + +CONSTANT StrictKex = TRUE + +INVARIANT TypeOK +INVARIANT NoTerrapin +INVARIANT StrictInjectionAborts + +CHECK_DEADLOCK FALSE From a1ab06aa930b0318a6a0282d049f8d1ef0007a2b Mon Sep 17 00:00:00 2001 From: Kenny Root Date: Wed, 22 Jul 2026 21:06:20 -0700 Subject: [PATCH 3/4] feat(tla+): model hostile environment Also need to start sending Unimplemented messages instead of dropping packets to maintain sequence. --- sshlib/build.gradle.kts | 78 +- .../connectbot/sshlib/client/SshConnection.kt | 47 +- .../sshlib/protocol/SshClientStateMachine.kt | 6 + .../protocol/SshStateMachineFormalModel.kt | 309 +++++++- .../connectbot/sshlib/transport/PacketIO.kt | 17 +- .../connectbot/sshlib/client/FakeSshServer.kt | 28 + .../sshlib/client/SshConnectionFlowTest.kt | 17 + .../protocol/SshStateMachineTlaGenerator.kt | 15 + .../resources/tla/SshClientStateMachine.cfg | 9 + .../resources/tla/SshClientStateMachine.tla | 74 ++ .../tla/SshClientStateMachineGenerated.tla | 728 +++++++++++++++++- .../tla/SshClientStateMachineHostilePeer.cfg | 28 + .../tla/SshClientStateMachineOnPath.cfg | 28 + .../tla/SshClientStateMachineUnsafeProof.cfg | 14 + 14 files changed, 1370 insertions(+), 28 deletions(-) create mode 100644 sshlib/src/test/resources/tla/SshClientStateMachineHostilePeer.cfg create mode 100644 sshlib/src/test/resources/tla/SshClientStateMachineOnPath.cfg create mode 100644 sshlib/src/test/resources/tla/SshClientStateMachineUnsafeProof.cfg diff --git a/sshlib/build.gradle.kts b/sshlib/build.gradle.kts index 2ad46101..67989afa 100644 --- a/sshlib/build.gradle.kts +++ b/sshlib/build.gradle.kts @@ -116,6 +116,75 @@ tasks.register("checkSshStateMachineTla") { } } +listOf( + "OnPath" to "SshClientStateMachineOnPath.cfg", + "HostilePeer" to "SshClientStateMachineHostilePeer.cfg", +).forEach { (profile, configFile) -> + tasks.register("checkSshStateMachine${profile}Tla") { + group = "verification" + description = "Checks the generated SSH lifecycle model with the $profile hostile environment" + mainClass.set("tlc2.TLC") + workingDir(tlaModelDirectory) + args( + "-workers", + "1", + "-metadir", + tlaStateDirectory.get().dir("ssh-${profile.lowercase()}").asFile.absolutePath, + "-config", + configFile, + "SshClientStateMachine.tla", + ) + jvmArgs("-XX:+UseParallelGC") + doFirst { + val jarPath = tla2toolsJar.orNull + ?: throw GradleException( + "Set -Ptla2toolsJar=/path/to/tla2tools.jar or TLA2TOOLS_JAR to run TLC", + ) + classpath = files(jarPath) + } + } +} + +val unsafeProofCounterexampleOutput = ByteArrayOutputStream() +tasks.register("checkSshStateMachineUnsafeProofTla") { + group = "verification" + description = "Requires TLC to find a hostile KEX counterexample when proof verification is disabled" + mainClass.set("tlc2.TLC") + workingDir(tlaModelDirectory) + args( + "-workers", + "1", + "-metadir", + tlaStateDirectory.get().dir("ssh-unsafe-proof").asFile.absolutePath, + "-config", + "SshClientStateMachineUnsafeProof.cfg", + "SshClientStateMachine.tla", + ) + jvmArgs("-XX:+UseParallelGC") + standardOutput = unsafeProofCounterexampleOutput + errorOutput = unsafeProofCounterexampleOutput + isIgnoreExitValue = true + doFirst { + unsafeProofCounterexampleOutput.reset() + val jarPath = tla2toolsJar.orNull + ?: throw GradleException( + "Set -Ptla2toolsJar=/path/to/tla2tools.jar or TLA2TOOLS_JAR to run TLC", + ) + classpath = files(jarPath) + } + doLast { + val output = unsafeProofCounterexampleOutput.toString(Charsets.UTF_8) + logger.lifecycle(output) + val exitValue = executionResult.get().exitValue + if (exitValue == 0 || "Invariant HostileKexReplyRequiresPossessionProof is violated" !in output) { + throw GradleException( + "Expected TLC to find the disabled-proof counterexample; exit=$exitValue", + ) + } + logger.lifecycle("Expected disabled-proof counterexample found; treating it as success.") + } +} + tasks.register("checkSftpStateMachineTla") { group = "verification" description = "Checks the generated SFTP lifecycle model with TLC" @@ -219,7 +288,14 @@ tasks.register("generateTla") { tasks.register("checkTla") { group = "verification" description = "Checks all TLA+ formal models (SSH and SFTP) with TLC" - dependsOn("checkSshStateMachineTla", "checkSftpStateMachineTla", "checkSshTerrapinTla") + dependsOn( + "checkSshStateMachineTla", + "checkSshStateMachineOnPathTla", + "checkSshStateMachineHostilePeerTla", + "checkSshStateMachineUnsafeProofTla", + "checkSftpStateMachineTla", + "checkSshTerrapinTla", + ) } java { diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt index a8aa63c8..0ce5f11c 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/client/SshConnection.kt @@ -117,6 +117,7 @@ import org.connectbot.sshlib.protocol.SshMsgPing import org.connectbot.sshlib.protocol.SshMsgPong import org.connectbot.sshlib.protocol.SshMsgServiceAccept import org.connectbot.sshlib.protocol.SshMsgServiceRequest +import org.connectbot.sshlib.protocol.SshMsgUnimplemented import org.connectbot.sshlib.protocol.SshMsgUserauthBanner import org.connectbot.sshlib.protocol.SshMsgUserauthFailure import org.connectbot.sshlib.protocol.SshMsgUserauthInfoRequest @@ -2341,7 +2342,7 @@ class SshConnection( * This is the central packet processing loop that converts packets to events. */ private inner class InboundPacketController { - private val packetsReceivedDuringRekey = ArrayDeque() + private val packetsReceivedDuringRekey = ArrayDeque() private fun requireAccepted(accepted: Boolean, messageType: Any) { if (!accepted) { @@ -2353,23 +2354,26 @@ class SshConnection( val queuedPacket = withContext(stateMachineDispatcher) { if (stateMachine.isKexInProgress()) null else packetsReceivedDuringRekey.removeFirstOrNull() } - val packet = queuedPacket ?: packetIO.readPacket() + val receivedPacket = queuedPacket ?: packetIO.readPacketWithSequence() + val packet = receivedPacket.payload + val packetSequenceNumber = receivedPacket.sequenceNumber + val messageNumber = receivedPacket.messageNumber val msgType = packet.messageType() logger.debug("Received packet: $msgType") withContext(stateMachineDispatcher) { - if (!isKeyExchangeMessage(msgType.id().toInt())) { + if (!isKeyExchangeMessage(messageNumber)) { val description = "Non-KEX packet $msgType is forbidden during strict initial key exchange" if (!stateMachine.authorizeNonKexPacket(description)) { throw ProtocolViolationException(description, responseSent = true) } } - if (isRekeying && stateMachine.isKexInProgress() && msgType.id().toInt() >= SSH_MSG_USERAUTH_REQUEST_ID) { + if (isRekeying && stateMachine.isKexInProgress() && messageNumber >= SSH_MSG_USERAUTH_REQUEST_ID) { if (packetsReceivedDuringRekey.size >= MAX_REKEY_IN_FLIGHT_PACKETS) { throw ProtocolViolationException("Too many higher-layer packets received during key exchange") } - packetsReceivedDuringRekey.addLast(packet) + packetsReceivedDuringRekey.addLast(receivedPacket) return@withContext } @@ -2410,6 +2414,10 @@ class SshConnection( requireAccepted(stateMachine.receiveDebug(packet.body() as SshMsgDebug), msgType) } + SshEnums.MessageType.SSH_MSG_UNIMPLEMENTED -> { + logger.debug("Peer reported packet ${parseBody(packet).packetSequence()} as unimplemented") + } + SshEnums.MessageType.SSH_MSG_GLOBAL_REQUEST -> { try { val rawBody = packet._raw_body() @@ -2723,8 +2731,8 @@ class SshConnection( // KEX-specific messages 30-49 are not in MessageType enum. // Disambiguate by negotiated KEX type since ECDH reply, DH reply, // and DH-GEX group all share message ID 31. - val msgId = msgType.id().toInt() - val rawBody = byteArrayOf(msgType.id().toByte()) + packet._raw_body() + val msgId = messageNumber + val rawBody = byteArrayOf(messageNumber.toByte()) + packet._raw_body() val kexEntry = negotiatedKex?.let { KexEntry.fromSshName(it) } when { kexEntry?.type == KexType.ECDH && @@ -2766,11 +2774,17 @@ class SshConnection( else -> { if (msgId in 30..49) { - throw ProtocolViolationException( - "Unexpected key-exchange packet ${packet.messageType()} for negotiated algorithm $negotiatedKex", - ) + val description = + "Unexpected key-exchange packet ${packet.messageType()} for negotiated algorithm $negotiatedKex" + if (stateMachine.isStrictKexEnabled() && !isRekeying) { + throw ProtocolViolationException(description) + } + logger.debug("$description; sending SSH_MSG_UNIMPLEMENTED") + sendUnimplemented(packetSequenceNumber) + } else { + logger.debug("Sending SSH_MSG_UNIMPLEMENTED for packet ${packet.messageType()}") + sendUnimplemented(packetSequenceNumber) } - logger.warn("Unhandled message type: ${packet.messageType()}") } } } @@ -2885,6 +2899,17 @@ class SshConnection( ) } + private suspend fun sendUnimplemented(packetSequenceNumber: Long) { + val msg = SshMsgUnimplemented().apply { + setPacketSequence(packetSequenceNumber and 0xffff_ffffL) + _check() + } + writePacket( + SshEnums.MessageType.SSH_MSG_UNIMPLEMENTED.id().toInt(), + msg.toByteArray(), + ) + } + private fun startPacketLoop() { if (packetLoopJob != null) return packetLoopJob = connectionScope.launch { diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachine.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachine.kt index fe7e3241..81e8e954 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachine.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshClientStateMachine.kt @@ -392,6 +392,8 @@ internal class SshClientStateMachine( origins = parsedPacket, effects = setOf( SshEffect.RECEIVE_KEX_DH_REPLY, + SshEffect.VERIFY_HOST_KEY_POSSESSION, + SshEffect.VERIFY_KEX_TRANSCRIPT, SshEffect.SEND_NEW_KEYS, SshEffect.ACTIVATE_OUTBOUND_PROTECTION, SshEffect.RESET_OUTBOUND_SEQUENCE, @@ -406,6 +408,8 @@ internal class SshClientStateMachine( origins = parsedPacket, effects = setOf( SshEffect.RECEIVE_KEX_ECDH_REPLY, + SshEffect.VERIFY_HOST_KEY_POSSESSION, + SshEffect.VERIFY_KEX_TRANSCRIPT, SshEffect.SEND_NEW_KEYS, SshEffect.ACTIVATE_OUTBOUND_PROTECTION, SshEffect.RESET_OUTBOUND_SEQUENCE, @@ -446,6 +450,8 @@ internal class SshClientStateMachine( origins = parsedPacket, effects = setOf( SshEffect.RECEIVE_KEX_DH_GEX_REPLY, + SshEffect.VERIFY_HOST_KEY_POSSESSION, + SshEffect.VERIFY_KEX_TRANSCRIPT, SshEffect.SEND_NEW_KEYS, SshEffect.ACTIVATE_OUTBOUND_PROTECTION, SshEffect.RESET_OUTBOUND_SEQUENCE, diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshStateMachineFormalModel.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshStateMachineFormalModel.kt index 1becab45..af47691d 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshStateMachineFormalModel.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/protocol/SshStateMachineFormalModel.kt @@ -121,9 +121,45 @@ internal enum class SshEffect { SEND_NEW_KEYS, SEND_SERVICE_REQUEST, SEND_PROTOCOL_ERROR, + SEND_UNIMPLEMENTED, SEND_USERAUTH_REQUEST, SEND_VERSION, START_AUTHENTICATION, + VERIFY_HOST_KEY_POSSESSION, + VERIFY_KEX_TRANSCRIPT, +} + +/** + * Lifecycle-relevant packet classes used by the hostile-environment model. + * + * These deliberately abstract packets that have identical authorization and + * state-machine behavior. Client-only classes are included so TLC can check + * that receiving a syntactically valid packet never changes the endpoint's + * role. + */ +internal enum class SshPacketClass { + KEX_INIT, + KEX_REPLY, + KEX_GEX_GROUP, + NEW_KEYS, + SERVICE_ACCEPT, + USERAUTH_SUCCESS, + USERAUTH_FAILURE, + USERAUTH_METHOD_SPECIFIC, + USERAUTH_BANNER, + EXT_INFO, + CONNECTION_PACKET, + CHANNEL_OPEN_REPLY, + CHANNEL_REQUEST_REPLY, + GLOBAL_REQUEST, + DEBUG, + IGNORE, + DISCONNECT, + CLIENT_KEX_INIT, + CLIENT_SERVICE_REQUEST, + CLIENT_USERAUTH_REQUEST, + CLIENT_CONNECTION_PACKET, + UNKNOWN, } internal enum class SshBooleanFact( @@ -296,7 +332,7 @@ internal data class SshStateMachineFormalModel( val body = buildString { appendLine("EXTENDS Naturals") appendLine() - appendLine("CONSTANT MaxChannels") + appendLine("CONSTANTS MaxChannels, EnableHostileEnvironment, AdversaryOwnsHostKey, EnforceKexProofVerification") appendLine() appendLine("ChannelIDs == 1..MaxChannels") appendLine("ChannelAttemptIDs == 0..(MaxChannels + 1)") @@ -308,9 +344,14 @@ internal data class SshStateMachineFormalModel( appendLine("States == ${renderSet(leafStateNames)}") appendLine("PostAuthenticatedStates == ${renderSet(descendantLeaves(POST_AUTHENTICATED_STATE))}") appendLine("KexStates == ${renderSet(KEX_STATE_NAMES)}") - appendLine("Events == ${renderSet(transitions.mapTo(sortedSetOf()) { it.meta.eventName })}") + val eventNames = transitions.mapTo(sortedSetOf()) { it.meta.eventName }.apply { + add("HostilePacketRejected") + } + appendLine("Events == ${renderSet(eventNames)}") appendLine("Origins == ${renderSet(SshEventOrigin.entries.mapTo(sortedSetOf()) { it.tlaName })}") appendLine("Effects == ${renderSet(SshEffect.entries.mapTo(sortedSetOf()) { it.tlaName })}") + appendLine("PacketClasses == ${renderSet(SshPacketClass.entries.mapTo(sortedSetOf()) { it.tlaName })}") + appendLine("PacketDispositions == {\"None\", \"Client\", \"Accepted\", \"Unimplemented\", \"Disconnected\"}") appendChannelDefinitions() appendLine() appendLine("Init ==") @@ -322,11 +363,20 @@ internal data class SshStateMachineFormalModel( appendTransition(transition, variables) appendLine() } - appendLine("Next ==") + appendPacketTransitionEnabled() + appendLine() + appendRejectHostilePacket(variables) + appendLine() + appendHostileEnvironmentNext(variables) + appendLine() + appendLine("ClientNext ==") transitions.sortedBy { it.meta.id.name }.forEach { transition -> appendLine(" \\/ ${transition.meta.id.name}") } appendLine(" \\/ AttemptChannelOperation") + appendLine(" \\/ RejectHostilePacket") + appendLine() + appendLine("Next == ClientNext \\/ HostileEnvironmentNext") appendLine() appendLine("Spec == Init /\\ [][Next]_vars") } @@ -355,6 +405,19 @@ internal data class SshStateMachineFormalModel( if (meta.guard != SshFormalGuard.Always) { appendLine(" /\\ ${meta.guard.renderTla()}") } + val packets = packetClasses(meta) + if (packets.isNotEmpty()) { + appendLine(" /\\ (inboundPacket = \"None\"") + appendLine(" \\/ /\\ inboundPacket \\in ${renderSet(packets.map { it.tlaName })}") + packetSecurityGuards(meta).forEach { guard -> + appendLine(" /\\ $guard") + } + appendLine(" )") + } + if (meta.id in NEW_KEYS_TRANSITIONS) { + appendLine(" /\\ (~EnforceKexProofVerification \\/ hostKeyPossessionVerified)") + appendLine(" /\\ (~EnforceKexProofVerification \\/ transcriptVerified)") + } variables.forEach { variable -> appendLine(" /\\ ${variable.renderNext(meta)}") } @@ -387,6 +450,31 @@ internal data class SshStateMachineFormalModel( variable("initialNewKeysActive", "FALSE", ::renderInitialNewKeysActiveUpdate), variable("authRequestPending", "FALSE", ::renderAuthRequestPendingUpdate), variable("previousAuthRequestPending", "FALSE") { "authRequestPending" }, + FormalVariable("inboundPacket", quote("None")) { meta -> + if (packetClasses(meta).isEmpty()) "inboundPacket' = inboundPacket" else "inboundPacket' = \"None\"" + }, + FormalVariable("lastInboundPacket", quote("None")) { meta -> + if (packetClasses(meta).isEmpty()) "lastInboundPacket' = lastInboundPacket" else "lastInboundPacket' = inboundPacket" + }, + FormalVariable("inboundTranscriptMatches", "FALSE") { meta -> + "inboundTranscriptMatches' = inboundTranscriptMatches" + }, + FormalVariable("inboundHostSignatureValid", "FALSE") { meta -> + "inboundHostSignatureValid' = inboundHostSignatureValid" + }, + FormalVariable("inboundTransportValid", "FALSE") { meta -> + "inboundTransportValid' = inboundTransportValid" + }, + variable("hostKeyPossessionVerified", "FALSE", ::renderHostKeyPossessionVerifiedUpdate), + variable("transcriptVerified", "FALSE", ::renderTranscriptVerifiedUpdate), + variable("transportKeysVerified", "FALSE", ::renderTransportKeysVerifiedUpdate), + FormalVariable("lastPacketDisposition", quote("None")) { meta -> + if (packetClasses(meta).isEmpty()) { + "lastPacketDisposition' = \"Client\"" + } else { + "lastPacketDisposition' = IF inboundPacket = \"None\" THEN \"Client\" ELSE \"Accepted\"" + } + }, variable("previousChannels", "[c \\in ChannelIDs |-> \"Unallocated\"]") { "channels" }, FormalVariable("activeChannel", "0") { meta -> val operation = meta.channelOperationEvent @@ -556,6 +644,189 @@ internal data class SshStateMachineFormalModel( else -> "authRequestPending" } + private fun renderHostKeyPossessionVerifiedUpdate(meta: SshFormalTransitionMeta): String = when { + meta.id in KEX_INIT_TRANSITIONS -> "FALSE" + meta.id in KEX_REPLY_TRANSITIONS -> "TRUE" + SshEffect.DISCONNECT in meta.effects -> "FALSE" + else -> "hostKeyPossessionVerified" + } + + private fun renderTranscriptVerifiedUpdate(meta: SshFormalTransitionMeta): String = when { + meta.id in KEX_INIT_TRANSITIONS -> "FALSE" + meta.id in KEX_REPLY_TRANSITIONS -> "TRUE" + SshEffect.DISCONNECT in meta.effects -> "FALSE" + else -> "transcriptVerified" + } + + private fun renderTransportKeysVerifiedUpdate(meta: SshFormalTransitionMeta): String = when { + meta.id in NEW_KEYS_TRANSITIONS -> "TRUE" + SshEffect.DISCONNECT in meta.effects -> "FALSE" + else -> "transportKeysVerified" + } + + private fun packetClasses(meta: SshFormalTransitionMeta): Set = when (meta.id) { + SshTransitionId.RECEIVE_INITIAL_STRICT_KEX_INIT, + SshTransitionId.RECEIVE_INITIAL_NON_STRICT_KEX_INIT, + SshTransitionId.RECEIVE_REKEY_KEX_INIT, + SshTransitionId.REJECT_STRICT_KEX_INIT_NOT_FIRST, + SshTransitionId.UNEXPECTED_KEX_INIT_WAIT_KEX, + SshTransitionId.UNEXPECTED_KEX_INIT_WAIT_KEX_DH_GEX_INIT, + SshTransitionId.UNEXPECTED_KEX_INIT_WAIT_NEW_KEYS, + -> setOf(SshPacketClass.KEX_INIT) + + SshTransitionId.RECEIVE_KEX_DH_REPLY, + SshTransitionId.RECEIVE_KEX_ECDH_REPLY, + SshTransitionId.RECEIVE_KEX_DH_GEX_REPLY, + -> setOf(SshPacketClass.KEX_REPLY) + + SshTransitionId.RECEIVE_KEX_DH_GEX_GROUP -> setOf(SshPacketClass.KEX_GEX_GROUP) + + SshTransitionId.RECEIVE_INITIAL_NEW_KEYS, + SshTransitionId.RECEIVE_REKEY_NEW_KEYS, + -> setOf(SshPacketClass.NEW_KEYS) + + SshTransitionId.RECEIVE_SERVICE_ACCEPT -> setOf(SshPacketClass.SERVICE_ACCEPT) + + SshTransitionId.AUTHENTICATION_SUCCESS -> setOf(SshPacketClass.USERAUTH_SUCCESS) + + SshTransitionId.AUTHENTICATION_FAILURE -> setOf(SshPacketClass.USERAUTH_FAILURE) + + SshTransitionId.RECEIVE_USERAUTH_INFO_REQUEST, + SshTransitionId.AUTHORIZE_AUTHENTICATION_PACKET, + -> setOf(SshPacketClass.USERAUTH_METHOD_SPECIFIC) + + SshTransitionId.RECEIVE_USERAUTH_BANNER_READY, + SshTransitionId.RECEIVE_USERAUTH_BANNER_AUTHENTICATING, + -> setOf(SshPacketClass.USERAUTH_BANNER) + + SshTransitionId.AUTHORIZE_SERVICE_EXT_INFO, + SshTransitionId.AUTHORIZE_POST_AUTH_EXT_INFO, + -> setOf(SshPacketClass.EXT_INFO) + + SshTransitionId.AUTHORIZE_CONNECTION_PACKET -> setOf(SshPacketClass.CONNECTION_PACKET) + + SshTransitionId.AUTHORIZE_AUTHENTICATED_PACKET -> setOf( + SshPacketClass.CONNECTION_PACKET, + SshPacketClass.CLIENT_CONNECTION_PACKET, + ) + + SshTransitionId.RECEIVE_GLOBAL_REQUEST -> setOf(SshPacketClass.GLOBAL_REQUEST) + + SshTransitionId.RECEIVE_CHANNEL_OPEN_CONFIRMATION, + SshTransitionId.RECEIVE_CHANNEL_OPEN_FAILURE, + -> setOf(SshPacketClass.CHANNEL_OPEN_REPLY) + + SshTransitionId.RECEIVE_CHANNEL_SUCCESS, + SshTransitionId.RECEIVE_CHANNEL_FAILURE, + -> setOf(SshPacketClass.CHANNEL_REQUEST_REPLY) + + SshTransitionId.RECEIVE_DEBUG -> setOf(SshPacketClass.DEBUG) + + SshTransitionId.RECEIVE_IGNORE -> setOf(SshPacketClass.IGNORE) + + SshTransitionId.DISCONNECT -> setOf(SshPacketClass.DISCONNECT) + + else -> emptySet() + } + + private fun packetSecurityGuards(meta: SshFormalTransitionMeta): List { + val packets = packetClasses(meta) + if (packets.isEmpty()) return emptyList() + return when { + meta.id in KEX_REPLY_TRANSITIONS -> listOf( + "(~EnforceKexProofVerification \\/ inboundHostSignatureValid)", + "(~EnforceKexProofVerification \\/ inboundTranscriptMatches)", + "(~initialNewKeysActive \\/ inboundTransportValid)", + ) + + packets.any { it in PRE_NEW_KEYS_PACKET_CLASSES } -> + listOf("(~initialNewKeysActive \\/ inboundTransportValid)") + + else -> listOf("inboundTransportValid") + } + } + + private fun StringBuilder.appendPacketTransitionEnabled() { + appendLine("PacketTransitionEnabled ==") + transitions + .filter { packetClasses(it.meta).isNotEmpty() } + .sortedBy { it.meta.id.name } + .forEach { transition -> + val meta = transition.meta + appendLine(" \\/ /\\ state \\in ${renderSet(transition.sourceStateNames)}") + appendLine(" /\\ inboundPacket \\in ${renderSet(packetClasses(meta).map { it.tlaName })}") + if (meta.guard != SshFormalGuard.Always) { + appendLine(" /\\ ${meta.guard.renderTla()}") + } + packetSecurityGuards(meta).forEach { appendLine(" /\\ $it") } + if (meta.id in NEW_KEYS_TRANSITIONS) { + appendLine(" /\\ (~EnforceKexProofVerification \\/ hostKeyPossessionVerified)") + appendLine(" /\\ (~EnforceKexProofVerification \\/ transcriptVerified)") + } + } + } + + private fun StringBuilder.appendRejectHostilePacket(variables: List) { + appendLine("HostilePacketFatal ==") + appendLine(" \\/ /\\ strictKex /\\ ~rekeying /\\ state \\in KexStates") + appendLine(" /\\ ~PacketTransitionEnabled") + appendLine(" \\/ /\\ inboundPacket = \"KexInit\"") + appendLine(" /\\ state \\in {\"WaitKex\", \"WaitKexDhGexInit\", \"WaitNewKeys\"}") + appendLine(" \\/ /\\ inboundPacket = \"KexReply\"") + appendLine(" /\\ (~inboundHostSignatureValid \\/ ~inboundTranscriptMatches)") + appendLine(" \\/ /\\ initialNewKeysActive /\\ ~inboundTransportValid") + appendLine() + appendLine("RejectHostilePacket ==") + appendLine(" /\\ inboundPacket # \"None\"") + appendLine(" /\\ ~PacketTransitionEnabled") + variables.forEach { variable -> + appendLine(" /\\ ${renderRejectedPacketUpdate(variable.name)}") + } + } + + private fun renderRejectedPacketUpdate(name: String): String = when (name) { + "state" -> "state' = IF HostilePacketFatal THEN \"Disconnected\" ELSE state" + "previousState" -> "previousState' = state" + "event" -> "event' = \"HostilePacketRejected\"" + "origin" -> "origin' = \"ParsedPacket\"" + "packetWasParsed" -> "packetWasParsed' = TRUE" + "effects" -> "effects' = IF HostilePacketFatal THEN {\"Disconnect\", \"SendProtocolError\"} ELSE {\"SendUnimplemented\"}" + "rekeying" -> "rekeying' = IF HostilePacketFatal THEN FALSE ELSE rekeying" + "authenticationEstablished" -> "authenticationEstablished' = authenticationEstablished" + "authRequestPending" -> "authRequestPending' = IF HostilePacketFatal THEN FALSE ELSE authRequestPending" + "previousAuthRequestPending" -> "previousAuthRequestPending' = authRequestPending" + "inboundPacket" -> "inboundPacket' = \"None\"" + "lastInboundPacket" -> "lastInboundPacket' = inboundPacket" + "inboundTranscriptMatches" -> "inboundTranscriptMatches' = inboundTranscriptMatches" + "inboundHostSignatureValid" -> "inboundHostSignatureValid' = inboundHostSignatureValid" + "inboundTransportValid" -> "inboundTransportValid' = inboundTransportValid" + "hostKeyPossessionVerified" -> "hostKeyPossessionVerified' = IF HostilePacketFatal THEN FALSE ELSE hostKeyPossessionVerified" + "transcriptVerified" -> "transcriptVerified' = IF HostilePacketFatal THEN FALSE ELSE transcriptVerified" + "transportKeysVerified" -> "transportKeysVerified' = IF HostilePacketFatal THEN FALSE ELSE transportKeysVerified" + "lastPacketDisposition" -> "lastPacketDisposition' = IF HostilePacketFatal THEN \"Disconnected\" ELSE \"Unimplemented\"" + "previousChannels" -> "previousChannels' = channels" + "activeChannel" -> "activeChannel' = 0" + "channelEvent" -> "channelEvent' = \"None\"" + "channelOrigin" -> "channelOrigin' = \"None\"" + "channels" -> "channels' = IF HostilePacketFatal THEN [c \\in ChannelIDs |-> IF channels[c] = \"Unallocated\" THEN \"Unallocated\" ELSE \"CLOSED\"] ELSE channels" + "channelEffects" -> "channelEffects' = {}" + else -> "$name' = $name" + } + + private fun StringBuilder.appendHostileEnvironmentNext(variables: List) { + appendLine("HostileEnvironmentNext ==") + appendLine(" /\\ EnableHostileEnvironment") + appendLine(" /\\ inboundPacket = \"None\"") + appendLine(" /\\ inboundPacket' \\in PacketClasses") + appendLine(" /\\ inboundTranscriptMatches' \\in BOOLEAN") + appendLine(" /\\ inboundHostSignatureValid' \\in BOOLEAN") + appendLine(" /\\ (inboundHostSignatureValid' => AdversaryOwnsHostKey)") + appendLine(" /\\ inboundTransportValid' \\in BOOLEAN") + appendLine(" /\\ (inboundTransportValid' => AdversaryOwnsHostKey /\\ transportKeysVerified)") + val unchanged = variables.map(FormalVariable::name).filterNot { it in HOSTILE_PACKET_VARIABLE_NAMES } + appendLine(" /\\ UNCHANGED <<${unchanged.joinToString()}>>") + } + private fun initialPostAuthenticatedState() = resolveInitialLeaf(POST_AUTHENTICATED_STATE) private fun resolveInitialLeaf(stateName: String): String { @@ -598,6 +869,35 @@ internal data class SshStateMachineFormalModel( SshEffect.RESET_INBOUND_SEQUENCE, SshEffect.RESET_OUTBOUND_SEQUENCE, ) + private val KEX_INIT_TRANSITIONS = setOf( + SshTransitionId.RECEIVE_INITIAL_STRICT_KEX_INIT, + SshTransitionId.RECEIVE_INITIAL_NON_STRICT_KEX_INIT, + SshTransitionId.RECEIVE_REKEY_KEX_INIT, + ) + private val KEX_REPLY_TRANSITIONS = setOf( + SshTransitionId.RECEIVE_KEX_DH_REPLY, + SshTransitionId.RECEIVE_KEX_ECDH_REPLY, + SshTransitionId.RECEIVE_KEX_DH_GEX_REPLY, + ) + private val NEW_KEYS_TRANSITIONS = setOf( + SshTransitionId.RECEIVE_INITIAL_NEW_KEYS, + SshTransitionId.RECEIVE_REKEY_NEW_KEYS, + ) + private val PRE_NEW_KEYS_PACKET_CLASSES = setOf( + SshPacketClass.KEX_INIT, + SshPacketClass.KEX_REPLY, + SshPacketClass.KEX_GEX_GROUP, + SshPacketClass.NEW_KEYS, + SshPacketClass.DEBUG, + SshPacketClass.IGNORE, + SshPacketClass.DISCONNECT, + ) + private val HOSTILE_PACKET_VARIABLE_NAMES = setOf( + "inboundPacket", + "inboundTranscriptMatches", + "inboundHostSignatureValid", + "inboundTransportValid", + ) private val CHANNEL_VARIABLE_NAMES = setOf( "channels", "previousChannels", @@ -609,6 +909,9 @@ internal data class SshStateMachineFormalModel( } } +private val SshPacketClass.tlaName: String + get() = name.lowercase().split('_').joinToString("") { it.replaceFirstChar(Char::uppercase) } + private val SshChannelEventOrigin.tlaName: String get() = when (this) { SshChannelEventOrigin.CONNECTION_CONTROL -> "ConnectionControl" diff --git a/sshlib/src/main/kotlin/org/connectbot/sshlib/transport/PacketIO.kt b/sshlib/src/main/kotlin/org/connectbot/sshlib/transport/PacketIO.kt index 235f26f1..05d0901c 100644 --- a/sshlib/src/main/kotlin/org/connectbot/sshlib/transport/PacketIO.kt +++ b/sshlib/src/main/kotlin/org/connectbot/sshlib/transport/PacketIO.kt @@ -49,6 +49,11 @@ internal class PacketIO( private val transport: Transport, private val secureRandom: SecureRandom = SecureRandom(), ) { + internal data class ReceivedPacket( + val payload: UnencryptedPacket.UnencryptedPayload, + val sequenceNumber: Long, + val messageNumber: Int, + ) companion object { private val logger = LoggerFactory.getLogger(PacketIO::class.java) @@ -230,7 +235,11 @@ internal class PacketIO( * @return Parsed SSH message payload * @throws TransportException if packet is malformed or transport fails */ - suspend fun readPacket(): UnencryptedPacket.UnencryptedPayload { + suspend fun readPacket(): UnencryptedPacket.UnencryptedPayload = readPacketWithSequence().payload + + /** Read a packet together with the uint32 sequence number that authenticated it. */ + suspend fun readPacketWithSequence(): ReceivedPacket { + val sequenceNumber = receiveSequenceNumber val rawPayloadBytes = readRawPayloadBytes() val compressor = receiveCompressor @@ -240,7 +249,11 @@ internal class PacketIO( rawPayloadBytes } - return parsePayloadBytes(payloadBytes) + return ReceivedPacket( + payload = parsePayloadBytes(payloadBytes), + sequenceNumber = sequenceNumber, + messageNumber = payloadBytes.first().toInt() and 0xff, + ) } /** diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/FakeSshServer.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/FakeSshServer.kt index 3534a680..53ea115a 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/FakeSshServer.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/FakeSshServer.kt @@ -52,6 +52,8 @@ import org.connectbot.sshlib.protocol.SshMsgKexinit import org.connectbot.sshlib.protocol.SshMsgPing import org.connectbot.sshlib.protocol.SshMsgPong import org.connectbot.sshlib.protocol.SshMsgServiceAccept +import org.connectbot.sshlib.protocol.SshMsgServiceRequest +import org.connectbot.sshlib.protocol.SshMsgUnimplemented import org.connectbot.sshlib.protocol.SshMsgUserauthBanner import org.connectbot.sshlib.protocol.SshMsgUserauthFailure import org.connectbot.sshlib.protocol.SshMsgUserauthInfoRequest @@ -114,6 +116,7 @@ class FakeSshServer( private val receivedChannelOpenConfirmations = Channel(Channel.UNLIMITED) private val receivedChannelOpenFailures = Channel(Channel.UNLIMITED) private val receivedChannelData = Channel(Channel.UNLIMITED) + private val receivedUnimplemented = Channel(Channel.UNLIMITED) fun start(ignoreTransportErrors: Boolean = false) { scope.launch(coroutineContext) { @@ -284,6 +287,13 @@ class FakeSshServer( receivedPongs.trySend(pongMsg.data().data()) } + SshEnums.MessageType.SSH_MSG_UNIMPLEMENTED -> { + val bodyBytes = rawBytes.copyOfRange(1, rawBytes.size) + val unimplemented = SshMsgUnimplemented(ByteBufferKaitaiStream(bodyBytes)) + unimplemented._read() + receivedUnimplemented.trySend(unimplemented) + } + else -> { /* ignore */ } } false @@ -628,6 +638,24 @@ class FakeSshServer( } } + suspend fun sendUnexpectedServiceRequest(service: String = "ssh-userauth") { + val request = SshMsgServiceRequest().apply { + setServiceName(createAsciiString(service)) + _check() + } + writeMutex.withLock { + serverIo.writePacket(SshEnums.MessageType.SSH_MSG_SERVICE_REQUEST.id().toInt(), request.toByteArray()) + } + } + + suspend fun sendUnknownPacket(messageNumber: Int = 191) { + writeMutex.withLock { + serverIo.writePacket(messageNumber, byteArrayOf()) + } + } + + suspend fun awaitUnimplemented(): SshMsgUnimplemented = receivedUnimplemented.receive() + suspend fun sendUserauthBanner(message: String) { val banner = SshMsgUserauthBanner() val utf8 = createUtf8String(message) diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt index 89430229..00c22f9f 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionFlowTest.kt @@ -75,6 +75,23 @@ class SshConnectionFlowTest { } } + @Test + fun `wrong direction packet receives unimplemented without advancing state`() = runTest { + connectedFixture { connection, server, dispatcher -> + server.sendUnknownPacket() + val unknownReply = withTimeout(5_000) { server.awaitUnimplemented() } + + server.sendUnexpectedServiceRequest() + val wrongDirectionReply = withTimeout(5_000) { server.awaitUnimplemented() } + assertEquals(unknownReply.packetSequence() + 1, wrongDirectionReply.packetSequence()) + + val authentication = async(dispatcher) { connection.authenticatePassword("user", "pass") } + withTimeout(5_000) { server.awaitUserauthRequest() } + server.sendUserauthSuccess() + assertEquals(AuthResult.Success, withTimeout(5_000) { authentication.await() }) + } + } + @Test fun `duplicate kex init during rekey is a fatal protocol error`() = runTest { connectedFixture { connection, server, dispatcher -> diff --git a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt index 24579fe5..242e0537 100644 --- a/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt +++ b/sshlib/src/test/kotlin/org/connectbot/sshlib/protocol/SshStateMachineTlaGenerator.kt @@ -249,6 +249,21 @@ class SshStateMachineFormalModelTest { assertTrue("PROPERTY StrictKexIsSticky" in config) } + @Test + fun `generated model composes client and hostile environment actions`() { + val rendered = createFormalModel().renderTla() + + assertTrue("PacketClasses ==" in rendered) + assertTrue("PacketTransitionEnabled ==" in rendered) + assertTrue("HostileEnvironmentNext ==" in rendered) + assertTrue("RejectHostilePacket ==" in rendered) + assertTrue("ClientNext ==" in rendered) + assertTrue("Next == ClientNext \\/ HostileEnvironmentNext" in rendered) + assertTrue("hostKeyPossessionVerified" in rendered) + assertTrue("transcriptVerified" in rendered) + assertTrue("transportKeysVerified" in rendered) + } + @Test fun `checked in TLA model matches KStateMachine declaration`() { val expected = Files.readString(Path.of("src/test/resources/tla/SshClientStateMachineGenerated.tla")) diff --git a/sshlib/src/test/resources/tla/SshClientStateMachine.cfg b/sshlib/src/test/resources/tla/SshClientStateMachine.cfg index 9adfa49f..508a6bd7 100644 --- a/sshlib/src/test/resources/tla/SshClientStateMachine.cfg +++ b/sshlib/src/test/resources/tla/SshClientStateMachine.cfg @@ -1,6 +1,9 @@ SPECIFICATION Spec CONSTANT MaxChannels = 2 +CONSTANT EnableHostileEnvironment = FALSE +CONSTANT AdversaryOwnsHostKey = FALSE +CONSTANT EnforceKexProofVerification = TRUE VIEW ModelView @@ -33,6 +36,12 @@ INVARIANT StrictKexInitMustBeFirst INVARIANT AcceptedInitialKexPacketOrderClearsHistory INVARIANT UserAuthenticationRequiresInitialNewKeys INVARIANT UnexpectedKexInitIsFatal +INVARIANT HostileKexReplyRequiresPossessionProof +INVARIANT NewKeysRequiresVerifiedTranscript +INVARIANT ProtectedHostilePacketsRequireTransportAuthentication +INVARIANT AuthenticationRequiresVerifiedTransport +INVARIANT HostileClientRolePacketsNeverAdvance +INVARIANT RejectedHostilePacketsDoNotEstablishSecurity PROPERTY AuthenticationNeverDowngrades PROPERTY DisconnectedIsTerminal diff --git a/sshlib/src/test/resources/tla/SshClientStateMachine.tla b/sshlib/src/test/resources/tla/SshClientStateMachine.tla index c42c96d1..bc413adb 100644 --- a/sshlib/src/test/resources/tla/SshClientStateMachine.tla +++ b/sshlib/src/test/resources/tla/SshClientStateMachine.tla @@ -50,6 +50,18 @@ TypeOK == /\ initialNewKeysActive \in BOOLEAN /\ authRequestPending \in BOOLEAN /\ previousAuthRequestPending \in BOOLEAN + /\ EnableHostileEnvironment \in BOOLEAN + /\ AdversaryOwnsHostKey \in BOOLEAN + /\ EnforceKexProofVerification \in BOOLEAN + /\ inboundPacket \in PacketClasses \cup {"None"} + /\ lastInboundPacket \in PacketClasses \cup {"None"} + /\ inboundTranscriptMatches \in BOOLEAN + /\ inboundHostSignatureValid \in BOOLEAN + /\ inboundTransportValid \in BOOLEAN + /\ hostKeyPossessionVerified \in BOOLEAN + /\ transcriptVerified \in BOOLEAN + /\ transportKeysVerified \in BOOLEAN + /\ lastPacketDisposition \in PacketDispositions /\ MaxChannels \in Nat \ {0} /\ channels \in [ChannelIDs -> ChannelStates] /\ previousChannels \in [ChannelIDs -> ChannelStates] @@ -131,6 +143,15 @@ ModelView == initialNewKeysActive, authRequestPending, previousAuthRequestPending, + inboundPacket, + lastInboundPacket, + inboundTranscriptMatches, + inboundHostSignatureValid, + inboundTransportValid, + hostKeyPossessionVerified, + transcriptVerified, + transportKeysVerified, + lastPacketDisposition, channels, NoInvalidChannelSideEffects, ChannelIsolation>> @@ -263,4 +284,57 @@ UnexpectedKexInitIsFatal == /\ "SendProtocolError" \in effects /\ "Disconnect" \in effects +HostileKexReplyRequiresPossessionProof == + inboundPacket = "None" /\ lastPacketDisposition = "Accepted" /\ + event \in {"ReceiveKex.DhReply", "ReceiveKex.EcdhReply", "ReceiveKex.DhGexReply"} => + /\ inboundHostSignatureValid + /\ inboundTranscriptMatches + /\ hostKeyPossessionVerified + /\ transcriptVerified + +NewKeysRequiresVerifiedTranscript == + event = "ReceiveNewKeys" => + /\ hostKeyPossessionVerified + /\ transcriptVerified + /\ transportKeysVerified + +ProtectedHostilePacketsRequireTransportAuthentication == + inboundPacket = "None" /\ lastPacketDisposition = "Accepted" /\ + event \in { + "ReceiveServiceAccept", + "AuthenticationSuccess", + "AuthenticationFailure", + "AuthorizeAuthenticationPacket", + "AuthorizeAuthenticatedPacket", + "AuthorizeConnectionPacket", + "AuthorizeExtInfo", + "ReceiveGlobalRequest", + "ReceiveChannelOpenConfirmation", + "ReceiveChannelOpenFailure", + "ReceiveChannelSuccess", + "ReceiveChannelFailure" + } => inboundTransportValid + +AuthenticationRequiresVerifiedTransport == + authenticationEstablished /\ state # "Disconnected" => transportKeysVerified + +HostileClientRolePacketsNeverAdvance == + inboundPacket = "None" /\ lastPacketDisposition = "Accepted" => + lastInboundPacket \notin { + "ClientKexInit", + "ClientServiceRequest", + "ClientUserauthRequest" + } + +RejectedHostilePacketsDoNotEstablishSecurity == + inboundPacket = "None" /\ lastPacketDisposition \in {"Unimplemented", "Disconnected"} => + /\ event = "HostilePacketRejected" + /\ (lastPacketDisposition = "Unimplemented" => + /\ state = previousState + /\ effects = {"SendUnimplemented"}) + +\* Hostile profiles focus on connection-level packet ordering. The baseline +\* configuration separately explores the full two-channel product state. +HostileSecurityActionConstraint == channelEvent' = "None" + ==== diff --git a/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla b/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla index 3222634a..5aa5ea90 100644 --- a/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla +++ b/sshlib/src/test/resources/tla/SshClientStateMachineGenerated.tla @@ -1,25 +1,27 @@ ---- MODULE SshClientStateMachineGenerated ---- \* Generated from SshClientStateMachine. Do not edit. -\* Model SHA-256: a34440960298ca1cd17a21377130492c5d394fe258e172479153503aaf3b61c0 +\* Model SHA-256: 51a83d84a0f081b32e4dfcf4d185ef2c83fec2c9a640b385db78f35607733b78 \* Lifecycle states: 11; transitions: 43. \* TLC distinct states count full variable valuations, not lifecycle nodes. EXTENDS Naturals -CONSTANT MaxChannels +CONSTANTS MaxChannels, EnableHostileEnvironment, AdversaryOwnsHostKey, EnforceKexProofVerification ChannelIDs == 1..MaxChannels ChannelAttemptIDs == 0..(MaxChannels + 1) -VARIABLES state, previousState, history, event, origin, packetWasParsed, effects, rekeying, strictKex, nonKexBeforeInitialKexInit, authenticationEstablished, initialNewKeysActive, authRequestPending, previousAuthRequestPending, previousChannels, activeChannel, channelEvent, channelOrigin, channels, channelEffects +VARIABLES state, previousState, history, event, origin, packetWasParsed, effects, rekeying, strictKex, nonKexBeforeInitialKexInit, authenticationEstablished, initialNewKeysActive, authRequestPending, previousAuthRequestPending, inboundPacket, lastInboundPacket, inboundTranscriptMatches, inboundHostSignatureValid, inboundTransportValid, hostKeyPossessionVerified, transcriptVerified, transportKeysVerified, lastPacketDisposition, previousChannels, activeChannel, channelEvent, channelOrigin, channels, channelEffects -vars == <> +vars == <> States == {"Authenticated", "Authenticating", "AuthenticationReady", "Disconnected", "Unconnected", "WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys", "WaitService", "WaitVersion"} PostAuthenticatedStates == {"Authenticated", "Authenticating", "AuthenticationReady"} KexStates == {"WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys"} -Events == {"AuthenticationFailure", "AuthenticationSuccess", "AuthorizeAuthenticatedPacket", "AuthorizeAuthenticationPacket", "AuthorizeConnectionPacket", "AuthorizeExtInfo", "BeginAuthentication", "Connect", "Disconnect", "OpenChannel", "ReceiveChannelFailure", "ReceiveChannelOpenConfirmation", "ReceiveChannelOpenFailure", "ReceiveChannelSuccess", "ReceiveDebug", "ReceiveGlobalRequest", "ReceiveIgnore", "ReceiveInitialNonStrictKexInit", "ReceiveInitialStrictKexInit", "ReceiveKex.DhGexGroup", "ReceiveKex.DhGexReply", "ReceiveKex.DhReply", "ReceiveKex.EcdhReply", "ReceiveNewKeys", "ReceiveNonKexPacket", "ReceiveRekeyKexInit", "ReceiveServiceAccept", "ReceiveUserauthBanner", "ReceiveUserauthInfoRequest", "ReceiveVersion", "RekeyStarted", "SendChannelRequest", "UnexpectedKexInit"} +Events == {"AuthenticationFailure", "AuthenticationSuccess", "AuthorizeAuthenticatedPacket", "AuthorizeAuthenticationPacket", "AuthorizeConnectionPacket", "AuthorizeExtInfo", "BeginAuthentication", "Connect", "Disconnect", "HostilePacketRejected", "OpenChannel", "ReceiveChannelFailure", "ReceiveChannelOpenConfirmation", "ReceiveChannelOpenFailure", "ReceiveChannelSuccess", "ReceiveDebug", "ReceiveGlobalRequest", "ReceiveIgnore", "ReceiveInitialNonStrictKexInit", "ReceiveInitialStrictKexInit", "ReceiveKex.DhGexGroup", "ReceiveKex.DhGexReply", "ReceiveKex.DhReply", "ReceiveKex.EcdhReply", "ReceiveNewKeys", "ReceiveNonKexPacket", "ReceiveRekeyKexInit", "ReceiveServiceAccept", "ReceiveUserauthBanner", "ReceiveUserauthInfoRequest", "ReceiveVersion", "RekeyStarted", "SendChannelRequest", "UnexpectedKexInit"} Origins == {"Internal", "LocalCommand", "ParsedPacket", "Timer"} -Effects == {"ActivateEncryption", "ActivateInboundProtection", "ActivateOutboundProtection", "AuthenticationFailure", "AuthenticationSuccess", "ClearNonKexBeforeInitialKexInit", "Debug", "Disconnect", "EnableStrictKex", "Ignore", "NegotiateNonStrictKex", "ReceiveChannelFailure", "ReceiveChannelOpenConfirmation", "ReceiveChannelOpenFailure", "ReceiveChannelSuccess", "ReceiveGlobalRequest", "ReceiveKexDhGexReply", "ReceiveKexDhReply", "ReceiveKexEcdhReply", "ReceiveKexInit", "ReceiveNewKeys", "ReceiveServiceAccept", "ReceiveUserauthBanner", "ReceiveUserauthInfoRequest", "ReceiveVersion", "RecordNonKexBeforeInitialKexInit", "RekeyComplete", "RekeyStarted", "ResetInboundSequence", "ResetOutboundSequence", "SendChannelOpen", "SendChannelRequest", "SendClientExtInfo", "SendKexDhGexInit", "SendKexExchangeInit", "SendKexInit", "SendNewKeys", "SendProtocolError", "SendServiceRequest", "SendUserauthRequest", "SendVersion", "StartAuthentication"} +Effects == {"ActivateEncryption", "ActivateInboundProtection", "ActivateOutboundProtection", "AuthenticationFailure", "AuthenticationSuccess", "ClearNonKexBeforeInitialKexInit", "Debug", "Disconnect", "EnableStrictKex", "Ignore", "NegotiateNonStrictKex", "ReceiveChannelFailure", "ReceiveChannelOpenConfirmation", "ReceiveChannelOpenFailure", "ReceiveChannelSuccess", "ReceiveGlobalRequest", "ReceiveKexDhGexReply", "ReceiveKexDhReply", "ReceiveKexEcdhReply", "ReceiveKexInit", "ReceiveNewKeys", "ReceiveServiceAccept", "ReceiveUserauthBanner", "ReceiveUserauthInfoRequest", "ReceiveVersion", "RecordNonKexBeforeInitialKexInit", "RekeyComplete", "RekeyStarted", "ResetInboundSequence", "ResetOutboundSequence", "SendChannelOpen", "SendChannelRequest", "SendClientExtInfo", "SendKexDhGexInit", "SendKexExchangeInit", "SendKexInit", "SendNewKeys", "SendProtocolError", "SendServiceRequest", "SendUnimplemented", "SendUserauthRequest", "SendVersion", "StartAuthentication", "VerifyHostKeyPossession", "VerifyKexTranscript"} +PacketClasses == {"ChannelOpenReply", "ChannelRequestReply", "ClientConnectionPacket", "ClientKexInit", "ClientServiceRequest", "ClientUserauthRequest", "ConnectionPacket", "Debug", "Disconnect", "ExtInfo", "GlobalRequest", "Ignore", "KexGexGroup", "KexInit", "KexReply", "NewKeys", "ServiceAccept", "Unknown", "UserauthBanner", "UserauthFailure", "UserauthMethodSpecific", "UserauthSuccess"} +PacketDispositions == {"None", "Client", "Accepted", "Unimplemented", "Disconnected"} ChannelStates == {"BOTH_EOF", "CLOSED", "CLOSE_SENT", "LOCAL_EOF", "OPEN", "OPENING", "REMOTE_EOF", "Unallocated"} ChannelEvents == {"AcceptRemoteOpen", "AllocateLocalOpen", "OpenConfirmed", "OpenFailed", "ReceiveClose", "ReceiveData", "ReceiveEof", "ReceiveRequest", "ReceiveWindowAdjust", "SendClose", "SendData", "SendEof", "SendRequest"} @@ -174,7 +176,7 @@ AttemptChannelOperation == ELSE /\ channels' = channels /\ channelEffects' = {} - /\ UNCHANGED <> + /\ UNCHANGED <> Init == /\ state = "Unconnected" @@ -191,6 +193,15 @@ Init == /\ initialNewKeysActive = FALSE /\ authRequestPending = FALSE /\ previousAuthRequestPending = FALSE + /\ inboundPacket = "None" + /\ lastInboundPacket = "None" + /\ inboundTranscriptMatches = FALSE + /\ inboundHostSignatureValid = FALSE + /\ inboundTransportValid = FALSE + /\ hostKeyPossessionVerified = FALSE + /\ transcriptVerified = FALSE + /\ transportKeysVerified = FALSE + /\ lastPacketDisposition = "None" /\ previousChannels = [c \in ChannelIDs |-> "Unallocated"] /\ activeChannel = 0 /\ channelEvent = "None" @@ -200,6 +211,10 @@ Init == AUTHENTICATION_FAILURE == /\ state \in {"Authenticating"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"UserauthFailure"} + /\ inboundTransportValid + ) /\ state' = "AuthenticationReady" /\ previousState' = state /\ history' = history @@ -214,6 +229,15 @@ AUTHENTICATION_FAILURE == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -223,6 +247,10 @@ AUTHENTICATION_FAILURE == AUTHENTICATION_SUCCESS == /\ state \in {"Authenticating"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"UserauthSuccess"} + /\ inboundTransportValid + ) /\ state' = "Authenticated" /\ previousState' = state /\ history' = history @@ -237,6 +265,15 @@ AUTHENTICATION_SUCCESS == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -246,6 +283,10 @@ AUTHENTICATION_SUCCESS == AUTHORIZE_AUTHENTICATED_PACKET == /\ state \in {"Authenticated"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"ConnectionPacket", "ClientConnectionPacket"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -260,6 +301,15 @@ AUTHORIZE_AUTHENTICATED_PACKET == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -269,6 +319,10 @@ AUTHORIZE_AUTHENTICATED_PACKET == AUTHORIZE_AUTHENTICATION_PACKET == /\ state \in {"Authenticating"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"UserauthMethodSpecific"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -283,6 +337,15 @@ AUTHORIZE_AUTHENTICATION_PACKET == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -292,6 +355,10 @@ AUTHORIZE_AUTHENTICATION_PACKET == AUTHORIZE_CONNECTION_PACKET == /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"ConnectionPacket"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -306,6 +373,15 @@ AUTHORIZE_CONNECTION_PACKET == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -315,6 +391,10 @@ AUTHORIZE_CONNECTION_PACKET == AUTHORIZE_POST_AUTH_EXT_INFO == /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"ExtInfo"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -329,6 +409,15 @@ AUTHORIZE_POST_AUTH_EXT_INFO == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -338,6 +427,10 @@ AUTHORIZE_POST_AUTH_EXT_INFO == AUTHORIZE_SERVICE_EXT_INFO == /\ state \in {"WaitService"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"ExtInfo"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -352,6 +445,15 @@ AUTHORIZE_SERVICE_EXT_INFO == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -376,6 +478,15 @@ BEGIN_AUTHENTICATION == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = TRUE /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = "Client" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -399,6 +510,15 @@ CONNECT == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = "Client" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -408,6 +528,10 @@ CONNECT == DISCONNECT == /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady", "Unconnected", "WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys", "WaitService", "WaitVersion"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"Disconnect"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = "Disconnected" /\ previousState' = state /\ history' = history @@ -422,6 +546,15 @@ DISCONNECT == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = FALSE + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -445,6 +578,15 @@ OPEN_CHANNEL == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = "Client" /\ previousChannels' = channels /\ activeChannel' \in ChannelIDs /\ ChannelOperationAllowed(authenticationEstablished, state, channels[activeChannel'], "AllocateLocalOpen") /\ channelEvent' = "AllocateLocalOpen" @@ -454,6 +596,10 @@ OPEN_CHANNEL == RECEIVE_CHANNEL_FAILURE == /\ state \in {"Authenticated"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"ChannelRequestReply"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -468,6 +614,15 @@ RECEIVE_CHANNEL_FAILURE == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -477,6 +632,10 @@ RECEIVE_CHANNEL_FAILURE == RECEIVE_CHANNEL_OPEN_CONFIRMATION == /\ state \in {"Authenticated"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"ChannelOpenReply"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -491,6 +650,15 @@ RECEIVE_CHANNEL_OPEN_CONFIRMATION == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' \in ChannelIDs /\ ChannelOperationAllowed(authenticationEstablished, state, channels[activeChannel'], "OpenConfirmed") /\ channelEvent' = "OpenConfirmed" @@ -500,6 +668,10 @@ RECEIVE_CHANNEL_OPEN_CONFIRMATION == RECEIVE_CHANNEL_OPEN_FAILURE == /\ state \in {"Authenticated"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"ChannelOpenReply"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -514,6 +686,15 @@ RECEIVE_CHANNEL_OPEN_FAILURE == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' \in ChannelIDs /\ ChannelOperationAllowed(authenticationEstablished, state, channels[activeChannel'], "OpenFailed") /\ channelEvent' = "OpenFailed" @@ -523,6 +704,10 @@ RECEIVE_CHANNEL_OPEN_FAILURE == RECEIVE_CHANNEL_SUCCESS == /\ state \in {"Authenticated"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"ChannelRequestReply"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -537,6 +722,15 @@ RECEIVE_CHANNEL_SUCCESS == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -546,6 +740,10 @@ RECEIVE_CHANNEL_SUCCESS == RECEIVE_DEBUG == /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady", "Unconnected", "WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys", "WaitService", "WaitVersion"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"Debug"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -560,6 +758,15 @@ RECEIVE_DEBUG == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -569,6 +776,10 @@ RECEIVE_DEBUG == RECEIVE_GLOBAL_REQUEST == /\ state \in {"Authenticated"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"GlobalRequest"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -583,6 +794,15 @@ RECEIVE_GLOBAL_REQUEST == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -592,6 +812,10 @@ RECEIVE_GLOBAL_REQUEST == RECEIVE_IGNORE == /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady", "Unconnected", "WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys", "WaitService", "WaitVersion"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"Ignore"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -606,6 +830,15 @@ RECEIVE_IGNORE == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -616,6 +849,12 @@ RECEIVE_IGNORE == RECEIVE_INITIAL_NEW_KEYS == /\ state \in {"WaitNewKeys"} /\ ~(rekeying) + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"NewKeys"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) + /\ (~EnforceKexProofVerification \/ hostKeyPossessionVerified) + /\ (~EnforceKexProofVerification \/ transcriptVerified) /\ state' = "WaitService" /\ previousState' = state /\ history' = history @@ -630,6 +869,15 @@ RECEIVE_INITIAL_NEW_KEYS == /\ initialNewKeysActive' = TRUE /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = TRUE + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -640,6 +888,10 @@ RECEIVE_INITIAL_NEW_KEYS == RECEIVE_INITIAL_NON_STRICT_KEX_INIT == /\ state \in {"WaitKexInit"} /\ ~(rekeying) + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = "WaitKex" /\ previousState' = state /\ history' = history @@ -654,6 +906,15 @@ RECEIVE_INITIAL_NON_STRICT_KEX_INIT == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -664,6 +925,10 @@ RECEIVE_INITIAL_NON_STRICT_KEX_INIT == RECEIVE_INITIAL_STRICT_KEX_INIT == /\ state \in {"WaitKexInit"} /\ (~(rekeying)) /\ (~(nonKexBeforeInitialKexInit)) + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = "WaitKex" /\ previousState' = state /\ history' = history @@ -678,6 +943,15 @@ RECEIVE_INITIAL_STRICT_KEX_INIT == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -687,6 +961,10 @@ RECEIVE_INITIAL_STRICT_KEX_INIT == RECEIVE_KEX_DH_GEX_GROUP == /\ state \in {"WaitKex"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexGexGroup"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = "WaitKexDhGexInit" /\ previousState' = state /\ history' = history @@ -701,6 +979,15 @@ RECEIVE_KEX_DH_GEX_GROUP == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -710,13 +997,19 @@ RECEIVE_KEX_DH_GEX_GROUP == RECEIVE_KEX_DH_GEX_REPLY == /\ state \in {"WaitKexDhGexInit"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexReply"} + /\ (~EnforceKexProofVerification \/ inboundHostSignatureValid) + /\ (~EnforceKexProofVerification \/ inboundTranscriptMatches) + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = "WaitNewKeys" /\ previousState' = state /\ history' = history /\ event' = "ReceiveKex.DhGexReply" /\ origin' = "ParsedPacket" /\ packetWasParsed' = (origin' = "ParsedPacket") - /\ effects' = IF strictKex THEN {"ActivateOutboundProtection", "ReceiveKexDhGexReply", "ResetOutboundSequence", "SendNewKeys"} ELSE {"ActivateOutboundProtection", "ReceiveKexDhGexReply", "SendNewKeys"} + /\ effects' = IF strictKex THEN {"ActivateOutboundProtection", "ReceiveKexDhGexReply", "ResetOutboundSequence", "SendNewKeys", "VerifyHostKeyPossession", "VerifyKexTranscript"} ELSE {"ActivateOutboundProtection", "ReceiveKexDhGexReply", "SendNewKeys", "VerifyHostKeyPossession", "VerifyKexTranscript"} /\ rekeying' = rekeying /\ strictKex' = strictKex /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit @@ -724,6 +1017,15 @@ RECEIVE_KEX_DH_GEX_REPLY == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = TRUE + /\ transcriptVerified' = TRUE + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -733,13 +1035,19 @@ RECEIVE_KEX_DH_GEX_REPLY == RECEIVE_KEX_DH_REPLY == /\ state \in {"WaitKex"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexReply"} + /\ (~EnforceKexProofVerification \/ inboundHostSignatureValid) + /\ (~EnforceKexProofVerification \/ inboundTranscriptMatches) + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = "WaitNewKeys" /\ previousState' = state /\ history' = history /\ event' = "ReceiveKex.DhReply" /\ origin' = "ParsedPacket" /\ packetWasParsed' = (origin' = "ParsedPacket") - /\ effects' = IF strictKex THEN {"ActivateOutboundProtection", "ReceiveKexDhReply", "ResetOutboundSequence", "SendNewKeys"} ELSE {"ActivateOutboundProtection", "ReceiveKexDhReply", "SendNewKeys"} + /\ effects' = IF strictKex THEN {"ActivateOutboundProtection", "ReceiveKexDhReply", "ResetOutboundSequence", "SendNewKeys", "VerifyHostKeyPossession", "VerifyKexTranscript"} ELSE {"ActivateOutboundProtection", "ReceiveKexDhReply", "SendNewKeys", "VerifyHostKeyPossession", "VerifyKexTranscript"} /\ rekeying' = rekeying /\ strictKex' = strictKex /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit @@ -747,6 +1055,15 @@ RECEIVE_KEX_DH_REPLY == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = TRUE + /\ transcriptVerified' = TRUE + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -756,13 +1073,19 @@ RECEIVE_KEX_DH_REPLY == RECEIVE_KEX_ECDH_REPLY == /\ state \in {"WaitKex"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexReply"} + /\ (~EnforceKexProofVerification \/ inboundHostSignatureValid) + /\ (~EnforceKexProofVerification \/ inboundTranscriptMatches) + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = "WaitNewKeys" /\ previousState' = state /\ history' = history /\ event' = "ReceiveKex.EcdhReply" /\ origin' = "ParsedPacket" /\ packetWasParsed' = (origin' = "ParsedPacket") - /\ effects' = IF strictKex THEN {"ActivateOutboundProtection", "ReceiveKexEcdhReply", "ResetOutboundSequence", "SendNewKeys"} ELSE {"ActivateOutboundProtection", "ReceiveKexEcdhReply", "SendNewKeys"} + /\ effects' = IF strictKex THEN {"ActivateOutboundProtection", "ReceiveKexEcdhReply", "ResetOutboundSequence", "SendNewKeys", "VerifyHostKeyPossession", "VerifyKexTranscript"} ELSE {"ActivateOutboundProtection", "ReceiveKexEcdhReply", "SendNewKeys", "VerifyHostKeyPossession", "VerifyKexTranscript"} /\ rekeying' = rekeying /\ strictKex' = strictKex /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit @@ -770,6 +1093,15 @@ RECEIVE_KEX_ECDH_REPLY == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = TRUE + /\ transcriptVerified' = TRUE + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -780,6 +1112,10 @@ RECEIVE_KEX_ECDH_REPLY == RECEIVE_REKEY_KEX_INIT == /\ state \in {"WaitKexInit"} /\ rekeying + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = "WaitKex" /\ previousState' = state /\ history' = history @@ -794,6 +1130,15 @@ RECEIVE_REKEY_KEX_INIT == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -804,6 +1149,12 @@ RECEIVE_REKEY_KEX_INIT == RECEIVE_REKEY_NEW_KEYS == /\ state \in {"WaitNewKeys"} /\ rekeying + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"NewKeys"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) + /\ (~EnforceKexProofVerification \/ hostKeyPossessionVerified) + /\ (~EnforceKexProofVerification \/ transcriptVerified) /\ state' = history /\ previousState' = state /\ history' = history @@ -818,6 +1169,15 @@ RECEIVE_REKEY_NEW_KEYS == /\ initialNewKeysActive' = TRUE /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = TRUE + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -827,6 +1187,10 @@ RECEIVE_REKEY_NEW_KEYS == RECEIVE_SERVICE_ACCEPT == /\ state \in {"WaitService"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"ServiceAccept"} + /\ inboundTransportValid + ) /\ state' = "AuthenticationReady" /\ previousState' = state /\ history' = history @@ -841,6 +1205,15 @@ RECEIVE_SERVICE_ACCEPT == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -850,6 +1223,10 @@ RECEIVE_SERVICE_ACCEPT == RECEIVE_USERAUTH_BANNER_AUTHENTICATING == /\ state \in {"Authenticating"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"UserauthBanner"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -864,6 +1241,15 @@ RECEIVE_USERAUTH_BANNER_AUTHENTICATING == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -873,6 +1259,10 @@ RECEIVE_USERAUTH_BANNER_AUTHENTICATING == RECEIVE_USERAUTH_BANNER_READY == /\ state \in {"AuthenticationReady"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"UserauthBanner"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -887,6 +1277,15 @@ RECEIVE_USERAUTH_BANNER_READY == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -896,6 +1295,10 @@ RECEIVE_USERAUTH_BANNER_READY == RECEIVE_USERAUTH_INFO_REQUEST == /\ state \in {"Authenticating"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"UserauthMethodSpecific"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -910,6 +1313,15 @@ RECEIVE_USERAUTH_INFO_REQUEST == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -933,6 +1345,15 @@ RECEIVE_VERSION == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = "Client" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -957,6 +1378,15 @@ RECORD_NON_KEX_BEFORE_INITIAL_KEX_INIT == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = "Client" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -981,6 +1411,15 @@ REJECT_NON_KEX_WAIT_KEX == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = FALSE + /\ lastPacketDisposition' = "Client" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -1005,6 +1444,15 @@ REJECT_NON_KEX_WAIT_KEX_DH_GEX_INIT == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = FALSE + /\ lastPacketDisposition' = "Client" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -1029,6 +1477,15 @@ REJECT_NON_KEX_WAIT_NEW_KEYS == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = FALSE + /\ lastPacketDisposition' = "Client" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -1039,6 +1496,10 @@ REJECT_NON_KEX_WAIT_NEW_KEYS == REJECT_STRICT_KEX_INIT_NOT_FIRST == /\ state \in {"WaitKexInit"} /\ (~(rekeying)) /\ (nonKexBeforeInitialKexInit) + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = "Disconnected" /\ previousState' = state /\ history' = history @@ -1053,6 +1514,15 @@ REJECT_STRICT_KEX_INIT_NOT_FIRST == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = FALSE + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -1076,6 +1546,15 @@ REKEY_STARTED == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = "Client" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -1100,6 +1579,15 @@ REPEAT_BEGIN_AUTHENTICATION == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = TRUE /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = "Client" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -1123,6 +1611,15 @@ SEND_CHANNEL_REQUEST == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = authRequestPending /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = "Client" /\ previousChannels' = channels /\ activeChannel' \in ChannelIDs /\ ChannelOperationAllowed(authenticationEstablished, state, channels[activeChannel'], "SendRequest") /\ channelEvent' = "SendRequest" @@ -1132,6 +1629,10 @@ SEND_CHANNEL_REQUEST == UNEXPECTED_KEX_INIT_WAIT_KEX == /\ state \in {"WaitKex"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = "Disconnected" /\ previousState' = state /\ history' = history @@ -1146,6 +1647,15 @@ UNEXPECTED_KEX_INIT_WAIT_KEX == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = FALSE + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -1155,6 +1665,10 @@ UNEXPECTED_KEX_INIT_WAIT_KEX == UNEXPECTED_KEX_INIT_WAIT_KEX_DH_GEX_INIT == /\ state \in {"WaitKexDhGexInit"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = "Disconnected" /\ previousState' = state /\ history' = history @@ -1169,6 +1683,15 @@ UNEXPECTED_KEX_INIT_WAIT_KEX_DH_GEX_INIT == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = FALSE + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -1178,6 +1701,10 @@ UNEXPECTED_KEX_INIT_WAIT_KEX_DH_GEX_INIT == UNEXPECTED_KEX_INIT_WAIT_NEW_KEYS == /\ state \in {"WaitNewKeys"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = "Disconnected" /\ previousState' = state /\ history' = history @@ -1192,6 +1719,15 @@ UNEXPECTED_KEX_INIT_WAIT_NEW_KEYS == /\ initialNewKeysActive' = initialNewKeysActive /\ authRequestPending' = FALSE /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = FALSE + /\ lastPacketDisposition' = IF inboundPacket = "None" THEN "Client" ELSE "Accepted" /\ previousChannels' = channels /\ activeChannel' = 0 /\ channelEvent' = "None" @@ -1199,7 +1735,174 @@ UNEXPECTED_KEX_INIT_WAIT_NEW_KEYS == /\ channels' = [c \in ChannelIDs |-> IF channels[c] = "Unallocated" THEN "Unallocated" ELSE "CLOSED"] /\ channelEffects' = {} -Next == +PacketTransitionEnabled == + \/ /\ state \in {"Authenticating"} + /\ inboundPacket \in {"UserauthFailure"} + /\ inboundTransportValid + \/ /\ state \in {"Authenticating"} + /\ inboundPacket \in {"UserauthSuccess"} + /\ inboundTransportValid + \/ /\ state \in {"Authenticated"} + /\ inboundPacket \in {"ConnectionPacket", "ClientConnectionPacket"} + /\ inboundTransportValid + \/ /\ state \in {"Authenticating"} + /\ inboundPacket \in {"UserauthMethodSpecific"} + /\ inboundTransportValid + \/ /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady"} + /\ inboundPacket \in {"ConnectionPacket"} + /\ inboundTransportValid + \/ /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady"} + /\ inboundPacket \in {"ExtInfo"} + /\ inboundTransportValid + \/ /\ state \in {"WaitService"} + /\ inboundPacket \in {"ExtInfo"} + /\ inboundTransportValid + \/ /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady", "Unconnected", "WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys", "WaitService", "WaitVersion"} + /\ inboundPacket \in {"Disconnect"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + \/ /\ state \in {"Authenticated"} + /\ inboundPacket \in {"ChannelRequestReply"} + /\ inboundTransportValid + \/ /\ state \in {"Authenticated"} + /\ inboundPacket \in {"ChannelOpenReply"} + /\ inboundTransportValid + \/ /\ state \in {"Authenticated"} + /\ inboundPacket \in {"ChannelOpenReply"} + /\ inboundTransportValid + \/ /\ state \in {"Authenticated"} + /\ inboundPacket \in {"ChannelRequestReply"} + /\ inboundTransportValid + \/ /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady", "Unconnected", "WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys", "WaitService", "WaitVersion"} + /\ inboundPacket \in {"Debug"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + \/ /\ state \in {"Authenticated"} + /\ inboundPacket \in {"GlobalRequest"} + /\ inboundTransportValid + \/ /\ state \in {"Authenticated", "Authenticating", "AuthenticationReady", "Unconnected", "WaitKex", "WaitKexDhGexInit", "WaitKexInit", "WaitNewKeys", "WaitService", "WaitVersion"} + /\ inboundPacket \in {"Ignore"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + \/ /\ state \in {"WaitNewKeys"} + /\ inboundPacket \in {"NewKeys"} + /\ ~(rekeying) + /\ (~initialNewKeysActive \/ inboundTransportValid) + /\ (~EnforceKexProofVerification \/ hostKeyPossessionVerified) + /\ (~EnforceKexProofVerification \/ transcriptVerified) + \/ /\ state \in {"WaitKexInit"} + /\ inboundPacket \in {"KexInit"} + /\ ~(rekeying) + /\ (~initialNewKeysActive \/ inboundTransportValid) + \/ /\ state \in {"WaitKexInit"} + /\ inboundPacket \in {"KexInit"} + /\ (~(rekeying)) /\ (~(nonKexBeforeInitialKexInit)) + /\ (~initialNewKeysActive \/ inboundTransportValid) + \/ /\ state \in {"WaitKex"} + /\ inboundPacket \in {"KexGexGroup"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + \/ /\ state \in {"WaitKexDhGexInit"} + /\ inboundPacket \in {"KexReply"} + /\ (~EnforceKexProofVerification \/ inboundHostSignatureValid) + /\ (~EnforceKexProofVerification \/ inboundTranscriptMatches) + /\ (~initialNewKeysActive \/ inboundTransportValid) + \/ /\ state \in {"WaitKex"} + /\ inboundPacket \in {"KexReply"} + /\ (~EnforceKexProofVerification \/ inboundHostSignatureValid) + /\ (~EnforceKexProofVerification \/ inboundTranscriptMatches) + /\ (~initialNewKeysActive \/ inboundTransportValid) + \/ /\ state \in {"WaitKex"} + /\ inboundPacket \in {"KexReply"} + /\ (~EnforceKexProofVerification \/ inboundHostSignatureValid) + /\ (~EnforceKexProofVerification \/ inboundTranscriptMatches) + /\ (~initialNewKeysActive \/ inboundTransportValid) + \/ /\ state \in {"WaitKexInit"} + /\ inboundPacket \in {"KexInit"} + /\ rekeying + /\ (~initialNewKeysActive \/ inboundTransportValid) + \/ /\ state \in {"WaitNewKeys"} + /\ inboundPacket \in {"NewKeys"} + /\ rekeying + /\ (~initialNewKeysActive \/ inboundTransportValid) + /\ (~EnforceKexProofVerification \/ hostKeyPossessionVerified) + /\ (~EnforceKexProofVerification \/ transcriptVerified) + \/ /\ state \in {"WaitService"} + /\ inboundPacket \in {"ServiceAccept"} + /\ inboundTransportValid + \/ /\ state \in {"Authenticating"} + /\ inboundPacket \in {"UserauthBanner"} + /\ inboundTransportValid + \/ /\ state \in {"AuthenticationReady"} + /\ inboundPacket \in {"UserauthBanner"} + /\ inboundTransportValid + \/ /\ state \in {"Authenticating"} + /\ inboundPacket \in {"UserauthMethodSpecific"} + /\ inboundTransportValid + \/ /\ state \in {"WaitKexInit"} + /\ inboundPacket \in {"KexInit"} + /\ (~(rekeying)) /\ (nonKexBeforeInitialKexInit) + /\ (~initialNewKeysActive \/ inboundTransportValid) + \/ /\ state \in {"WaitKex"} + /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + \/ /\ state \in {"WaitKexDhGexInit"} + /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + \/ /\ state \in {"WaitNewKeys"} + /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + +HostilePacketFatal == + \/ /\ strictKex /\ ~rekeying /\ state \in KexStates + /\ ~PacketTransitionEnabled + \/ /\ inboundPacket = "KexInit" + /\ state \in {"WaitKex", "WaitKexDhGexInit", "WaitNewKeys"} + \/ /\ inboundPacket = "KexReply" + /\ (~inboundHostSignatureValid \/ ~inboundTranscriptMatches) + \/ /\ initialNewKeysActive /\ ~inboundTransportValid + +RejectHostilePacket == + /\ inboundPacket # "None" + /\ ~PacketTransitionEnabled + /\ state' = IF HostilePacketFatal THEN "Disconnected" ELSE state + /\ previousState' = state + /\ history' = history + /\ event' = "HostilePacketRejected" + /\ origin' = "ParsedPacket" + /\ packetWasParsed' = TRUE + /\ effects' = IF HostilePacketFatal THEN {"Disconnect", "SendProtocolError"} ELSE {"SendUnimplemented"} + /\ rekeying' = IF HostilePacketFatal THEN FALSE ELSE rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit + /\ authenticationEstablished' = authenticationEstablished + /\ initialNewKeysActive' = initialNewKeysActive + /\ authRequestPending' = IF HostilePacketFatal THEN FALSE ELSE authRequestPending + /\ previousAuthRequestPending' = authRequestPending + /\ inboundPacket' = "None" + /\ lastInboundPacket' = inboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = IF HostilePacketFatal THEN FALSE ELSE hostKeyPossessionVerified + /\ transcriptVerified' = IF HostilePacketFatal THEN FALSE ELSE transcriptVerified + /\ transportKeysVerified' = IF HostilePacketFatal THEN FALSE ELSE transportKeysVerified + /\ lastPacketDisposition' = IF HostilePacketFatal THEN "Disconnected" ELSE "Unimplemented" + /\ previousChannels' = channels + /\ activeChannel' = 0 + /\ channelEvent' = "None" + /\ channelOrigin' = "None" + /\ channels' = IF HostilePacketFatal THEN [c \in ChannelIDs |-> IF channels[c] = "Unallocated" THEN "Unallocated" ELSE "CLOSED"] ELSE channels + /\ channelEffects' = {} + +HostileEnvironmentNext == + /\ EnableHostileEnvironment + /\ inboundPacket = "None" + /\ inboundPacket' \in PacketClasses + /\ inboundTranscriptMatches' \in BOOLEAN + /\ inboundHostSignatureValid' \in BOOLEAN + /\ (inboundHostSignatureValid' => AdversaryOwnsHostKey) + /\ inboundTransportValid' \in BOOLEAN + /\ (inboundTransportValid' => AdversaryOwnsHostKey /\ transportKeysVerified) + /\ UNCHANGED <> + +ClientNext == \/ AUTHENTICATION_FAILURE \/ AUTHENTICATION_SUCCESS \/ AUTHORIZE_AUTHENTICATED_PACKET @@ -1244,6 +1947,9 @@ Next == \/ UNEXPECTED_KEX_INIT_WAIT_KEX_DH_GEX_INIT \/ UNEXPECTED_KEX_INIT_WAIT_NEW_KEYS \/ AttemptChannelOperation + \/ RejectHostilePacket + +Next == ClientNext \/ HostileEnvironmentNext Spec == Init /\ [][Next]_vars ==== diff --git a/sshlib/src/test/resources/tla/SshClientStateMachineHostilePeer.cfg b/sshlib/src/test/resources/tla/SshClientStateMachineHostilePeer.cfg new file mode 100644 index 00000000..f01c84fd --- /dev/null +++ b/sshlib/src/test/resources/tla/SshClientStateMachineHostilePeer.cfg @@ -0,0 +1,28 @@ +SPECIFICATION Spec + +CONSTANT MaxChannels = 1 +CONSTANT EnableHostileEnvironment = TRUE +CONSTANT AdversaryOwnsHostKey = TRUE +CONSTANT EnforceKexProofVerification = TRUE + +VIEW ModelView +ACTION_CONSTRAINT HostileSecurityActionConstraint + +INVARIANT TypeOK +INVARIANT ParsedPacketProvenance +INVARIANT NoForgedPacketProvenance +INVARIANT AuthenticationSuccessIsGuarded +INVARIANT AuthenticationStateIsMonotonic +INVARIANT KexEventsAreStrictlySequenced +INVARIANT StrictInitialKexRejectsNonKexPackets +INVARIANT StrictKexInitMustBeFirst +INVARIANT UserAuthenticationRequiresInitialNewKeys +INVARIANT UnexpectedKexInitIsFatal +INVARIANT HostileKexReplyRequiresPossessionProof +INVARIANT NewKeysRequiresVerifiedTranscript +INVARIANT ProtectedHostilePacketsRequireTransportAuthentication +INVARIANT AuthenticationRequiresVerifiedTransport +INVARIANT HostileClientRolePacketsNeverAdvance +INVARIANT RejectedHostilePacketsDoNotEstablishSecurity + +CHECK_DEADLOCK FALSE diff --git a/sshlib/src/test/resources/tla/SshClientStateMachineOnPath.cfg b/sshlib/src/test/resources/tla/SshClientStateMachineOnPath.cfg new file mode 100644 index 00000000..1ddcd7ff --- /dev/null +++ b/sshlib/src/test/resources/tla/SshClientStateMachineOnPath.cfg @@ -0,0 +1,28 @@ +SPECIFICATION Spec + +CONSTANT MaxChannels = 1 +CONSTANT EnableHostileEnvironment = TRUE +CONSTANT AdversaryOwnsHostKey = FALSE +CONSTANT EnforceKexProofVerification = TRUE + +VIEW ModelView +ACTION_CONSTRAINT HostileSecurityActionConstraint + +INVARIANT TypeOK +INVARIANT ParsedPacketProvenance +INVARIANT NoForgedPacketProvenance +INVARIANT AuthenticationSuccessIsGuarded +INVARIANT AuthenticationStateIsMonotonic +INVARIANT KexEventsAreStrictlySequenced +INVARIANT StrictInitialKexRejectsNonKexPackets +INVARIANT StrictKexInitMustBeFirst +INVARIANT UserAuthenticationRequiresInitialNewKeys +INVARIANT UnexpectedKexInitIsFatal +INVARIANT HostileKexReplyRequiresPossessionProof +INVARIANT NewKeysRequiresVerifiedTranscript +INVARIANT ProtectedHostilePacketsRequireTransportAuthentication +INVARIANT AuthenticationRequiresVerifiedTransport +INVARIANT HostileClientRolePacketsNeverAdvance +INVARIANT RejectedHostilePacketsDoNotEstablishSecurity + +CHECK_DEADLOCK FALSE diff --git a/sshlib/src/test/resources/tla/SshClientStateMachineUnsafeProof.cfg b/sshlib/src/test/resources/tla/SshClientStateMachineUnsafeProof.cfg new file mode 100644 index 00000000..07a1ef7b --- /dev/null +++ b/sshlib/src/test/resources/tla/SshClientStateMachineUnsafeProof.cfg @@ -0,0 +1,14 @@ +SPECIFICATION Spec + +CONSTANT MaxChannels = 1 +CONSTANT EnableHostileEnvironment = TRUE +CONSTANT AdversaryOwnsHostKey = FALSE +CONSTANT EnforceKexProofVerification = FALSE + +VIEW ModelView +ACTION_CONSTRAINT HostileSecurityActionConstraint + +INVARIANT TypeOK +INVARIANT HostileKexReplyRequiresPossessionProof + +CHECK_DEADLOCK FALSE From 94c52b25b1306a9ab2a158d13404f370ead5744d Mon Sep 17 00:00:00 2001 From: Kenny Root Date: Wed, 22 Jul 2026 21:06:24 -0700 Subject: [PATCH 4/4] chore(tla+): make build rules more readable --- sshlib/build.gradle.kts | 285 +++++++++++++++++----------------------- 1 file changed, 117 insertions(+), 168 deletions(-) diff --git a/sshlib/build.gradle.kts b/sshlib/build.gradle.kts index 67989afa..158f90a4 100644 --- a/sshlib/build.gradle.kts +++ b/sshlib/build.gradle.kts @@ -70,136 +70,54 @@ tasks.test { val tlaModelDirectory = layout.projectDirectory.dir("src/test/resources/tla") val tlaStateDirectory = layout.buildDirectory.dir("tla/states") - -tasks.register("generateSshStateMachineTla") { - group = "verification" - description = "Regenerates the TLA+ lifecycle model from SshClientStateMachine" - dependsOn(tasks.testClasses) - classpath = sourceSets.test.get().runtimeClasspath - mainClass.set("org.connectbot.sshlib.protocol.SshStateMachineTlaGenerator") - args(tlaModelDirectory.file("SshClientStateMachineGenerated.tla").asFile.absolutePath) -} - -tasks.register("generateSftpStateMachineTla") { - group = "verification" - description = "Regenerates the TLA+ lifecycle model from SftpStateMachine" - dependsOn(tasks.testClasses) - classpath = sourceSets.test.get().runtimeClasspath - mainClass.set("org.connectbot.sshlib.protocol.SftpStateMachineTlaGenerator") - args(tlaModelDirectory.file("SftpClientStateMachineGenerated.tla").asFile.absolutePath) -} - val tla2toolsJar = providers.gradleProperty("tla2toolsJar") .orElse(providers.environmentVariable("TLA2TOOLS_JAR")) -tasks.register("checkSshStateMachineTla") { - group = "verification" - description = "Checks the generated SSH lifecycle model with TLC" - mainClass.set("tlc2.TLC") - workingDir(tlaModelDirectory) - args( - "-workers", - "1", - "-metadir", - tlaStateDirectory.get().asFile.absolutePath, - "-config", - "SshClientStateMachine.cfg", - "SshClientStateMachine.tla", - ) - jvmArgs("-XX:+UseParallelGC") - doFirst { - val jarPath = tla2toolsJar.orNull - ?: throw GradleException( - "Set -Ptla2toolsJar=/path/to/tla2tools.jar or TLA2TOOLS_JAR to run TLC", - ) - classpath = files(jarPath) - } -} - listOf( - "OnPath" to "SshClientStateMachineOnPath.cfg", - "HostilePeer" to "SshClientStateMachineHostilePeer.cfg", -).forEach { (profile, configFile) -> - tasks.register("checkSshStateMachine${profile}Tla") { + "Ssh" to ("SshClientStateMachine" to "SshStateMachineTlaGenerator"), + "Sftp" to ("SftpClientStateMachine" to "SftpStateMachineTlaGenerator"), +).forEach { (type, config) -> + val (modelName, generatorClass) = config + tasks.register("generate${type}StateMachineTla") { group = "verification" - description = "Checks the generated SSH lifecycle model with the $profile hostile environment" - mainClass.set("tlc2.TLC") - workingDir(tlaModelDirectory) - args( - "-workers", - "1", - "-metadir", - tlaStateDirectory.get().dir("ssh-${profile.lowercase()}").asFile.absolutePath, - "-config", - configFile, - "SshClientStateMachine.tla", - ) - jvmArgs("-XX:+UseParallelGC") - doFirst { - val jarPath = tla2toolsJar.orNull - ?: throw GradleException( - "Set -Ptla2toolsJar=/path/to/tla2tools.jar or TLA2TOOLS_JAR to run TLC", - ) - classpath = files(jarPath) - } + description = "Regenerates the TLA+ lifecycle model from $modelName" + dependsOn(tasks.testClasses) + classpath = sourceSets.test.get().runtimeClasspath + mainClass.set("org.connectbot.sshlib.protocol.$generatorClass") + args(tlaModelDirectory.file("${modelName}Generated.tla").asFile.absolutePath) } } -val unsafeProofCounterexampleOutput = ByteArrayOutputStream() -tasks.register("checkSshStateMachineUnsafeProofTla") { +fun TaskContainer.registerTlcCheck( + name: String, + description: String, + configFile: String, + tlaFile: String, + stateSubdir: String? = null, + configure: (JavaExec.() -> Unit)? = null, +): TaskProvider = register(name) { group = "verification" - description = "Requires TLC to find a hostile KEX counterexample when proof verification is disabled" + this.description = description mainClass.set("tlc2.TLC") workingDir(tlaModelDirectory) - args( - "-workers", - "1", - "-metadir", - tlaStateDirectory.get().dir("ssh-unsafe-proof").asFile.absolutePath, - "-config", - "SshClientStateMachineUnsafeProof.cfg", - "SshClientStateMachine.tla", - ) - jvmArgs("-XX:+UseParallelGC") - standardOutput = unsafeProofCounterexampleOutput - errorOutput = unsafeProofCounterexampleOutput - isIgnoreExitValue = true - doFirst { - unsafeProofCounterexampleOutput.reset() - val jarPath = tla2toolsJar.orNull - ?: throw GradleException( - "Set -Ptla2toolsJar=/path/to/tla2tools.jar or TLA2TOOLS_JAR to run TLC", - ) - classpath = files(jarPath) - } - doLast { - val output = unsafeProofCounterexampleOutput.toString(Charsets.UTF_8) - logger.lifecycle(output) - val exitValue = executionResult.get().exitValue - if (exitValue == 0 || "Invariant HostileKexReplyRequiresPossessionProof is violated" !in output) { - throw GradleException( - "Expected TLC to find the disabled-proof counterexample; exit=$exitValue", - ) - } - logger.lifecycle("Expected disabled-proof counterexample found; treating it as success.") + + val metaDir = if (stateSubdir != null) { + tlaStateDirectory.get().dir(stateSubdir).asFile.absolutePath + } else { + tlaStateDirectory.get().asFile.absolutePath } -} -tasks.register("checkSftpStateMachineTla") { - group = "verification" - description = "Checks the generated SFTP lifecycle model with TLC" - mainClass.set("tlc2.TLC") - workingDir(tlaModelDirectory) args( "-workers", "1", "-metadir", - tlaStateDirectory.get().asFile.absolutePath, + metaDir, "-config", - "SftpClientStateMachine.cfg", - "SftpClientStateMachine.tla", + configFile, + tlaFile, ) jvmArgs("-XX:+UseParallelGC") + doFirst { val jarPath = tla2toolsJar.orNull ?: throw GradleException( @@ -207,72 +125,103 @@ tasks.register("checkSftpStateMachineTla") { ) classpath = files(jarPath) } + + configure?.invoke(this) } -val checkSshTerrapinStrictTla = tasks.register("checkSshTerrapinStrictTla") { - group = "verification" - description = "Proves that strict KEX prevents the modeled Terrapin prefix truncation attack" - mainClass.set("tlc2.TLC") - workingDir(tlaModelDirectory) - args( - "-workers", - "1", - "-metadir", - tlaStateDirectory.get().dir("terrapin-strict").asFile.absolutePath, - "-config", - "SshTerrapinStrict.cfg", - "SshTerrapin.tla", - ) - jvmArgs("-XX:+UseParallelGC") - doFirst { - val jarPath = tla2toolsJar.orNull - ?: throw GradleException( - "Set -Ptla2toolsJar=/path/to/tla2tools.jar or TLA2TOOLS_JAR to run TLC", - ) - classpath = files(jarPath) +fun TaskContainer.registerTlcCounterexampleCheck( + name: String, + description: String, + configFile: String, + tlaFile: String, + stateSubdir: String, + expectedViolation: String, + failureMessage: String, + successMessage: String, +): TaskProvider { + val outputStream = ByteArrayOutputStream() + return registerTlcCheck( + name = name, + description = description, + configFile = configFile, + tlaFile = tlaFile, + stateSubdir = stateSubdir, + ) { + standardOutput = outputStream + errorOutput = outputStream + isIgnoreExitValue = true + doFirst { + outputStream.reset() + } + doLast { + val output = outputStream.toString(Charsets.UTF_8) + logger.lifecycle(output) + val exitValue = executionResult.get().exitValue + if (exitValue == 0 || expectedViolation !in output) { + throw GradleException("$failureMessage; exit=$exitValue") + } + logger.lifecycle(successMessage) + } } } -val terrapinCounterexampleOutput = ByteArrayOutputStream() -val checkSshTerrapinNonStrictTla = tasks.register("checkSshTerrapinNonStrictTla") { - group = "verification" - description = "Requires TLC to find the modeled Terrapin counterexample without failing the build" - mainClass.set("tlc2.TLC") - workingDir(tlaModelDirectory) - args( - "-workers", - "1", - "-metadir", - tlaStateDirectory.get().dir("terrapin-non-strict").asFile.absolutePath, - "-config", - "SshTerrapinNonStrict.cfg", - "SshTerrapin.tla", +tasks.registerTlcCheck( + name = "checkSshStateMachineTla", + description = "Checks the generated SSH lifecycle model with TLC", + configFile = "SshClientStateMachine.cfg", + tlaFile = "SshClientStateMachine.tla", +) + +listOf( + "OnPath" to "SshClientStateMachineOnPath.cfg", + "HostilePeer" to "SshClientStateMachineHostilePeer.cfg", +).forEach { (profile, configFile) -> + tasks.registerTlcCheck( + name = "checkSshStateMachine${profile}Tla", + description = "Checks the generated SSH lifecycle model with the $profile hostile environment", + configFile = configFile, + tlaFile = "SshClientStateMachine.tla", + stateSubdir = "ssh-${profile.lowercase()}", ) - jvmArgs("-XX:+UseParallelGC") - standardOutput = terrapinCounterexampleOutput - errorOutput = terrapinCounterexampleOutput - isIgnoreExitValue = true - doFirst { - terrapinCounterexampleOutput.reset() - val jarPath = tla2toolsJar.orNull - ?: throw GradleException( - "Set -Ptla2toolsJar=/path/to/tla2tools.jar or TLA2TOOLS_JAR to run TLC", - ) - classpath = files(jarPath) - } - doLast { - val output = terrapinCounterexampleOutput.toString(Charsets.UTF_8) - logger.lifecycle(output) - val exitValue = executionResult.get().exitValue - if (exitValue == 0 || "Invariant NoTerrapin is violated" !in output) { - throw GradleException( - "Expected TLC to find the non-strict Terrapin counterexample; exit=$exitValue", - ) - } - logger.lifecycle("Expected non-strict Terrapin counterexample found; treating it as success.") - } } +tasks.registerTlcCounterexampleCheck( + name = "checkSshStateMachineUnsafeProofTla", + description = "Requires TLC to find a hostile KEX counterexample when proof verification is disabled", + configFile = "SshClientStateMachineUnsafeProof.cfg", + tlaFile = "SshClientStateMachine.tla", + stateSubdir = "ssh-unsafe-proof", + expectedViolation = "Invariant HostileKexReplyRequiresPossessionProof is violated", + failureMessage = "Expected TLC to find the disabled-proof counterexample", + successMessage = "Expected disabled-proof counterexample found; treating it as success.", +) + +tasks.registerTlcCheck( + name = "checkSftpStateMachineTla", + description = "Checks the generated SFTP lifecycle model with TLC", + configFile = "SftpClientStateMachine.cfg", + tlaFile = "SftpClientStateMachine.tla", +) + +val checkSshTerrapinStrictTla = tasks.registerTlcCheck( + name = "checkSshTerrapinStrictTla", + description = "Proves that strict KEX prevents the modeled Terrapin prefix truncation attack", + configFile = "SshTerrapinStrict.cfg", + tlaFile = "SshTerrapin.tla", + stateSubdir = "terrapin-strict", +) + +val checkSshTerrapinNonStrictTla = tasks.registerTlcCounterexampleCheck( + name = "checkSshTerrapinNonStrictTla", + description = "Requires TLC to find the modeled Terrapin counterexample without failing the build", + configFile = "SshTerrapinNonStrict.cfg", + tlaFile = "SshTerrapin.tla", + stateSubdir = "terrapin-non-strict", + expectedViolation = "Invariant NoTerrapin is violated", + failureMessage = "Expected TLC to find the non-strict Terrapin counterexample", + successMessage = "Expected non-strict Terrapin counterexample found; treating it as success.", +) + tasks.register("checkSshTerrapinTla") { group = "verification" description = "Checks strict Terrapin resistance and the expected non-strict counterexample"