[prev in list] [next in list] [prev in thread] [next in thread] 

List:       avispa-users
Subject:    [Avispa-users] Select from a field. Late decryption.
From:       laurent.vigneron () loria ! fr (Laurent Vigneron)
Date:       2008-02-26 15:37:18
Message-ID: 1204040238.47c4322ee441b () www ! loria ! fr
[Download RAW message or body]


Hi again,

For decomposing a message Msg received some steps before, you only have to write
in the left-hand side of the transition, in which you receive the key PK, that
Msg is equal to some signed information:

    2. State = 1 /\ RCV(...PK'...)
        /\ Msg = {N1'.N2'}_inv(PK')
       =|>
            State':= 2
            /\ SND(...N1'...)

Laurent.

[prev in list] [next in list] [prev in thread] [next in thread]