Cargando…

Transport Layer Security 1.0 handshake protocol formal verification case study: How to use a proof script generator for existing large proof scores

The Transport Layer Security (TLS) 1.0 protocol has been formally verified with CafeInMaude Proof Generator (CiMPG) and Proof Assistant (CiMPA), where CafeInMaude is the second major implementation of CafeOBJ, a direct successor of OBJ3, a canonical algebraic specification language. The properties c...

Descripción completa

Detalles Bibliográficos
Autores principales: Tran, Duong Dinh, Wai Mon, Thet, Ogata, Kazuhiro
Formato: Online Artículo Texto
Lenguaje:English
Publicado: PeerJ Inc. 2023
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC10280648/
https://www.ncbi.nlm.nih.gov/pubmed/37346581
http://dx.doi.org/10.7717/peerj-cs.1284