Sound Automatic Implementation Generation and Monitoring of Security Protocol Implementations from Veried Formal Specications
A. Pironti, Riccardo Sisto, Pietro Laface · 2010
ing the Refined Model In this section it is shown that, under some conditions, if SYSTEM does not have security flaws, then SYSTEM ′ does not have any either. Like in the previous section, although by a technically different reasoning, it is shown in a first step that under some assumptions the refined SYSTEM ′ meets any security property that is satisfied by a more abstract, intermediate SYSTEM ∗. Note that this relation holds for any security property that can be defined on traces, provided that it is not defined on the send or receive events that may appear in a trace. Then, in a second step, it is shown that under further assumptions the intermediate SYSTEM ∗ can be further simplified to the original abstract SYSTEM , by applying a newly introduced simplifying transformation, that still preserves secrecy and authentication. In order to obtain the intermediate SYSTEM ∗, let us define privA , {priv sendA,priv receiveA} and the function f(·) that transforms P ′ A into P ∗ A , f(P ′ A). Informally, function f(·) removes events on the channels in privA without changing the external behavior of the process. Formally, f(·) can be defined as a function on CSP processes that distributes over any CSP operator ω but the action prefix operator, on which f(·) acts by removing the events in privA, that is • for any CSP operator ω, with any arity n, except action prefix: f(ω(P1, . . . ,Pn)) = ω(f(P1), . . . ,f(Pn)) • for the action prefix operator ev → P : if (ev / ∈ {receive?B.A} ∪ privA) ∨ (ev ∈ {receive?B.A} ∧ ∀ pev ∈ privA · P / = pev → P ′) then f(ev → P ) = ev → f(P )