Управление
Кликните по подсвеченному переходу или жмите «Шаг» — сработает первый разрешённый переход.
Розовая заливка означает, что переход разрешён в текущей маркировке.
Сеть Петри
Текущая маркировка
M = (1, 1, 0, 0, 0, 0)
Граф достижимости
Если маркировка
P6 = 1 достижима, атакующий успешно перехватил учётные данные —
модель подтверждает возможность атаки. Модель позволяет проверить контрмеры: добавление позиции
«WIDS активен» и перехода, сбрасывающего отравленный ARP-кеш.
Формальное описание
N = (P, T, F, W, M₀)
P = {P1, P2, P3, P4, P5, P6} — позиции
T = {T1, T2, T3, T4} — переходы
F ⊆ (P×T) ∪ (T×P) — дуги
W: F → ℕ — кратность дуг (все 1)
M₀ = (1, 1, 0, 0, 0, 0) — начальная маркировка
Переход t разрешён, если ∀p ∈ •t : M(p) ≥ W(p, t)
Срабатывание: M'(p) = M(p) − W(p, t) + W(t, p)| Переход | Входы (•t) | Выходы (t•) | Смысл |
|---|---|---|---|
T1 | — | P3 | Атакующий занимает позицию |
T2 | P1, P2, P3 | P4 | ARP-отравление прошло успешно |
T3 | P4 | P5 | Трафик перенаправлен через атакующего |
T4 | P5 | P6 | Захват учётных данных |
Задание
- Перечислите все достижимые маркировки из начальной M₀ — сравните с выводом графа выше.
- Добавьте в модель позицию P7 «WIDS обнаружил аномалию» и переход T5, сбрасывающий P4 в P1, P2. Как изменится множество достижимых состояний?
- Оцените вероятность успеха атаки, если каждое из срабатываний T2–T4 успешно с вероятностью 0.7, а T1 — с вероятностью 1.0.
- Постройте аналогичную сеть Петри для атаки DNS-спуфинга и сравните структуру.