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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
PeerJ Inc.
2023-03-01
|
| Series: | PeerJ Computer Science |
| Subjects: | |
| Online Access: | https://peerj.com/articles/cs-1284.pdf |