--- the Dolev-Yao intruder specialized for Needham-Schroeder

(reset)
in needham-schroeder2.msr
in dolev-yao.msr
(
module ns2-dolevyao
import needham-schroeder2 * .
import dolev-yao * .
export * .

privK: princ -> type.
pubK  P <: knowledge.
privK P <: knowledge.

PDC: {
  PDC: forall A: princ. forall k: pubK A. forall k': privK A. forall t: msg.
    I(encrypt k t), I(k') => I(t).
}

PEC: {
  PEC: forall A: princ. forall k: pubK A. forall t: msg.
    I(t), I(k) => I(encrypt k t).
}

IPB: {
  IPB: forall A: princ. forall k: pubK A.
    empty => I(k).
}

i: princ.
privK-i: privK i.
pubK-i: pubK i.

config START-1 A, START-2 B, I(privK-i).

)