Abstract: This paper proposes a new method of security protocol design using theorem proven and security protocol analyzer. It constructs full information items based on requirement to gets a redundancy protocol firstly, and then uses theorem proven to prove the security of the designed protocol. It reduces the redundancy protocol step by step, using the reduce rules supported by theorem proven, until it gets optimized protocols which meet the requirement of protocol. The method can realize auto-design of security protocol and has good extension for design rules and reduce rules.