diff --git a/sshlib/build.gradle.kts b/sshlib/build.gradle.kts index b3dffa0..158f90a 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) @@ -69,67 +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( + "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 = "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) } } -tasks.register("checkSftpStateMachineTla") { +fun TaskContainer.registerTlcCheck( + name: String, + description: String, + configFile: String, + tlaFile: String, + stateSubdir: String? = null, + configure: (JavaExec.() -> Unit)? = null, +): TaskProvider = register(name) { group = "verification" - description = "Checks the generated SFTP lifecycle model with TLC" + this.description = description mainClass.set("tlc2.TLC") workingDir(tlaModelDirectory) + + val metaDir = if (stateSubdir != null) { + tlaStateDirectory.get().dir(stateSubdir).asFile.absolutePath + } else { + tlaStateDirectory.get().asFile.absolutePath + } + 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( @@ -137,6 +125,107 @@ tasks.register("checkSftpStateMachineTla") { ) classpath = files(jarPath) } + + configure?.invoke(this) +} + +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) + } + } +} + +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()}", + ) +} + +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" + dependsOn(checkSshTerrapinStrictTla, checkSshTerrapinNonStrictTla) } tasks.register("generateTla") { @@ -148,7 +237,14 @@ tasks.register("generateTla") { tasks.register("checkTla") { group = "verification" description = "Checks all TLA+ formal models (SSH and SFTP) with TLC" - dependsOn("checkSshStateMachineTla", "checkSftpStateMachineTla") + 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 62ebb4f..0ce5f11 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 @@ -156,6 +157,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 +301,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 +317,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 +371,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 +1220,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 +1241,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 +1302,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 +1525,7 @@ class SshConnection( ) } - private suspend fun sendNewKeys() { + private suspend fun sendNewKeys(resetSequenceNumber: Boolean) { logger.info("Sending NEW_KEYS") prepareEncryption() try { @@ -1530,7 +1537,7 @@ class SshConnection( protection.installOutbound(packetIO) packetIO.enableSendCompression(pendingSendCompressor, pendingCompressionImmediate) pendingSendCompressor = null - if (strictKexEnabled) { + if (resetSequenceNumber) { packetIO.resetSendSequenceNumber() } outboundPacketController.completeKex() @@ -1620,14 +1627,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() } } @@ -2335,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) { @@ -2347,16 +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 (isRekeying && stateMachine.isKexInProgress() && msgType.id().toInt() >= SSH_MSG_USERAUTH_REQUEST_ID) { + 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() && 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 } @@ -2374,6 +2391,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,19 +2407,17 @@ 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) } + 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() @@ -2712,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 && @@ -2755,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()}") } } } @@ -2874,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 68af679..81e8e95 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,45 @@ 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.VERIFY_HOST_KEY_POSSESSION, + SshEffect.VERIFY_KEX_TRANSCRIPT, + 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.VERIFY_HOST_KEY_POSSESSION, + SshEffect.VERIFY_KEX_TRANSCRIPT, + 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 +436,29 @@ 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.VERIFY_HOST_KEY_POSSESSION, + SshEffect.VERIFY_KEX_TRANSCRIPT, + 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 +472,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 +487,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 +504,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 +584,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 +598,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 +656,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 +683,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 +696,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 +708,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 504a5e0..af47691 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, @@ -106,31 +121,83 @@ 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( 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 +205,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 +217,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, @@ -241,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)") @@ -253,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 ==") @@ -267,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") } @@ -300,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)}") } @@ -318,12 +436,45 @@ 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), 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 @@ -464,8 +615,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 { @@ -475,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 { @@ -513,6 +865,39 @@ 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 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", @@ -524,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 235f26f..05d0901 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 3534a68..53ea115 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 8943022..00c22f9 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/client/SshConnectionPacketClassificationTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/SshConnectionPacketClassificationTest.kt new file mode 100644 index 0000000..0354fc3 --- /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/client/sftp/SftpClientIntegrationTest.kt b/sshlib/src/test/kotlin/org/connectbot/sshlib/client/sftp/SftpClientIntegrationTest.kt index b603799..5ea18fa 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() 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 e5c9b79..abcf2e7 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 d9ccdb6..242e053 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,33 @@ 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 `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 c3d5b9d..508a6bd 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 @@ -27,10 +30,21 @@ INVARIANT NoHigherLayerPacketsSentDuringKex INVARIANT AuthenticationRequestIsGuarded INVARIANT AuthenticationRequestResponseClearsPending INVARIANT KexEventsAreStrictlySequenced +INVARIANT StrictKexProtectionSwitchesResetSequenceNumbers +INVARIANT StrictInitialKexRejectsNonKexPackets +INVARIANT StrictKexInitMustBeFirst +INVARIANT AcceptedInitialKexPacketOrderClearsHistory INVARIANT UserAuthenticationRequiresInitialNewKeys INVARIANT UnexpectedKexInitIsFatal +INVARIANT HostileKexReplyRequiresPossessionProof +INVARIANT NewKeysRequiresVerifiedTranscript +INVARIANT ProtectedHostilePacketsRequireTransportAuthentication +INVARIANT AuthenticationRequiresVerifiedTransport +INVARIANT HostileClientRolePacketsNeverAdvance +INVARIANT RejectedHostilePacketsDoNotEstablishSecurity 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 1f88d49..bc413ad 100644 --- a/sshlib/src/test/resources/tla/SshClientStateMachine.tla +++ b/sshlib/src/test/resources/tla/SshClientStateMachine.tla @@ -44,10 +44,24 @@ 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 /\ 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] @@ -123,10 +137,21 @@ ModelView == packetWasParsed, effects, rekeying, + strictKex, + nonKexBeforeInitialKexInit, authenticationEstablished, initialNewKeysActive, authRequestPending, previousAuthRequestPending, + inboundPacket, + lastInboundPacket, + inboundTranscriptMatches, + inboundHostSignatureValid, + inboundTransportValid, + hostKeyPossessionVerified, + transcriptVerified, + transportKeysVerified, + lastPacketDisposition, channels, NoInvalidChannelSideEffects, ChannelIsolation>> @@ -194,7 +219,8 @@ AuthenticationRequestResponseClearsPending == ~authRequestPending KexEventsAreStrictlySequenced == - /\ event = "ReceiveKexInit" => + /\ event \in {"ReceiveInitialStrictKexInit", "ReceiveInitialNonStrictKexInit", "ReceiveRekeyKexInit"} /\ + "Disconnect" \notin effects => /\ previousState = "WaitKexInit" /\ state = "WaitKex" /\ "SendKexExchangeInit" \in effects @@ -202,6 +228,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 +238,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 => @@ -225,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 3bdf542..5aa5ea9 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: 882c266edfb2fed9a28f79bc2ce7a5d343d87371ecfc9c9ca2ff42c467ed0a5f -\* Lifecycle states: 11; transitions: 36. +\* 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, 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", "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", "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", "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", "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" @@ -185,10 +187,21 @@ Init == /\ packetWasParsed = FALSE /\ effects = {} /\ rekeying = FALSE + /\ strictKex = FALSE + /\ nonKexBeforeInitialKexInit = FALSE /\ authenticationEstablished = FALSE /\ 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" @@ -198,6 +211,10 @@ Init == AUTHENTICATION_FAILURE == /\ state \in {"Authenticating"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"UserauthFailure"} + /\ inboundTransportValid + ) /\ state' = "AuthenticationReady" /\ previousState' = state /\ history' = history @@ -206,10 +223,21 @@ AUTHENTICATION_FAILURE == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"AuthenticationFailure"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -219,6 +247,10 @@ AUTHENTICATION_FAILURE == AUTHENTICATION_SUCCESS == /\ state \in {"Authenticating"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"UserauthSuccess"} + /\ inboundTransportValid + ) /\ state' = "Authenticated" /\ previousState' = state /\ history' = history @@ -227,10 +259,21 @@ AUTHENTICATION_SUCCESS == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"AuthenticationSuccess"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = TRUE /\ 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" @@ -240,6 +283,10 @@ AUTHENTICATION_SUCCESS == AUTHORIZE_AUTHENTICATED_PACKET == /\ state \in {"Authenticated"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"ConnectionPacket", "ClientConnectionPacket"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -248,10 +295,21 @@ AUTHORIZE_AUTHENTICATED_PACKET == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -261,6 +319,10 @@ AUTHORIZE_AUTHENTICATED_PACKET == AUTHORIZE_AUTHENTICATION_PACKET == /\ state \in {"Authenticating"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"UserauthMethodSpecific"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -269,10 +331,21 @@ AUTHORIZE_AUTHENTICATION_PACKET == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -282,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 @@ -290,10 +367,21 @@ AUTHORIZE_CONNECTION_PACKET == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -303,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 @@ -311,10 +403,21 @@ AUTHORIZE_POST_AUTH_EXT_INFO == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -324,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 @@ -332,10 +439,21 @@ AUTHORIZE_SERVICE_EXT_INFO == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -354,10 +472,21 @@ BEGIN_AUTHENTICATION == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"SendUserauthRequest"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -375,10 +504,21 @@ CONNECT == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"SendVersion"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -388,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 @@ -396,10 +540,21 @@ DISCONNECT == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"Disconnect"} /\ rekeying' = FALSE + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -417,10 +572,21 @@ OPEN_CHANNEL == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"SendChannelOpen"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -430,6 +596,10 @@ OPEN_CHANNEL == RECEIVE_CHANNEL_FAILURE == /\ state \in {"Authenticated"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"ChannelRequestReply"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -438,10 +608,21 @@ RECEIVE_CHANNEL_FAILURE == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveChannelFailure"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -451,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 @@ -459,10 +644,21 @@ RECEIVE_CHANNEL_OPEN_CONFIRMATION == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveChannelOpenConfirmation"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -472,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 @@ -480,10 +680,21 @@ RECEIVE_CHANNEL_OPEN_FAILURE == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveChannelOpenFailure"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -493,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 @@ -501,10 +716,21 @@ RECEIVE_CHANNEL_SUCCESS == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveChannelSuccess"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -514,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 @@ -522,10 +752,21 @@ RECEIVE_DEBUG == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"Debug"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -535,6 +776,10 @@ RECEIVE_DEBUG == RECEIVE_GLOBAL_REQUEST == /\ state \in {"Authenticated"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"GlobalRequest"} + /\ inboundTransportValid + ) /\ state' = state /\ previousState' = state /\ history' = history @@ -543,10 +788,21 @@ RECEIVE_GLOBAL_REQUEST == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveGlobalRequest"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -556,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 @@ -564,10 +824,21 @@ RECEIVE_IGNORE == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"Ignore"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -578,18 +849,109 @@ 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 /\ 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 /\ 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" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_INITIAL_NON_STRICT_KEX_INIT == + /\ state \in {"WaitKexInit"} + /\ ~(rekeying) + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) + /\ 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 + /\ 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" + /\ channelOrigin' = "None" + /\ channels' = channels + /\ channelEffects' = {} + +RECEIVE_INITIAL_STRICT_KEX_INIT == + /\ state \in {"WaitKexInit"} + /\ (~(rekeying)) /\ (~(nonKexBeforeInitialKexInit)) + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) + /\ 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 + /\ 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" @@ -599,6 +961,10 @@ RECEIVE_INITIAL_NEW_KEYS == RECEIVE_KEX_DH_GEX_GROUP == /\ state \in {"WaitKex"} + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexGexGroup"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ state' = "WaitKexDhGexInit" /\ previousState' = state /\ history' = history @@ -607,10 +973,21 @@ RECEIVE_KEX_DH_GEX_GROUP == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"SendKexDhGexInit"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -620,18 +997,35 @@ 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' = {"ReceiveKexDhGexReply", "SendNewKeys"} + /\ effects' = IF strictKex THEN {"ActivateOutboundProtection", "ReceiveKexDhGexReply", "ResetOutboundSequence", "SendNewKeys", "VerifyHostKeyPossession", "VerifyKexTranscript"} ELSE {"ActivateOutboundProtection", "ReceiveKexDhGexReply", "SendNewKeys", "VerifyHostKeyPossession", "VerifyKexTranscript"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -641,18 +1035,35 @@ 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' = {"ReceiveKexDhReply", "SendNewKeys"} + /\ effects' = IF strictKex THEN {"ActivateOutboundProtection", "ReceiveKexDhReply", "ResetOutboundSequence", "SendNewKeys", "VerifyHostKeyPossession", "VerifyKexTranscript"} ELSE {"ActivateOutboundProtection", "ReceiveKexDhReply", "SendNewKeys", "VerifyHostKeyPossession", "VerifyKexTranscript"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -662,18 +1073,35 @@ 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' = {"ReceiveKexEcdhReply", "SendNewKeys"} + /\ effects' = IF strictKex THEN {"ActivateOutboundProtection", "ReceiveKexEcdhReply", "ResetOutboundSequence", "SendNewKeys", "VerifyHostKeyPossession", "VerifyKexTranscript"} ELSE {"ActivateOutboundProtection", "ReceiveKexEcdhReply", "SendNewKeys", "VerifyHostKeyPossession", "VerifyKexTranscript"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -681,20 +1109,36 @@ RECEIVE_KEX_ECDH_REPLY == /\ channels' = channels /\ channelEffects' = {} -RECEIVE_KEX_INIT == +RECEIVE_REKEY_KEX_INIT == /\ state \in {"WaitKexInit"} + /\ rekeying + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) /\ 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 /\ 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" @@ -705,18 +1149,35 @@ RECEIVE_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 /\ 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 /\ 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" @@ -726,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 @@ -734,10 +1199,21 @@ RECEIVE_SERVICE_ACCEPT == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveServiceAccept", "StartAuthentication"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -747,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 @@ -755,10 +1235,21 @@ RECEIVE_USERAUTH_BANNER_AUTHENTICATING == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveUserauthBanner"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -768,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 @@ -776,10 +1271,21 @@ RECEIVE_USERAUTH_BANNER_READY == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveUserauthBanner"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -789,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 @@ -797,10 +1307,21 @@ RECEIVE_USERAUTH_INFO_REQUEST == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveUserauthInfoRequest"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -818,10 +1339,21 @@ RECEIVE_VERSION == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"ReceiveVersion", "SendKexInit"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -829,6 +1361,175 @@ 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 + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = hostKeyPossessionVerified + /\ transcriptVerified' = transcriptVerified + /\ transportKeysVerified' = transportKeysVerified + /\ lastPacketDisposition' = "Client" + /\ 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 + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = FALSE + /\ lastPacketDisposition' = "Client" + /\ 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 + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = FALSE + /\ lastPacketDisposition' = "Client" + /\ 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 + /\ inboundPacket' = inboundPacket + /\ lastInboundPacket' = lastInboundPacket + /\ inboundTranscriptMatches' = inboundTranscriptMatches + /\ inboundHostSignatureValid' = inboundHostSignatureValid + /\ inboundTransportValid' = inboundTransportValid + /\ hostKeyPossessionVerified' = FALSE + /\ transcriptVerified' = FALSE + /\ transportKeysVerified' = FALSE + /\ lastPacketDisposition' = "Client" + /\ 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) + /\ (inboundPacket = "None" + \/ /\ inboundPacket \in {"KexInit"} + /\ (~initialNewKeysActive \/ inboundTransportValid) + ) + /\ 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 + /\ 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" + /\ 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,10 +1540,21 @@ REKEY_STARTED == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"RekeyStarted", "SendKexInit"} /\ rekeying' = TRUE + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -861,10 +1573,21 @@ REPEAT_BEGIN_AUTHENTICATION == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"SendUserauthRequest"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -882,10 +1605,21 @@ SEND_CHANNEL_REQUEST == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"SendChannelRequest"} /\ rekeying' = rekeying + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -895,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 @@ -903,10 +1641,21 @@ UNEXPECTED_KEX_INIT_WAIT_KEX == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"Disconnect", "SendProtocolError"} /\ rekeying' = FALSE + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -916,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 @@ -924,10 +1677,21 @@ 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 /\ 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" @@ -937,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 @@ -945,10 +1713,21 @@ UNEXPECTED_KEX_INIT_WAIT_NEW_KEYS == /\ packetWasParsed' = (origin' = "ParsedPacket") /\ effects' = {"Disconnect", "SendProtocolError"} /\ rekeying' = FALSE + /\ strictKex' = strictKex + /\ nonKexBeforeInitialKexInit' = nonKexBeforeInitialKexInit /\ authenticationEstablished' = authenticationEstablished /\ 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" @@ -956,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 @@ -976,17 +1922,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 @@ -994,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 0000000..f01c84f --- /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 0000000..1ddcd7f --- /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 0000000..07a1ef7 --- /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 diff --git a/sshlib/src/test/resources/tla/SshTerrapin.tla b/sshlib/src/test/resources/tla/SshTerrapin.tla new file mode 100644 index 0000000..9a06977 --- /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 0000000..152a46c --- /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 0000000..d497e94 --- /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