The question is about "formal" analysis, proofs, etc... What is a correct definition of a formal proof, or a formal analysis? Is there a good way and a bad way to formally prove something. What is the meaning of a a "semi-formal" proof, "semi-formal" argument.
$\begingroup$
$\endgroup$
3
-
1$\begingroup$ "Formal" usually means "mathematically correct". $\endgroup$– dkaeaeFeb 6, 2019 at 16:34
-
1$\begingroup$ @dkaeae Not really. An informal argument can be perfectly correct, while a completely formal proof can have an error making it incorrect. $\endgroup$– MaeherFeb 6, 2019 at 19:22
-
1$\begingroup$ - A formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference (Wiki..) $\endgroup$– kelalakaFeb 6, 2019 at 21:27
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
2
You may want to check the answers to this question. As the question (and answers) point out, it is not rare to find people use "formal proof" to refer to proofs generated using computer-aided means.
However, as some comments to your question also point out, a "formal" proof of something strictly means a mathematical proof showing that all the claimed (security) properties are met. This can be done using computer-aided tools, but not necessarily. The term provable cryptography refers to a major area in cryptography which deals with the main techniques to create such proofs (not necessarily -and not usually- computer-aided tools). See, for instance, this entry in the Wikipedia for some further insight and references.
About "semi-formal" proofs: I guess that it refers to proofs that do not go down to the full detail, and just set out the overall approach and leave some (or all) parts as sketches. This means that while they may overlook some things, such "semi-formal" proofs point towards the right direction to build a formal proof.
-
$\begingroup$ Thank you. In which type fall game-bases proofs, which consists to rewrite a game as a sequence of games, and then to determine a inequality to bound the advantage of the original game. Is this a formal proof? $\endgroup$– Adam54Feb 7, 2019 at 9:18
-
$\begingroup$ It is a formal type of proof in the sense that it is used to give mathematical demonstrations of the desired properties. As such, it is also a technique very commonly used in provable cryptography. But that does not mean that there are no computer-aided tools compatible with this technique. $\endgroup$– GinswichFeb 7, 2019 at 10:06