攻撃者の視点を導入すると今までとは少し毛色の変わった形で完全秘匿性と同値な命題を定式化することができます。それは模倣性(simulatability)という考えです。
攻撃者Aは暗号文を見て何かを出力する確率的アルゴリズムだとします。その動作は出力の確率分布として表されます。一方ある確率的アルゴリズムSが暗号文なしでAの動作を模倣できる、すなわち出力の確率分布が同じであるとします。その場合にはAがやっていることにとって暗号文の情報は全く意味がない、と言うことになるわけです。少し式を使って（概念的に）書くとA(Enc(k, m))=SならばAは暗号文から情報を取り出すことに失敗しているといえます。このように暗号文なしでAを模倣できるSが存在する、という性質を完全模倣性と言います。
安永先生の本暗号理論入門ではこの概念を以下のように定式化しています。
p20 定義2.3 完全模倣性
共通鍵暗号(Enc, Dec)が完全に模倣可能(perfectly simulatable)であるとは、任意の攻撃者Aに対し、ある確率分布$S_A$が存在して、任意の平文分布M及び値aに対して、
$$Pr[A(Enc_K(M))=a] = Pr[S_A = a]$$
を満たすことである。
確率分布SはAに依存してよいので$S_A$としていますがMには依存しません。
完全模倣性をLean4で形式化すると以下のように書けます。
def perfect_simulatability (Enc : K → M → C) (Gen : PMF K) : Prop :=
∀ (V : Type) (A : C → PMF V), ∃ (S : PMF V), ∀ (Msg : PMF M),
(do let c ← (cipher_dist Enc Gen Msg); A c) = S
ここでは攻撃者AはA : C → PMF Vとして定式化しています。Aへの入力は暗号文、出力の方はなんでも良くて、ただ確率的なのでPMF Vとしています。Sは入力なしでVを出力する確率分布PMF Vです。
この定義の面白いところは、Aは暗号文をcを渡されて一生懸命計算して出力するのですが、出力の確率分布は結局は暗号文を知らないSに真似されてしまうと言うことです。渡された暗号文cから攻撃者Aは情報を取り出そうとしますが手も足も出ません。
この完全模倣性と言う概念も実は完全秘匿性と同値です。すでに完全識別不可能性と完全秘匿性の同値は示しているので、完全模倣性と完全識別不可能性の同値が示れば良いわけです。
theorem perfect_indistinguishability_iff_perfect_simulatability [Inhabited M]
(Enc : K → M → C) (Gen : PMF K) :
perfect_indistinguishability Enc Gen ↔ perfect_simulatability Enc Gen
のLean4による証明では←はとても簡単で６行くらいで終わりました。ポイントは完全模倣性の攻撃者A : C → PMF VからV=Boolとして完全識別不可能性用の攻撃者を作ることです。
逆向きの証明はちょっと大変でした。実質35行くらい。一つのポイントはSの構成でした。適当に選んだ平文defaultを使って、
let S : PMF V := (do c←(Enc_dist Enc Gen default); A c)
としてSを構成し、それが任意の平文mについて(do c←(Enc_dist Enc Gen m); A c)と等しいことを言えば、証明は終了します。
