Formal Methods and Protocol Verification
In computer science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically rigorous techniques for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing the appropriate mathematical analysis can contribute to the reliability and robustness of a design.
Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particular logic calculi, formal languages, automata theory, discrete event dynamic system and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification.
I recently learnt that The Dolev-Yao model is a formal model used to prove properties of interactive cryptographic protocols.
I watched a video on using AVISPA with hlpsl tool to verify the working of cryptographic protocols.
Happy Learning Security!