Logic Analysis And Design Of Cryptographic Protocols

In secure distributed systems it is essential that principals could prove their identities to each other and establish a session key. Authentication protocols are used to ensure authentication and related purposes, but the design of authentication protocols is error pone. It is a valuable filed on how to find out the flaws of a cryptographic protocols and how to design the correct protocol in various environments There are various methods that bave been proposed and applied to the analysis of cryptographic protocols. Among those methods , the best known and most influential one is that developed by Burows , Abadi, Needhani, commonly known as BAN-logic. This is due to its simplicity and efficiency. The main research work and results on the designing and analyzing of cryptographic protocol are as follows: ?The weakness of the BAN-logic is presented, the method of protocol idealization is made perfect. ?The attacks of message replay are classified, The parallel attack is discussed from the semantics, and the method of decision is presented. ?Two attacks on the TMN-protocol is sho~red, and an improved TMN-protocol is given. ?Some errors m BAN-Logic is pointed out, a modified version of the BAN-logic, which has a sound semantics and correct logic rules , is also presented, that is some new BAN-logic semantics and rules are presented, its language has , apart from the constructs taken from BAN, a few additional constructs. ?A classification of types of barter schemes is developed, and new cryptographic protocols for multi-item exchange with fairness are presented, These protocols assume the presence of a 搒emi-trusted neutral party? ?The properties of lottery and micro-lottery is discussed, two protocols of lottery and micro-lottery are presented, in which the result of the lottery is determined by the ticket number purchased. These protocols are the applications of a cryptographic component-bit commitment.