Analyzing Encryption Protocols Based on Temporal Logic
Xiao De · Chinese Journal of Computers · 2002
In order to develope a unified theory to verify encryption protocols. This paper provided a way to describe encryption protocols based on temporal logic from the main weakness and threats to encryption protocols. The protocol's actions,the intruder's actions and correctness requirements can be specified using temporal formulas under this model. All this analysis is specified according to standard safety properties,for which standard temporal logic proof techniques apply. In particular, authors model an encryption protocol where the intruder cannot obtain plaintexts by any logical or algebraic techniques. Comparing with relevant ones, it is a better formal way to describe encryption protocols. This scheme can be used widely,not only in analyzing traditional cryptosystem's,but also in describing public key cryptosystem's. In addition,it can also analyze other characteristics,such as the characteristics of fault-tolerance and no key to be reused.