Как использовать NuSMV, чтобы засвидетельствовать атаку "человек посередине" (протокол Нидхэма-Шредера)?

Question

Как использовать NuSMV, чтобы засвидетельствовать атаку "человек посередине" (протокол Нидхэма-Шредера)?

У меня есть следующий упрощенный протокол Нидхэма-Шредера с открытым ключом:

A → B: {Na, A} Kb
B → A: {Na, Nb} Ka
A → B: {Nb} Kb

где Na, Nb одноразовые A, B, а также Ka, Kb являются открытыми ключами A, B соответственно.

Сообщения, зашифрованные открытым ключом стороны, могут быть расшифрованы только стороной.

На этапе (1) A инициирует протокол, отправив одноразовый номер и его идентификатор (зашифрованный B открытый ключ) B, Используя свой закрытый ключ, B расшифровывает сообщение и получает A личность.
На этапе (2) B посылает A и его одноразовые номера (зашифрованы A открытый ключ) вернуться к A, Используя свой закрытый ключ, A декодирует сообщение и проверяет, что его одноразовый номер возвращается.
На этапе (3) A возвращается B одноразовый номер (зашифрован B открытый ключ) вернуться к B,

Вот основная атака по середине к вышеуказанному упрощенному протоколу:

(1А) A → E: {Na, A} Ke (A хочет поговорить с E)
(1B) E → B: {Na, A} Kb (E хочет убедить B что это A)
(2В) B → E: {Na, Nb} Ka (B возвращает одноразовые номера в зашифрованном виде Ka)
(2A) E → A: {Na, Nb} Ka (E пересылает зашифрованное сообщение A)
(3A) A → E: {Nb} Ke (A подтверждает, что разговаривает с E)
(3B) E → B: {Nb} Kb (E возвращается B одноразовый обратно)

Я надеюсь, что когда атака была обнаружена, было предложено исправление для предотвращения атаки (B отправляет свою личность вместе с одноразовыми номерами обратно A):

A → B: {Na, A} Kb
B → A: {Na, Nb, B} Ka (B отправляет свою личность вместе с одноразовыми номерами обратно A)
A → B: {Nb} Kb

Вопросы:

Как я могу написать формулу LTL и модуль NuSMV eve смоделировать атакующего и стать свидетелем атаки "человек посередине"?
Как предотвратить атаку?

Процесс Алисы (А):

MODULE alice (in0, in1, inkey, out0, out1, outkey)
VAR
    st : { request, wait, attack, finish };
    nonce : { NONE, Na, Nb, Ne };
ASSIGN
    init (st) := request;
    next (st) := case
        st = request                        : wait;
        st = wait & in0 = Na & inkey = Ka   : attack;
        st = attack                         : finish;
        TRUE                                : st;
    esac;

    init (nonce) := NONE;
    next (nonce) := case
        st = wait & in0 = Na & inkey = Ka : in1;
        TRUE                              : nonce;
    esac;

    init (out0) := NONE;
    next (out0) := case
        st = request : Na;
        st = attack  : nonce;
        TRUE         : out0;
    esac;

    init (out1) := NOONE;
    next (out1) := case
        st = request : Ia;
        st = attack  : NOONE;
        TRUE         : out1;
    esac;

    init (outkey) := NOKEY;
    next (outkey) := case
        st = request : { Kb };
        TRUE         : outkey;
    esac;
FAIRNESS running;

Процесс Боб (B):

MODULE bob (in0, in1, inkey, out0, out1, outkey)
VAR
    st : { wait, receive, confirm, done };
    nonce : { NONE, Na, Nb, Ne };
    other : { NOONE, Ia, Ib, Ie };
ASSIGN
    init (st) := wait;
    next (st) := case
        st = wait & in0 = Na & in1 = Ia & inkey = Kb       : receive;
        st = wait & in0 = Ne & in1 = Ie & inkey = Kb       : receive;
        st = receive                                       : confirm;
        st = confirm & in0 = Nb & in1 = NOONE & inkey = Kb : done;
        TRUE                                               : st;
    esac;

    init (nonce) := NONE;
    next (nonce) := case
        st = wait & in0 = Na & in1 = Ia & inkey = Kb : in0;
        st = wait & in0 = Ne & in1 = Ie & inkey = Kb : in0;
        TRUE                                         : nonce;
    esac;

    init (other) := NOONE;
    next (other) := case
        st = wait & in0 = Na & in1 = Ia & inkey = Kb : in1;
        st = wait & in0 = Ne & in1 = Ie & inkey = Kb : in1;
        TRUE                                         : other;
    esac;

    init (out0) := NONE;
    next (out0) := case
        st = confirm : nonce;
        TRUE         : out0;
    esac;

    init (out1) := NONE;
    next (out1) := case
        st = confirm : Nb;
        TRUE         : out1;
    esac;

    init (outkey) := NOKEY;
    next (outkey) := case
        st = confirm & other = Ia : Ka;
        st = confirm & other = Ie : Ke;
        TRUE                      : outkey;
    esac;
FAIRNESS running;

Процесс основной:

MODULE main 
VAR
    a_in0 : { NONE, Na, Nb, Ne };
    a_in1 : { NONE, Na, Nb, Ne };
    a_out0 : { NONE, Na, Nb, Ne };
    a_out1 : { NOONE, Ia, Ib, Ie };
    a_inkey : { NOKEY, Ka, Kb, Ke };
    a_outkey : { NOKEY, Ka, Kb, Ke };
    a : process alice (a_in0, a_in1, a_inkey, a_out0, a_out1, a_outkey);
    b : process bob (a_out0, a_out1, a_outkey, a_in0, a_in1, a_inkey);
FAIRNESS running;

LTLSPEC F (a.st = finish & b.st = done)

Большое спасибо!

1

encryption model-checking nusmv

Источник

user7095660 08 дек '17 в 08:10

1 ответ

Решение

Другие вопросы по тегам encryption model-checking nusmv

user6024122 17 дек '17 в 02:20 2017-12-17 02:20 · Accepted Answer · 2017-12-17 02:20

(примечание: моделирование и проверка системы, которую вы имеете в виду, с помощью другого инструмента (например,SpinилиSTIATE Toolkit) было бы намного проще.)

Алиса и Боб.

Здесь мы моделируем тип user который ведет себя честно, прозрачно и что в вашем сценарии использования может быть реализовано как Alice или же Bob,

В качестве упрощения я жестко закодировал тот факт, что если user является Alice затем он инициирует протокол, пытаясь связаться с другим объектом.

Входы my_nonce, my_id а также my_key определить userЛичность, тогда как other_key а также other_id представлять общедоступную информацию о других user мы хотим связаться с. входные in_1, in_2 а также in_k так же, как в вашем примере кода, тогда как in_3 зарезервировано для обмена третьим значением, используемым в исправленной версии протокола.

user может быть в одном из пяти состояний:

IDLE: начальное состояние, Alice инициирует протокол, тогда как Bob ждет некоторого запроса.
WAIT_RESPONSE: когда Alice ждет ответа ей request
WAIT_CONFIRMATION: когда Bob ждет подтверждения его response
OK: когда Alice а также Bob рукопожатие прошло успешно
ERROR: когда что-то идет не так в рукопожатии (например, неожиданные входные данные)

Пользователь может выполнить одно из следующих действий:

SEND_REQUEST: {Na, IA} Kb
SEND_RESPONSE: {Na, Nb} Ka
SEND_CONFIRMATION: {Nb} Kb

В качестве упрощения, аналогично вашей собственной модели, я сделал выходные значения постоянными при нескольких переходах вместо того, чтобы сразу же возвращать их в NONE, Таким образом, мне не нужно добавлять дополнительные переменные, чтобы отслеживать входные значения, прежде чем они будут сброшены.

MODULE user(patched, my_nonce, my_id, my_key, other_key, other_id, in_1, in_2, in_3, in_k)
VAR
    state  : { IDLE, WAIT_RESPONSE, WAIT_CONFIRMATION, OK, ERROR };
    action : { NONE, SEND_REQUEST, SEND_RESPONSE, SEND_CONFIRMATION };
    out_1  : { NONE, NA, NB, NE, IA, IB, IE };
    out_2  : { NONE, NA, NB, NE, IA, IB, IE };
    out_3  : { NONE, NA, NB, NE, IA, IB, IE };
    out_k  : { NONE, KA, KB, KE };

INIT
    state = IDLE & action = NONE & out_1 = NONE
    & out_2 = NONE & out_3 = NONE & out_k = NONE;

-- protocol actions defining outputs
TRANS
    next(action) = SEND_REQUEST -> (
        next(out_1) = my_nonce & next(out_2) = my_id &
        next(out_3) = NONE     & next(out_k) = other_key
    );

TRANS
    ((next(action) = SEND_RESPONSE) & patched) -> (
        next(out_1) = in_1     & next(out_2) = my_nonce &
        next(out_3) = my_id    & next(out_k) = other_key
    );

TRANS
    ((next(action) = SEND_RESPONSE) & !patched) -> (
        next(out_1) = in_1     & next(out_2) = my_nonce &
        next(out_3) = NONE     & next(out_k) = other_key
    );

TRANS
    next(action) = SEND_CONFIRMATION -> (
        next(out_1) = in_2     & next(out_2) = NONE &
        next(out_3) = NONE     & next(out_k) = other_key
    );

-- outputs stabilization: easier modeling
TRANS
    next(action) = NONE -> (
        next(out_1) = out_1    & next(out_2) = out_2 &
        next(out_3) = out_3    & next(out_k) = out_k
    );

-- protocol life-cycle
TRANS
case
    -- protocol: end-positions
    (action = NONE &
     state = ERROR)
                        : next(action) = NONE &
                          next(state) = ERROR;
    (action = NONE &
     state = OK)
                        : next(action) = NONE &
                          next(state) = OK;

    -- protocol: send request
    (action = NONE &
     state = IDLE &
     my_id = IA)
                        : next(action) = SEND_REQUEST &
                          next(state) = WAIT_RESPONSE;

    -- protocol: handle request
    (action = NONE &
     state = IDLE &
     in_k = my_key)
                        : next(action) = SEND_RESPONSE &
                          next(state) = WAIT_CONFIRMATION;

    -- protocol: handle response
    -- without patch
    (action = NONE &
     state = WAIT_RESPONSE &
     in_k = my_key &
     in_1 = my_nonce &
     !patched)
                        : next(action) = SEND_CONFIRMATION &
                          next(state) = OK;
    -- with patch
    (action = NONE &
     state = WAIT_RESPONSE &
     in_k = my_key &
     in_1 = my_nonce &
     in_3 = other_id &
     patched)
                        : next(action) = SEND_CONFIRMATION &
                          next(state) = OK;

    -- protocol: handle confirmation
    (action = NONE &
     state = WAIT_CONFIRMATION &
     in_k = my_key &
     in_1 = my_nonce)
                        : next(action) = NONE &
                          next(state) = OK;

    -- protocol: no change state while performing action
    (action != NONE)
                        : next(action) = NONE &
                          next(state) = state;

    -- protocol: no state change if no valid input
    (action = NONE &
     in_k != my_key)
                        : next(action) = NONE &
                          next(state) = state;

    -- sink error condition for malformed inputs
    TRUE
                        : next(action) = NONE &
                          next(state) = ERROR;
esac;

Мы добавляем очень простой main модуль и простой CTL свойство проверить это Alice а также Bob вести себя ожидаемым образом и способны завершить рукопожатие в обычных условиях:

MODULE main
VAR
    a1 : process user(FALSE, NA, IA, KA, KB, IB, b1.out_1, b1.out_2, b1.out_3, b1.out_k);
    b1 : process user(FALSE, NB, IB, KB, KA, IA, a1.out_1, a1.out_2, a1.out_3, a1.out_k);

FAIRNESS running;


CTLSPEC ! EF (a1.state = OK & b1.state = OK);

Вывод следующий:

NuSMV > reset; read_model -i ns01.smv ; go ; check_property             
...
-- specification !(EF (a1.state = OK & b1.state = OK))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    a1.state = IDLE
    a1.action = NONE
    a1.out_1 = NONE
    a1.out_2 = NONE
    a1.out_3 = NONE
    a1.out_k = NONE
    b1.state = IDLE
    b1.action = NONE
    b1.out_1 = NONE
    b1.out_2 = NONE
    b1.out_3 = NONE
    b1.out_k = NONE
  -> Input: 1.2 <-
    _process_selector_ = main
    running = TRUE
    b1.running = FALSE
    a1.running = FALSE
  -> State: 1.2 <-
    a1.state = WAIT_RESPONSE
    a1.action = SEND_REQUEST
    a1.out_1 = NA
    a1.out_2 = IA
    a1.out_k = KB
  -> Input: 1.3 <-
  -> State: 1.3 <-
    a1.action = NONE
    b1.state = WAIT_CONFIRMATION
    b1.action = SEND_RESPONSE
    b1.out_1 = NA
    b1.out_2 = NB
    b1.out_k = KA
  -> Input: 1.4 <-
  -> State: 1.4 <-
    a1.state = OK
    a1.action = SEND_CONFIRMATION
    a1.out_1 = NB
    a1.out_2 = NONE
    b1.action = NONE
  -> Input: 1.5 <-
  -> State: 1.5 <-
    a1.action = NONE
    b1.state = OK

Алиса, Боб и Ева.

Чтобы смоделировать наш сценарий атаки, нам сначала нужно смоделировать attacker, Это очень похоже на Alice а также BobЕдинственное, что у него двойное inputs а также outputs так что он может общаться с обоими Alice а также Bob в то же время.

Его дизайн очень похож на Alice а также Bobтак что я не буду тратить на это много слов. В качестве упрощения я удалил проверку ошибок на attacker, поскольку у него фактически нет какой-либо значимой причины сбоя в рассматриваемом сценарии использования. Невыполнение этого условия усложнит код без уважительной причины.

MODULE attacker(my_nonce, my_id, my_key, a_key, b_key,
    ain_1, ain_2, ain_3, ain_k,
    bin_1, bin_2, bin_3, bin_k)
VAR
    state  : { IDLE, WAIT_RESPONSE, WAIT_CONFIRMATION, OK, ERROR };
    action : { NONE, SEND_REQUEST, SEND_RESPONSE, SEND_CONFIRMATION };
    aout_1  : { NONE, NA, NB, NE, IA, IB, IE };
    aout_2  : { NONE, NA, NB, NE, IA, IB, IE };
    aout_3  : { NONE, NA, NB, NE, IA, IB, IE };
    aout_k  : { NONE, KA, KB, KE };
    bout_1  : { NONE, NA, NB, NE, IA, IB, IE };
    bout_2  : { NONE, NA, NB, NE, IA, IB, IE };
    bout_3  : { NONE, NA, NB, NE, IA, IB, IE };
    bout_k  : { NONE, KA, KB, KE };

INIT
    state = IDLE & action = NONE &
        aout_1 = NONE & aout_2 = NONE & aout_3 = NONE & aout_k = NONE &
        bout_1 = NONE & bout_2 = NONE & bout_3 = NONE & bout_k = NONE;

-- protocol actions defining outputs
TRANS
    -- attacker: forward A secrets to B
    next(action) = SEND_REQUEST -> (
        next(aout_1) = NONE    & next(aout_2) = NONE  &
        next(aout_3) = NONE    & next(aout_k) = NONE  &
        next(bout_1) = ain_1   & next(bout_2) = ain_2 &
        next(bout_3) = ain_3   & next(bout_k) = b_key
    );

TRANS
    -- attacker: forward B response to A (cannot be unencripted)
    next(action) = SEND_RESPONSE -> (
        next(aout_1) = bin_1   & next(aout_2) = bin_2 &
        next(aout_3) = bin_3   & next(aout_k) = bin_k &
        next(bout_1) = NONE    & next(bout_2) = NONE  &
        next(bout_3) = NONE    & next(bout_k) = NONE
    );

TRANS
    -- attacker: send confirmation to B
    next(action) = SEND_CONFIRMATION -> (
        next(aout_1) = NONE    & next(aout_2) = NONE &
        next(aout_3) = NONE    & next(aout_k) = NONE &
        next(bout_1) = ain_1   & next(bout_2) = NONE &
        next(bout_3) = NONE    & next(bout_k) = b_key
    );

-- outputs stabilization: easier modeling
TRANS
    next(action) = NONE -> (
        next(aout_1) = aout_1  & next(aout_2) = aout_2 &
        next(aout_3) = aout_3  & next(aout_k) = aout_k &
        next(bout_1) = bout_1  & next(bout_2) = bout_2 &
        next(bout_3) = bout_3  & next(bout_k) = bout_k
    );

-- attack life-cycle
TRANS
case
    -- attack: end-positions
    (action = NONE &
     state = ERROR)
                        : next(action) = NONE &
                          next(state) = ERROR;
    (action = NONE &
     state = OK)
                        : next(action) = NONE &
                          next(state) = OK;

    -- attack: handle request, send forged request
    (action = NONE &
     state = IDLE &
     ain_k = my_key)
                        : next(action) = SEND_REQUEST &
                          next(state) = WAIT_RESPONSE;

    -- attack: handle response, forward undecryptable response
    (action = NONE &
     state = WAIT_RESPONSE &
     bin_k = a_key)
                        : next(action) = SEND_RESPONSE &
                          next(state) = WAIT_CONFIRMATION;

    -- attack: handle confirmation, send confirmation
    (action = NONE &
     state = WAIT_CONFIRMATION &
     ain_k = my_key)
                        : next(action) = SEND_CONFIRMATION &
                          next(state) = OK;

    -- attack: simple catch-all control no error checking
    TRUE
                        : next(action) = NONE &
                          next(state) = state;
esac;

Опять же, мы добавляем очень простой main модуль и простой CTL свойство проверить это Eve способен успешно атаковать Alice а также Bob.. в конце концов, Alice думает разговаривать с Eve (как есть) и Bob думает разговаривать с Alice когда он действительно разговаривает с Eve,

MODULE main
VAR
    a2 : process user(FALSE, NA, IA, KA, KE, IE, e2.aout_1, e2.aout_2, e2.aout_3, e2.aout_k);
    b2 : process user(FALSE, NB, IB, KB, KA, IA, e2.bout_1, e2.bout_2, e2.bout_3, e2.bout_k);
    e2 : process attacker(NE, IE, KE, KA, KB,
                          a2.out_1, a2.out_2, a2.out_3, a2.out_k,
                          b2.out_1, b2.out_2, b2.out_3, b2.out_k);

FAIRNESS running;


CTLSPEC ! EF (a2.state = OK & b2.state = OK & e2.state = OK);

Вывод следующий:

NuSMV > reset; read_model -i ns02.smv ; go ; check_property
...
-- specification !(EF ((a2.state = OK & b2.state = OK) & e2.state = OK))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    a2.state = IDLE
    a2.action = NONE
    a2.out_1 = NONE
    a2.out_2 = NONE
    a2.out_3 = NONE
    a2.out_k = NONE
    b2.state = IDLE
    b2.action = NONE
    b2.out_1 = NONE
    b2.out_2 = NONE
    b2.out_3 = NONE
    b2.out_k = NONE
    e2.state = IDLE
    e2.action = NONE
    e2.aout_1 = NONE
    e2.aout_2 = NONE
    e2.aout_3 = NONE
    e2.aout_k = NONE
    e2.bout_1 = NONE
    e2.bout_2 = NONE
    e2.bout_3 = NONE
    e2.bout_k = NONE
  -> Input: 1.2 <-
    _process_selector_ = main
    running = TRUE
    e2.running = FALSE
    b2.running = FALSE
    a2.running = FALSE
  -> State: 1.2 <-
    a2.state = WAIT_RESPONSE
    a2.action = SEND_REQUEST
    a2.out_1 = NA
    a2.out_2 = IA
    a2.out_k = KE
  -> Input: 1.3 <-
  -> State: 1.3 <-
    a2.action = NONE
    e2.state = WAIT_RESPONSE
    e2.action = SEND_REQUEST
    e2.bout_1 = NA
    e2.bout_2 = IA
    e2.bout_k = KB
  -> Input: 1.4 <-
  -> State: 1.4 <-
    b2.state = WAIT_CONFIRMATION
    b2.action = SEND_RESPONSE
    b2.out_1 = NA
    b2.out_2 = NB
    b2.out_k = KA
    e2.action = NONE
  -> Input: 1.5 <-
  -> State: 1.5 <-
    b2.action = NONE
    e2.state = WAIT_CONFIRMATION
    e2.action = SEND_RESPONSE
    e2.aout_1 = NA
    e2.aout_2 = NB
    e2.aout_k = KA
    e2.bout_1 = NONE
    e2.bout_2 = NONE
    e2.bout_k = NONE
  -> Input: 1.6 <-
  -> State: 1.6 <-
    a2.state = OK
    a2.action = SEND_CONFIRMATION
    a2.out_1 = NB
    a2.out_2 = NONE
    e2.action = NONE
  -> Input: 1.7 <-
  -> State: 1.7 <-
    a2.action = NONE
    e2.state = OK
    e2.action = SEND_CONFIRMATION
    e2.aout_1 = NONE
    e2.aout_2 = NONE
    e2.aout_k = NONE
    e2.bout_1 = NB
    e2.bout_k = KB
  -> Input: 1.8 <-
  -> State: 1.8 <-
    b2.state = OK
    e2.action = NONE

Исправлена Алиса, Боб и Ева.

К счастью, я уже прокрался исправленную версию Alice а также Bob в коде, который я уже показал. Итак, все, что осталось сделать, это проверить, соответствует ли патч желаемому поведению, написав новый main что сочетает в себе Alice, Bob а также Eve все вместе:

MODULE main
VAR
    a3 : process user(TRUE, NA, IA, KA, KE, IE, e3.aout_1, e3.aout_2, e3.aout_3, e3.aout_k);
    b3 : process user(TRUE, NB, IB, KB, KA, IA, e3.bout_1, e3.bout_2, e3.bout_3, e3.bout_k);
    e3 : process attacker(NE, IE, KE, KA, KB,
                          a3.out_1, a3.out_2, a3.out_3, a3.out_k,
                          b3.out_1, b3.out_2, b3.out_3, b3.out_k);

FAIRNESS running;


CTLSPEC ! EF (a3.state = OK & b3.state = OK & e3.state = OK);
CTLSPEC ! EF (a3.state = ERROR & b3.state = ERROR);

Вывод следующий:

NuSMV > reset; read_model -i ns03.smv ; go ; check_property             
...
-- specification !(EF ((a3.state = OK & b3.state = OK) & e3.state = OK))  is true
-- specification !(EF (a3.state = ERROR & b3.state = ERROR))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    a3.state = IDLE
    a3.action = NONE
    a3.out_1 = NONE
    a3.out_2 = NONE
    a3.out_3 = NONE
    a3.out_k = NONE
    b3.state = IDLE
    b3.action = NONE
    b3.out_1 = NONE
    b3.out_2 = NONE
    b3.out_3 = NONE
    b3.out_k = NONE
    e3.state = IDLE
    e3.action = NONE
    e3.aout_1 = NONE
    e3.aout_2 = NONE
    e3.aout_3 = NONE
    e3.aout_k = NONE
    e3.bout_1 = NONE
    e3.bout_2 = NONE
    e3.bout_3 = NONE
    e3.bout_k = NONE
  -> Input: 1.2 <-
    _process_selector_ = main
    running = TRUE
    e3.running = FALSE
    b3.running = FALSE
    a3.running = FALSE
  -> State: 1.2 <-
    a3.state = WAIT_RESPONSE
    a3.action = SEND_REQUEST
    a3.out_1 = NA
    a3.out_2 = IA
    a3.out_k = KE
  -> Input: 1.3 <-
  -> State: 1.3 <-
    a3.action = NONE
    e3.state = WAIT_RESPONSE
    e3.action = SEND_REQUEST
    e3.bout_1 = NA
    e3.bout_2 = IA
    e3.bout_k = KB
  -> Input: 1.4 <-
  -> State: 1.4 <-
    b3.state = WAIT_CONFIRMATION
    b3.action = SEND_RESPONSE
    b3.out_1 = NA
    b3.out_2 = NB
    b3.out_3 = IB
    b3.out_k = KA
    e3.action = NONE
  -> Input: 1.5 <-
  -> State: 1.5 <-
    b3.action = NONE
    e3.state = WAIT_CONFIRMATION
    e3.action = SEND_RESPONSE
    e3.aout_1 = NA
    e3.aout_2 = NB
    e3.aout_3 = IB
    e3.aout_k = KA
    e3.bout_1 = NONE
    e3.bout_2 = NONE
    e3.bout_k = NONE
  -> Input: 1.6 <-
  -> State: 1.6 <-
    a3.state = ERROR
    e3.action = NONE
  -> Input: 1.7 <-
  -> State: 1.7 <-
    e3.state = OK
    e3.action = SEND_CONFIRMATION
    e3.aout_1 = NONE
    e3.aout_2 = NONE
    e3.aout_3 = NONE
    e3.aout_k = NONE
    e3.bout_1 = NA
    e3.bout_k = KB
  -> Input: 1.8 <-
  -> State: 1.8 <-a
    b3.state = ERROR
    e3.action = NONE

Первое свойство подтверждает, что атака не удалась и рукопожатие не завершено ни Alice ни Bob так как Eve не выполняет это. Второе свойство показывает, как предпринята атака и как она проваливается на практике.