@MASTERSTHESIS\{IMM2007-05453,
    author       = "Q. Wang",
    title        = "Verification of Security Protocols Using A Formal Approach",
    year         = "2007",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    note         = "Supervised by Assoc. Prof. J{\o}rgen Villadsen, {IMM,} {DTU}.",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/5453-full.html",
    abstract     = "Security protocols are expected to build secure communications over vulnerable networks. However, security protocols may contain potential flaws. Therefore, they need formal verifications.

In this thesis, we investigate Paulson’s inductive approach and apply this formal approach to a classical cryptographic protocol which has not been previously verified in this way. We also investigate the modelling of timestamps and further extension of the inductive approach with message reception and agent’s knowledge. We modelled and verified Lowe’s modified Denning-Sacco sharedkey protocol using the inductive approach. The model and theorems are later updated with message reception and agent’s knowledge.

Theorem proving is supported by the interactive theorem prover Isabelle. We have completed the proofs for both versions. As a result, Lowe’s modified Denning-Sacco shared-key protocol has been formally verified using the inductive approach."
}