[Avispa-users] Modeling resilient channels in HLPSL (correction)

[Jorge López]

Dear all,

Sorry for the last mail. I interpreted badly the attack trace. The receiver
wasn't executing the recovery protocol, she was just following the normal
flow of the main one.

However, the attack still remains (with cl-atse backend), and I guess that
may be due to the LTL formulas. The recovery protocol is not being executed
by the receiver, though it should, as a timeout should be raised since the
receiver is not obtaining the last expected item. Is it possible that, once
the EOR is known by the origin agent, the LTL formula is evaluated and thus
considered unfulfilled?

For a better comprehension of the situation, I indicate the transitions for
the receiver:

%Main subprotocol
      0.    State      = 0     /\ RCV_R_SCE(POO')
                                      /\ POO'     =
{Pub_sce.Pub_tce.Pub_r.Pub_s.Msg'.Label'.Tpl_id}_inv(Pub_sce) =|>
             State' := 1        /\ POR'    :=
{Pub_sce.Pub_tce.Pub_r.Pub_s.Msg'.Label'.Tpl_id}_inv(Pub_r)
                                      /\ SND_R_TCE(POO'.POR')
                                      /\ witness(R,TCE,tce_r_por,POR')
                                      /\ wrequest(R,SCE,r_sce_poo,POO')

      1.    State      = 1     /\ RCV_R_TCE(NRO')
                                      /\ NRO'  =
{Pub_sce.Pub_tce.Pub_r.Pub_s.POR}_inv(Pub_tce) =|>
             State' := 2        /\ NRR'    := {NRO'}_inv(Pub_r)
                                      /\ SND_R_SCE(NRR')
                                      /\ witness(R,SCE,sce_r_nrr,NRR')
                                     /\ wrequest(R,TCE,r_tce_nro,NRO')

      2.     State    = 2     /\ RCV_R_SCE(NRA')
                                     /\ NRA'     = {NRR}_inv(Pub_sce) =|>
             State' := 3      /\ wrequest(R,SCE,r_sce_nra,NRA')
                                    /\ aknows(R,receiver,NRA')

      3.    State    = 1     --|>
             State' := 4

        % Recovery subprotocol
        4.    State    = 2     --|>
              State' := 5    /\ SND_R_S(POO.POR.NRO.NRR)

        % - Protocol successfully recovered
        5.   State    = 5     /\ RCV_R_S(NRA_TTP')
                                     /\ NRA_TTP'     = {NRR}_inv(Pub_s) =|>
             State' := 6       /\ aknows(R,receiver,NRA_TTP')

        % - Protocol already aborted by origin
        6.    State    = 5    /\ RCV_R_S(Abort_TTP')
                                     /\ Abort_TTP'     =
{{abort.Label}_inv(Pub_sce)}_inv(Pub_s) =|>
            State' := 7        /\ aknows(R,receiver,Abort_TTP')

        % Loop...
        7.    State    = 5    --|>
               State' := 2

The steps shown in the attack trace contained in the previous email
indicated that the receiver had executed steps 0 and 1, going to state 2.
However, step 4 (recovery subprotocol execution) is not launched...

LTL formulas for non-repudiation properties are the next:

[] (((aknows(SCE,sce,NRA) \/ aknows(SCE,sce,NRA_TTP)) \/
aknows(SCE,sce,Abort_TTP)) =>
   ((aknows(R,receiver,NRA) \/ aknows(R,receiver,NRA_TTP)) \/
aknows(R,receiver,Abort_TTP)))

[] (((aknows(R,receiver,NRA) \/ aknows(R,receiver,NRA_TTP)) \/
aknows(R,receiver,Abort_TTP)) =>
   ((aknows(SCE,sce,NRA) \/ aknows(SCE,sce,NRA_TTP)) \/
aknows(SCE,sce,Abort_TTP)))

At the end of the attack trace, agent sce has (and then knows) item NRA_TTP,
while agent receiver got nothing.

Again, thanks for any help.

Jorge.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mail63.csoft.net/pipermail/avispa-users/attachments/20091031/9ec1b659/attachment.htm