Verifying security protocols using theorem provers(Algebras, Languages, Computations and their Applications)
Miki Tanaka · Institutional Repositories DataBase (IRDB) · 2007
This is a report on a project in formal verification of cryptographic protocol.We adapt Paulson's work of verification of TLS (Transport Security Layer) on $Isabelle/HOL[1]$ to the proof-assistant Coq.Paulson's trace model of TLS is translated into the Coq syntax and the proofs of security properties are explicitly constructed on the Coq system.