Suppose one have to design handshake protocol using known secure cryptographic algorithm. The designer of implementer can assume that crypotography is secure but how would they ensure protocol itself is secure. so far, I can think of few way to go about it but not sure if I am on the right path intuition wise.
1) Have the protocol as close as possible to well know protocol like TLS. So we will benefit from any discovery of weakness.
2) Use symbolic modeling. So far I know of tools like Proverif and Tamarin but not sure how widely they are used in industry. I know Tamarin was used in verification of TLS 1.3. This allow more flexibility in protocol design but symbolic modeling will not find any side channel attack.