Modeling for security verification of a cryptographic protocol with MAC payload

Abstract

We propose a new sub-term relation to specify syntax of messages with MAC (Message Authentication Code) payload for the cryptographic protocols in the strand space model. The sub-term relation was introduced to formal analysis of cryptographic protocols based on theorem proving, but some defects have been found in it. In the present paper, first, the operator f is defined to the extend sub-term relation, which is used to amend its original flaws. Second, a new ideal is constructed, and is used to expand the bounds on the penetrator's abilities. Third, the decidable theorem for honesty of ideals holds as it is described under the extended sub-term relation is proved. Fourth, we propose the theorem of the satisfiability for decidable conditions of honest ideals and annotate how invariant-sets generate, which is used to verify security properties of cryptographic protocols. © Springer-Verlag Berlin Heidelberg 2005.