Definitions and Analysis of Integrity in Strand Spaces Model

Integrity of messages is an important security property of cryptographic protocols; however, strand spaces model cannot analyze it on account of its poor cryptographic primitives´ abstracts. The definition of component is extended to realize the more detailed description of messages; Abstracts of four mathematical operations are added to show the principle that applying digital signature or keyed hash function to protect integrity of messages in the real world; Penetrator strands are extended by adding three new strands that can summarize penetrator´ attacks on integrity of messages; New notions of Integrity and Integrity Set are defined and the relevant theorem and propositions are therefore proposed and proved. Due to the extension, strand spaces model for the first time is adaptive to analyze protocols with integrity protection such as NSM.