attempt test suite 2

tests/paper2.yaml

@@ -0,0 +1,127 @@
+unidirectional-drop-abp: 
+  - command: python src/main.py --model=tests/abp/abp.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: abp resists drop, see https://en.wikipedia.org/wiki/Alternating_bit_protocol
+
+bidirectional-drop-abp: 
+  - command: python src/main.py --model=tests/abp/abp.pml --attacker=drop --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: abp resists drop, see https://en.wikipedia.org/wiki/Alternating_bit_protocol
+
+# =============================================================================
+# TCP tests
+#
+# NOTE: The TCP model uses separate send/receive channel pairs
+# (AtoN[1], NtoA[0], BtoN[1], NtoB[0]) with no network forwarding process.
+# A sends on AtoN but B receives on NtoB; Korg's single-channel attacker
+# gadgets cannot bridge this gap. As a result, all single-channel attacks
+# are ineffective: consumed/replayed/reordered messages on AtoN never
+# reach B (and vice versa). Both TCP processes fall back to Closed via
+# timeout transitions, so all properties hold trivially or vacuously.
+#
+# This demonstrates a structural limitation: Korg's channel-local attackers
+# require that communicating processes share the attacked channel. A network
+# forwarding process (AtoN -> NtoB, BtoN -> NtoA) would be needed for
+# meaningful cross-channel attacks.
+# =============================================================================
+
+# phi1: safety - half-open prevention
+# always (leftClosed implies !rightEstablished)
+
+tcp-phi1-drop-AtoN:
+  - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: attacker consumes from AtoN but B reads NtoB; no messages are delivered cross-channel so neither side reaches Established, and phi1 holds trivially
+
+tcp-phi1-drop-bidirectional:
+  - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: dropping on both outbound channels still cannot affect the inbound rendezvous channels NtoA/NtoB; no handshake progress occurs
+
+tcp-phi1-replay-AtoN:
+  - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: replayed messages land back on AtoN, which only A writes to; B never reads AtoN so no half-open state can be manufactured
+
+tcp-phi1-replay-bidirectional:
+  - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: replaying on both outbound channels cannot bridge to the rendezvous inbound channels; property holds vacuously
+
+tcp-phi1-reorder-AtoN:
+  - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=reorder --chan=AtoN --output=temp.pml --eval --cleanup --mem=2
+  - intended: no violation
+  - explanation: reordering on AtoN is invisible to B; the channel architecture prevents any cross-channel effect
+
+tcp-phi1-reorder-bidirectional:
+  - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2
+  - intended: no violation
+  - explanation: reordering both outbound channels still cannot deliver messages to the inbound rendezvous channels
+
+# phi3: liveness - no infinite stalls/deadlocks
+
+tcp-phi3-drop-AtoN:
+  - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: timeout transitions in LISTEN and SYN_SENT return both processes to Closed; no permanent stall occurs because no cross-channel delivery happens
+
+tcp-phi3-drop-bidirectional:
+  - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: same as above; both sides cycle through Closed via timeout, preventing any permanent intermediate state
+
+tcp-phi3-replay-AtoN:
+  - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: replayed messages on AtoN do not reach B; both sides timeout-cycle through Closed, so no stall
+
+tcp-phi3-reorder-bidirectional:
+  - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2
+  - intended: no violation
+  - explanation: reordering cannot create stalls when messages never cross between the two TCP processes
+
+# phi5: liveness - SYN_RECEIVED resolution
+# SynReceived implies eventually (Established or FinWait1 or Closed)
+
+tcp-phi5-drop-AtoN:
+  - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: neither process enters SynReceived because no SYN is ever delivered cross-channel; the property holds vacuously
+
+tcp-phi5-drop-BtoN:
+  - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=BtoN --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: same as above; without cross-channel delivery, SynReceived is never entered
+
+tcp-phi5-replay-AtoN:
+  - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: replaying on AtoN cannot deliver a SYN to B via NtoB; SynReceived is never reached, so the property holds vacuously
+
+tcp-phi5-reorder-AtoN:
+  - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=reorder --chan=AtoN --output=temp.pml --eval --cleanup --mem=2
+  - intended: no violation
+  - explanation: reordering on AtoN has no cross-channel effect; property holds vacuously as SynReceived is unreachable
+
+# phi6: safety - strict closing transitions
+# Closing implies next(Closing or Closed)
+
+tcp-phi6-drop-AtoN:
+  - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=drop --chan=AtoN --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: Closing state is never reached without cross-channel message delivery; property holds vacuously
+
+tcp-phi6-replay-AtoN:
+  - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=replay --chan=AtoN --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: replay on AtoN cannot drive either process into Closing; property holds vacuously
+
+tcp-phi6-replay-bidirectional:
+  - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=replay --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: replaying on both outbound channels still cannot bridge to inbound rendezvous channels; Closing never entered
+
+tcp-phi6-reorder-bidirectional:
+  - command: python src/main.py --model=tests/tcp/tcp-phi6.pml --attacker=reorder --chan=AtoN,BtoN --output=temp.pml --eval --cleanup --mem=2
+  - intended: no violation
+  - explanation: reordering both outbound channels has no effect on the rendezvous inbound channels; Closing never entered