「暗号プロトコルを形式的に記述し，その枠組みのもとで安全性を検証することが広く研究されてきました．そういったやり方は『形式的手法』と呼ばれます．
この，『形式的』という言葉について，『形だけのこと』という，どちらかというと否定的な意味合いは入っておらず，対象を何らかの形で，たいていは数学的に，定式化することをいいます．
例えば，対称暗号における暗号化と復号の関係は，d( x, e( x, y ) ) → yという式で表すことができます．xを鍵，yを平文に対応づけると，平文yを鍵xで暗号化eしてできる暗号文e ( x, y )，を鍵xで復号dすると，右辺のとおり，平文yが得られる，というわけです．
『安全性検証』というのは，既存の，または自分で安全であると主張したいような，暗号プロトコルの仕様を用意しまして，枠組に沿うよう記述したのち，論証などを通じて安全である，または安全でないことを，導きます．
そういった暗号プロトコルの仕様ありきではなく，ある枠組で設計すると，その暗号プロトコルは安全なのですよと言えてしまう，というアプローチもあります．
そんなやり方で得られたものは，『安全性が証明可能な暗号プロトコル』なんて言い方をします．
ホワイトボードに，いくつか英単語を書いていきましょう．まず，『証明』は…
Proof
と書いて，『プルーフ』ですね．
動詞の『証明する』にするには，終わりの2文字を書き換えます．
Prove
これで発音は，『プローヴ』と言いたいところですが，『プルーヴ』です．ちなみに情報通信技術では『プロウブ』と発音する単語(probe)もよく出てきます．それはさておき…
さらに書き換えます．『証明可能な』という形容詞形にします．こうです．
Provable
『プルーヴァブル』という言い方になります．
末尾をもう少し変えれば，副詞形になります．
Provably
そしてこの単語が，Secureという形容詞を修飾します．
Provably Secure
これが，『安全性が証明可能な』の英語表現です．
ここで1文字だけ変えると，意味ががらりと変わります．
Probably Secure
直訳すると『たぶん安全』です．安全性をきちんと証明・説明できないということになりまして，安全のレベルはガタ落ちです．
1文字違いで大違い．くれぐれも注意しましょう」
（最終更新：2016-07-18 朝）
