On the Formal Modeling of Inductive Verification for Cryptographical Protocols

This paper addresses a formal modeling issue in the inductive verification approach for crypto graphical protocols. In the formalization of the inductive semantics of a protocol, the knowledge of an agent over a trace is not faithful to the intuition of the inductive approach to formally model a protocol. We find that the agent does not know the fresh items which he originates if the item is encrypted by a public key which he do not hold. We present a novel formal characterization of traces to solve the problem.