Temporal logics of knowledge are useful for reasoning about situations where we require both dynamic aspects and informational aspects relating to knowledge. So, the application of temporal logics of knowledge is investigated to the specification and verification the properties of TLS protocol. Two main properties of TLS are given out. And the definitions and lemmas for the proof of these properti...Show More
