Formal Specification of Security Protocols

Needham R M, Schroeder N D. Using encryption for authentication in large network of computers[J].Communications of the ACM.1978, 21(12):993-999[2]Steiner J G, Neuman B C, Schiller J I. Kerberos: an authentication service for open network systems. In Usenix Conference Proceedings, Dallas, Texas, 1988: 191-202.[3]CCITT. CCITT Recommendation X.509, The directory authentication framework, version 7,1987.[4]Owre S, Rushby J, Shankar N, Henke F. Formal verification for fault-tolerant architectures:Prolegomena to the design of PVS. IEEE Trans. on Software Engineering, 1995, SE-21(2): 107-125.[5]Paulson L. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 1998, 6(1): 85-128.[6]Millen J.[J].H. Rue. Protocol-independent secrecy. In 2000 IEEE Symposium on Security and Privacy, Oakland California, USA, IEEE Computer Society Press.2000,:-[7]Lowe G. A hierarchy of authentication specifications. In Proc. of The 10th Computer Security Foundations Workshop, Rockport, Massachusetts, USA, IEEE Computer Society Press, 1997:31-43.[8]Burrows M, Abadi M, Needham R. A logic of authentication[J].ACM Trans. on Computer Systems.1990, 8(1):18-36[9]Guttman J D, Thayer F J. Authentication tests. In 2000 IEEE Symposium on Security and Privacy, Oakland, California, USA, IEEE Computer Society Press, 2000: 96-109.[10]Roscoe A W. Modeling and verifying key-exchange protocols using CSP FDR. In Proc. of the 1995 IEEE Computer Security Foundations Workshop IIX, Dromquinna Manor, Kenmare,County Kerry, Ireland, IEEE Computer Society Press, 1995: 98-107.[11]Thayer J, Herzog J, Guttman J. Strand spaces: Why is a security protocol correct? In Proc. of the 1998 Symposium on Security and Privacy, Oakland California, USA, IEEE Computer Society Press, 1998: 160-171.[12]Paulson L. Isabelle: A Generic Theorem Prover. Berlin, New York: Springer, 1994.[13]胡成军,郑援,沈昌祥.密码协议的秘密性证明.计算机学报,2003,26(3):367-372.