From panther-ivy-plugin
Use when working with NCT (compositional protocol testing), NACT (attack testing, security testing, APT lifecycle), or NSCT (simulation, Shadow NS, large-scale testing) methodology. Covers all three PANTHER formal testing methodologies.
How this skill is triggered — by the user, by Claude, or both
Slash command
/panther-ivy-plugin:methodology-referenceThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
This is the authoritative reference for all three PANTHER formal testing methodologies: NCT, NACT, and NSCT. All three share the same Ivy formal specification language, 14-layer template, and before/after monitor pattern. They differ in execution environment and testing focus.
This is the authoritative reference for all three PANTHER formal testing methodologies: NCT, NACT, and NSCT. All three share the same Ivy formal specification language, 14-layer template, and before/after monitor pattern. They differ in execution environment and testing focus.
NCT is a specification-based testing methodology where a formal Ivy protocol specification plays one role (client, server, or man-in-the-middle) against an Implementation Under Test (IUT). The specification generates test traffic via Z3/SMT symbolic execution and monitors received packets against formal assertions.
The Ivy tester's role is the opposite of what it tests:
{prot}_server_test_*.ivy files){prot}_client_test_*.ivy files){prot}_mim_test_*.ivy files)Protocol specs use monitors (before/after clauses) attached to protocol events:
Specifications use export to declare actions that the test mirror generates randomly:
export frame.ack.handle
export frame.stream.handle
export packet_event
export client_send_event
Z3/SMT solving ensures generated traffic complies with specification constraints.
Identify the protocol to test and the RFC(s) defining it. Extract testable requirements (MUST, SHOULD, MAY statements).
Map RFC sections to the 14-layer template. Minimum viable set:
Start with {prot}_types.ivy -- the foundation layer defining identifiers, bit vectors, enumerations used throughout the model.
Progress through layers in dependency order:
{prot}_frame.ivy) -- PDU definitions{prot}_packet.ivy) -- wire-level structure{prot}_protection.ivy) -- encryption/decryption{prot}_connection.ivy) -- session lifecycleCreate entity definitions for each protocol participant:
ivy_{prot}_client.ivy -- client instanceivy_{prot}_server.ivy -- server instanceEncode RFC requirements as before/after monitors in ivy_{prot}_{role}_behavior.ivy. This is the largest and most complex protocol-specific code.
Write role-specific test files:
#lang ivy1.7
include order
include {prot}_infer
include file
include ivy_{prot}_shim_client
include ivy_{prot}_client_behavior
after init {
# Initialize sockets, TLS, transport parameters
}
# Export actions for test mirror generation
export frame.ack.handle
export frame.stream.handle
export packet_event
# End-state verification
export action _finalize = {
require is_no_error;
require conn_total_data(the_cid) > 0;
}
Use ivy_verify MCP tool to verify formal properties: isolate assumptions, invariants, safety properties.
Use ivy_compile MCP tool with target=test to produce executable test binary.
Run compiled test against the implementation via PANTHER experiment framework.
| Step | Tool | Usage |
|---|---|---|
| Formal verification | ivy_verify | Check isolate/invariant/safety properties |
| Compile tests | ivy_compile | Build test executables (target=test) |
| Inspect model | ivy_model_info | View types, relations, actions, invariants |
| Fast structural lint | ivy_lint | Quick structural checks |
IMPORTANT: Always use ivy-tools MCP tools. Never run ivy_check, ivyc, ivy_show, or ivy_to_cpp directly via Bash.
protocol-testing/{prot}/
|-- {prot}_stack/ # Core protocol model (layers 1-9)
|-- {prot}_entities/ # Entity definitions and behavior
|-- {prot}_shims/ # Implementation bridge
|-- {prot}_utils/ # Serialization, utilities
+-- {prot}_tests/
|-- server_tests/ # Tests targeting server IUTs
|-- client_tests/ # Tests targeting client IUTs
+-- mim_tests/ # Man-in-the-middle tests
The QUIC model (protocol-testing/quic/) is the most complete NCT implementation with 50+ test variants covering: stream handling, connection close, retry, migration, transport parameter validation, error conditions, 0-RTT, congestion control, loss recovery, version negotiation, timeout handling.
Examine quic_server_test.ivy as the canonical test structure example.
| Rationalization | Reality |
|---|---|
| "I can skip the type layer" | Types are the foundation. Everything depends on them. |
| "Verification can wait until the end" | Verify after every meaningful change. Errors compound. |
| "I know this protocol well enough to skip the RFC" | RFC is the source of truth. Your memory is not. |
| "This monitor doesn't need a bracket tag" | Every assertion needs traceability. No exceptions. |
| "Role inversion doesn't matter for this test" | It always matters. Testing a server = Ivy acts as client. |
| "I'll add _finalize later" | Without _finalize, end-state properties are never checked. |
| "Direct ivy_check is faster" | MCP tools are required. The hook will block you anyway. |
Missing after init
after init block setting initial state for all relationsWrong role in test file name
quic_client_test_*.ivy but Ivy plays client role, creating confusionquic_server_test_*.ivy = testing the server.Missing bracket tags on assertions
[rfcNNNN:X.Y] comments, breaking traceabilityrequire/ensure/assert with its RFC section referenceNACT extends NCT to model and test protocols from an attacker's perspective. It uses the APT (Advanced Persistent Threat) lifecycle model to systematically test security properties of protocol implementations. Attack specifications use the same Ivy formal language and before/after monitor pattern as NCT but focus on adversarial behavior.
The attack lifecycle is organized into 3 phases with 6 stages plus a cross-cutting concern:
Phase 1: Infiltration
Reconnaissance (attack_reconnaissance.ivy) -- Gather information about the target. Passive (OSINT, social engineering, WHOIS, DNS queries) and active (port scanning, service enumeration, OS fingerprinting, banner grabbing).
launch_whois_lookup(), launch_dns_query(), endpoint_scanning(src, dst)Infiltration (attack_infiltration.ivy) -- Initial access to the target network. Exploit detected vulnerabilities to establish a foothold.
C2 Communication (attack_c2_communication.ivy) -- Establish command & control channels for remote control of compromised systems.
Phase 2: Expansion
4. Privilege Escalation (attack_privilege_escalation.ivy) -- Gain higher access levels within the compromised network.
attack_maintain_persistence.ivy) -- Maintain access to the compromised system across reboots and security updates.Phase 3: Extraction
6. Exfiltration (attack_exfiltration.ivy) -- Extract data from the target network.
Cross-cutting: White Noise (attack_white_noise.ivy) -- Distraction attacks to cover the primary attack operation.
The master file attack_life_cycle.ivy composes all stages:
#lang ivy1.7
include attack_white_noise
# Infiltration
include attack_reconnaissance
include attack_infiltration
include attack_c2_communication
# Expansion
include attack_privilege_escalation
include attack_maintain_persistence
# Extraction
include attack_exfiltration
NACT defines additional entity roles beyond NCT's client/server:
Entity definitions reside in apt_entities/ with behavioral constraints in apt_entities_behavior/.
| Protocol | Binding Directory | Description |
|---|---|---|
| QUIC | quic_apt_lifecycle/ | Maps attacks to QUIC connection manipulation |
| MiniP | minip_apt_lifecycle/ | Simplified protocol attack bindings |
| UDP | udp_apt_lifecycle/ | Basic datagram-level attacks |
| Stream Data | stream_data_apt_lifecycle/ | Stream-oriented attack bindings |
apt_entities/apt_entities_behavior/{prot}_apt_lifecycle/apt_tests/ivy_verify MCP tool for model consistencyivy_compile MCP tool for executablesprotocol-testing/apt/
|-- apt_entities/ # Attack entity definitions
|-- apt_entities_behavior/ # Attack entity behavioral constraints
|-- apt_lifecycle/ # 6-stage lifecycle definitions
| |-- attack_life_cycle.ivy # Master include file
| |-- attack_reconnaissance.ivy
| |-- attack_infiltration.ivy
| |-- attack_c2_communication.ivy
| |-- attack_privilege_escalation.ivy
| |-- attack_maintain_persistence.ivy
| |-- attack_exfiltration.ivy
| |-- attack_white_noise.ivy
| |-- quic_apt_lifecycle/ # QUIC-specific bindings
| |-- minip_apt_lifecycle/ # MiniP-specific bindings
| +-- udp_apt_lifecycle/ # UDP-specific bindings
|-- apt_network/ # Attack network infrastructure
|-- apt_protocols/ # Protocol-specific APT integration
|-- apt_shims/ # Attack implementation bridges
|-- apt_stack/ # Attack protocol stack layers
|-- apt_tests/ # Attack test specifications
+-- apt_utils/ # Attack utilities
| Rationalization | Reality |
|---|---|
| "I can skip the threat model definition" | Without a threat model, you're testing random behavior, not attacks. |
| "This attack doesn't need entity definitions" | Every attack needs attacker, target, and optionally bot/C2/MIM entities. |
| "I can reuse the NCT behavior files directly" | NACT requires adversarial monitors -- NCT monitors enforce compliance, not attacks. |
| "The APT stages don't apply to this protocol" | All 6 stages apply. Some may be trivial, but they must be considered. |
| "I'll add persistence modeling later" | Without persistence, the attack model is incomplete and unrealistic. |
Missing attack entity definitions
apt_entities/ with attack-specific state and capabilitiesConfusing NCT and NACT monitors
require (compliance check) instead of attack-specific constraintsNSCT is a compositional testing methodology that runs protocol verification in simulated network environments using the Shadow Network Simulator. It enables testing at scale with deterministic execution, complex topologies, and controlled network conditions -- complementing NCT's real-network testing.
Shadow NS provides deterministic network simulation within PANTHER:
NSCT uses PANTHER's experiment configuration with type: shadow_ns network environment:
tests:
- name: "NSCT Protocol Test"
network_environment:
type: shadow_ns
topology:
nodes:
- name: client_node
ip: "10.0.0.1"
- name: server_node
ip: "10.0.0.2"
links:
- source: client_node
target: server_node
latency: "50ms"
bandwidth: "10Mbit"
loss: "0.1%"
simulation:
duration: "60s"
seed: 42
services:
server:
implementation:
name: picoquic
type: iut
protocol:
name: quic
version: rfc9000
role: server
| Criterion | NCT (Real Network) | NSCT (Simulated) |
|---|---|---|
| Fidelity | High (real OS stack) | Medium (simulated stack) |
| Scale | Limited (container resources) | High (many simulated nodes) |
| Determinism | Non-deterministic | Deterministic |
| Topology control | Basic (Docker networks) | Full (arbitrary topologies) |
| Network conditions | Limited manipulation | Full control (latency, loss, bandwidth) |
| Debugging | Harder (non-deterministic) | Easier (deterministic replay) |
| Performance testing | Realistic | Simulated |
Choose NSCT when: testing under specific network conditions, testing at scale, needing deterministic reproducibility, exploring complex topologies, running regression tests.
Choose NCT when: needing realistic network stack behavior, testing actual performance, verifying against real-world conditions, final validation before deployment.
type: shadow_nspanther run --config <config.yaml>NSCT requires a specific Z3 build mode for Shadow NS compatibility:
build_mode: "" (empty string) in the PANTHER Ivy configmk_make.py build system compatible with Shadow NSdebug-asan, rel-lto, release-static-pgo) are for NCT/NACT Docker environments| Rationalization | Reality |
|---|---|
| "I can skip the simulation config" | Without proper topology, your simulation doesn't test what you think it tests. |
| "The same Docker build works for Shadow" | Shadow requires specific build modes. Use the right build_mode setting. |
| "Deterministic seeds don't matter for this test" | Determinism is Shadow's key advantage. Always set and document seeds. |
| "I don't need network condition modeling" | If you're not using latency/loss/bandwidth, why use Shadow at all? |
Wrong build mode
"" build mode for Shadow NS compatibilityMissing seed configuration
seed in the experiment YAML for Shadow runsA complete protocol verification campaign combines all three methodologies:
Each methodology shares the same Ivy formal specifications but applies them in different execution contexts, providing comprehensive coverage of protocol correctness, security, and robustness.
Related agents:
Related skills:
Related commands:
/nct-check -- Quick verification/nct-compile -- Compilation/nct-scaffold -- Protocol and test scaffolding/nct-review -- Comprehensive multi-agent reviewnpx claudepluginhub elniak/panther-ivy-plugin --plugin panther-ivy-pluginGenerates complete layered testing strategy (L1-L4 pyramid), plans, architecture, scenarios, code templates, and CI/CD configs for Backend+APP, Backend+WEB, or Backend+APP+Embedded projects.
Helps plan, write, review, execute, and maintain manual test cases with reproducible artifacts traceable to design documents.
Provides test attack patterns, coverage matrices, and reporting formats for structured testing strategies.