1

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

  1. A → B: {Na, A} Kb
  2. B → A: {Na, Nb} Ka
  3. A → B: {Nb} Kb

其中Na,是, , 和Nb的随机数,分别是 的公钥。ABKaKbAB

由一方的公钥加密的消息只能由一方解密。

在步骤 (1)，A通过向 发送随机数及其身份（由B的公钥加密）来启动协议B。使用其私钥，B解密消息并获得A的身份。

在第 (2) 步，B将A's 及其随机数（由A's 的公钥加密）发送回A。使用它的私钥，A解码消息并检查它的随机数是否被返回。

在第 (3) 步，A将B的随机数（由B的公钥加密）返回给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( return 的 nonceE返回B)

我希望当发现攻击时，提出一个修复来防止攻击（B将其身份与随机数一起发送回A）：

  1. A → B: {Na, A} Kb
  2. B → A: {Na, Nb, B} Ka（B将其身份与随机数一起发送回A）
  3. A → B: {Nb} Kb

问题是：

  1. 如何编写 LTL 公式和 NuSMV 模块eve来对攻击者进行建模并见证中间人攻击？
  2. 如何防止攻击？

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)的过程：

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)

非常感谢！

4

1 回答 1

2

Spin（注意：使用其他工具（例如或）对您心目中的系统进行建模和验证STIATE Toolkit会简单得多。）

爱丽丝和鲍勃。

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

作为简化，我硬编码了这样一个事实，如果user是，Alice那么它将通过尝试联系其他实体来启动协议。

输入my_nonce和定义 a的身份，而my_id和代表我们想要联系的其他人的公开可用信息。Inputs和就像在您的代码示例中一样，而保留用于交换协议修补版本中使用的第三个值。my_keyuserother_keyother_iduserin_1in_2in_kin_3

Auser可以处于以下五种状态之一：

  • 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这与and非常相似Bob，只是它具有双重inputs和，outputs因此它可以同时与两者Alice通信Bob。

Alice它的设计与and的设计非常相似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 和 Eve。

幸运的是，我已经在我已经展示的代码中偷偷安装了和的补丁版本。所以，剩下要做的就是通过编写一个新的来检查补丁是否满足所需的行为，并结合在一起：AliceBobmainAliceBobEve

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没有完成它。第二个属性显示了攻击是如何尝试的以及它在实践中是如何失败的。

于 2017-12-17T02:20:01.467 回答