Encryption Protocol, A Method Of Analysis

In this dissertation we present a general,extensible methodology that examines cryptographic protocols.Our approach is specify a protocol in CPAL (Cryptographic Protocol Analysis Language) ,apply Hoare and Dijkstra抯 theory of formal semantics to it, analysis it抯 forma] semantics, define weakest precondition of each kind of language statement. We specify a statement of failure as postcondition, expend the relative axioms and use them try to prove weakest precondition, if the proving succeed, it means that the protocol suffer from an attack.