如何使用NuSMV见证中间人攻击(Needham-Schroeder协议)? [英] How to use NuSMV to witness the man-in-the-middle attack (Needham-Schroeder protocol)?

查看：307 发布时间：2020/6/30 23:52:39 encryption model-checking nusmv

本文介绍了如何使用NuSMV见证中间人攻击(Needham-Schroeder协议)?的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！

问题描述

我有以下简化的公钥Needham-Schroeder协议:

I have the following simplified public-key Needham-Schroeder protocol:

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

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

其中，Na，Nb是A，B和Ka的现时，Kb分别是A，B的公钥.

where Na, Nb are the nonces of A, B, and Ka, Kb are the public keys of A, B respectively.

使用一方公钥加密的邮件只能由该方解密.

Messages encrypted by a party’s public key can only be decrypted by the party.

在步骤(1)中，A通过将随机数及其标识(由B的公钥加密)发送给B来启动协议. B使用其私钥来解密邮件并获取A的身份.

At Step (1), A initiates the protocol by sending a nonce and its identity (encrypted by B’s public key) to B. Using its private key, B deciphers the message and gets A’s identity.

在步骤(2)中，B将A和它的现时值(由A的公钥加密)发送回A. A使用其私钥对消息进行解码并检查其现时是否已返回.

At Step (2), B sends A’s and its nonces (encrypted by A’s public key) back to A. Using its private key, A decodes the message and checks its nonce is returned.

在步骤(3)中，A将B的随机数(由B的公钥加密)返回给B.

At Step (3), A returns B’s nonce (encrypted by B’s public key) back to B.

这是上述简化协议的中间人攻击:

(1A)A → E: {Na, A} Ke(A想和E交谈)
(1B)E → B: {Na, A} Kb(E要说服B它是A)
(2B)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的现时值)

(1A) A → E: {Na, A} Ke (A wants to talk to E)
(1B) E → B: {Na, A} Kb (E wants to convince B that it is A)
(2B) B → E: {Na, Nb} Ka (B returns nonces encrypted by Ka)
(2A) E → A: {Na, Nb} Ka (E forwards the encrypted message to A)
(3A) A → E: {Nb} Ke (A confirms it is talking to E)
(3B) E → B: {Nb} Kb (E returns B’s nonce back)

我希望当发现攻击时，提出了一个修复程序来阻止攻击(B将其身份和现时值发送回A):

I hope that when the attack was found, a fix was proposed to prevent the attack (B sends its identity along with the nonces back to A):

A → B: {Na, A} Kb
B → A: {Na, Nb, B} Ka(B将其身份和随机数发送回A)
A → B: {Nb} Kb

A → B: {Na, A} Kb
B → A: {Na, Nb, B} Ka (B sends its identity along with the nonces back to A)
A → B: {Nb} Kb

问题是:

如何编写LTL公式和NuSMV模块eve建模攻击者并见证中间人攻击?
如何防止攻击?

How can I write an LTL formula and a NuSMV module eve to model the attacker and witness the man-in-the middle attack?
How to prevents the attack?

alice(A)的过程:

The process of alice(A):

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;

bob(B)的过程

The process of bob(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;

主要过程:

The process of main:

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)

非常感谢！

推荐答案

(注意:使用其他工具(例如 STIATE Toolkit )会更简单.)

爱丽丝和鲍勃.

在这里，我们对user的类型进行建模，该类型以诚实，透明的方式运行，并且在您的用例中可以实例化为Alice或Bob.

Here we model the type of user that behaves in a honest, transparent manner and that in your use-case can be instantiated as either Alice or Bob.

为简化起见，我对如果user是Alice的事实进行了硬编码，那么它将通过尝试与其他实体联系来启动协议.

As a simplification, i hard-coded the fact that if the user is Alice then it will initiate the protocol by trying to contact the other entity.

输入my_nonce，my_id和my_key定义了user的身份，而other_key和other_id表示有关我们要联系的其他user的公开信息.和.输入in_1，in_2和in_k就像您的代码示例一样，而in_3保留用于交换协议的修补版本中使用的第三个值.

The inputs my_nonce, my_id and my_key define a user's identity, whereas other_key and other_id represent the publicly available information about the other user we want to get in touch with. Inputs in_1, in_2 and in_k are just like in your code example, whereas in_3 is reserved for exchanging the third value used in the patched version of the protocol.

user可以处于以下五个状态之一:

A user can be in one of five states:

IDLE:初始状态，Alice将启动协议，而Bob等待某些请求.
WAIT_RESPONSE:Alice等待对其request
WAIT_CONFIRMATION:当Bob等待对他的response
OK:Alice和Bob握手成功后
ERROR:当握手出现问题时(例如意外输入)

IDLE: initial state, Alice will initiate the protocol whereas Bob waits for some request.
WAIT_RESPONSE: when Alice waits to a response to her request
WAIT_CONFIRMATION: when Bob waits to a confirmation to his response
OK: when Alice and Bob handshake has been successful
ERROR: when something goes wrong in the handshake (e.g. unexpected inputs)

用户可以执行以下操作之一:

A user can perform one of the following actions:

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

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

为简化起见，类似于您自己的模型，我使输出值在多个转换中保持不变，而不是立即将其返回到NONE.这样，在重置输入值之前，我不必添加额外的变量来跟踪输入值.

As a simplification, similarly to your own model, I made output values persistent along several transitions instead of putting them back immediately to NONE. In this way, I don't have to add extra variables to keep track of input values before they are resetted.

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的行为是否符合预期，并能够在正常情况下完成握手:

We add a very simple main module and a simple CTL property to check that Alice and Bob behave in the expected way and are able to complete the handshake in normal circumstances:

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进行通信.

In order to model our attack scenario, we first need to model the attacker. This is very similar to Alice and Bob, only that it has double inputs and outputs so that it can communicate with both Alice and Bob at the same time.

它的设计与Alice和Bob的设计非常相似，因此我不会在上面花很多字.为简化起见，我删除了attacker上的所有错误检查，因为在考虑用例的情况下，它实际上没有任何有意义的原因导致失败.否则，没有充分的理由会使代码复杂化.

Its design is very similar to that of Alice and Bob, so I won't spend many words on it. As a simplification, i removed any error checking on the attacker, since it does not actually have any meaningful reason to fail in the use-case scenario being considered. Not doing so would complicate the code for no good reason.

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对话.

Again, we add a very simple main module and a simple CTL property to check that Eve is able to successfully attack Alice and Bob.. at the end of it, Alice thinks to be talking to Eve (as it is) and Bob thinks to be talking with Alice when it's truly talking with 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和Eve.

幸运的是，我已经在已经显示的代码中潜行了Alice和Bob的已修补版本.因此，剩下要做的就是通过编写将Alice，Bob和Eve组合在一起的新main来检查补丁是否符合所需的行为:

Luckily, I already sneaked the patched version of Alice and Bob in the code that I have already shown. So, all that it remains to do is to check that the patch meets the desired behavior by writing a new main that combines Alice, Bob and Eve together:

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无法实现.第二个属性显示如何如何进行攻击以及在实践中如何失败.

The first property confirms that the attack fails and the handshake is not completed for neither Alice nor Bob because Eve does not fulfil it. The second property shows how the attack is attempted and how it fails in practice.

这篇关于如何使用NuSMV见证中间人攻击(Needham-Schroeder协议)?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！

查看全文

如何使用NuSMV见证中间人攻击(Needham-Schroeder协议)? [英] How to use NuSMV to witness the man-in-the-middle attack (Needham-Schroeder protocol)?

问题描述

推荐答案

相关文章

其他开发最新文章

热门教程

热门工具

登录关闭

如何使用NuSMV见证中间人攻击(Needham-Schroeder协议)? [英] How to use NuSMV to witness the man-in-the-middle attack (Needham-Schroeder protocol)?

问题描述

推荐答案

相关文章

其他开发最新文章

热门教程

热门工具

登录 关闭

登录关闭