2.4.2 モジュール型

EasyCryptリファレンスマニュアルの非公式(かつガバガバな)訳です。
モジュール型って要するにインターフェースとかよばれるものですね。

EasyCryptのモジュール型は手続きの集合の型である。たとえば次のモジュール型ORを考えてみよう。

module type OR = {
  proc init (secret : int, tries : int) : unit
  proc guess(guess : int) : unit
  proc guessed() : bool
}.

ORは"guessing oracle"の最小要件を表している。すなわち少なくとも型がついた手続きを与えるものである。モジュール型においては手続きの順番は関係ない。手続きの型においては、次のように、複数の同じ型のパラメータをまとめることもできる。

proc init(secret tries : int) : unit

手続きのパラメータ名は純粋にドキュメントのためだけに使われるので、代わりにアンダースコアを使うことで省略することもできる。たとえば、

proc init(_ : int, _ : int) : unit

なお、モジュール型はモジュールが持つであろうグローバル変数については何も言っていない。モジュール型はモジュールとは異なる名前空間を持つ。

つぎの例はguessing oracleの実装を表す。

module Or' = {
  var sec : int
  var tris : int
  var guessed : bool

  proc init(secret, tries: int) : unit = {
    sec <- secret;
    tris <- tries;
    guessed <- false;
  }

  proc guess(guess : int) : unit = {
    if (0 < tris) {
      guessed <- guessed \/ (guess = sec);
      tris <- tris - 1;
    }
  }

  proc guessed() : bool = {
    return guessed;
  }
}.

手続きinitはグローバル変数secに与えられた秘密情報を格納し、グローバル変数trisを許された推測の回数で初期化し、グローバル変数guessedは「秘密情報がまだ当てられていない」ことの記録で初期化する。(省略) Orはモジュール型ORの要件を満たし、Orを宣言するときにモジュール型を渡すことで、EasyCryptにそれを確かめさせることができる。

module Or : OR = {
  var sec : int
  var tris : int
  var guessed : bool

  proc init(secret tries : int) : unit = {
    sec <- secret;
    tris <- tries;
    guessed <- false;
  }

  proc guess(guess : int) : unit = {
    if (0 < tris) {
      guessed <- guessed \/ (guess = sec);
      tris <- tris - 1;
    }
  }

  proc guessed() : bool = {
    return guessed;
  }
}.

モジュール型を渡すことはモジュールの宣言の結果に影響を与えない。たとえば、モジュール型ORからguessedを取り除いたとしても、Orは手続きguessedをもつことができる。さらには、モジュールを宣言するとき、EasyCryptに、複数のモジュール型を満たしているかどうかを確かめさせることができる。

module type A = { proc f() : unit }.
module type B = { proc g() : unit }.
module X: A, B = {
  var x, y : int
  proc f() : unit = { x <- x + 1; }
  proc g() : unit = { y <- y + 1; }
}.

モジュールのエイリアスを宣言したときには、EasyCryptにモジュールがモジュール型と合うかどうかを確かめさせることもできる。

module X' : A, B = X.

guessing oracleを使って暗号学的ゲームを宣言し、オラクルのguessにアクセスできる攻撃者でパラメータ化し、推測ゲームが行われる値域と、推測を行うという2つの手続きを与えたいとしよう。これは次のように書くことができる。

module type GAME = {
  proc main() : bool
}.

module Game(Adv: ADV) : GAME = {
  module A = Adv(OR)
  proc main() :bool = { ... }
}.

すなわち、攻撃者を表すモジュール型ADVはORの実装によってパラメータ化されなければならない。我々が念頭に置いている攻撃者の手続きを考えると、これに対する構文は、

module type ADV'(O: OR) = {
  proc chooseRange() : int * int
  proc doGuessing() : unit
}.

しかし、この定義は攻撃者にすべてのOの手続きにアクセスすることを許してしまう。これは望んでいない。代わりにこう書ける。

module type ADV''(O: OR) = {
  proc chooseRange() : int * int {}
  proc doGuessing() : unit {O.guess}
}.

これは、choooseRangeはオラクルにアクセスできず、doGuessingは手続きguessのみを呼び出せることを意味する。この記法をつかうと、最初の試みは次のように書けただろう。

module type ADV_origin(O:OR) = {
  proc chooseRange() : int * int {O.init O.guess O.guessed}
  proc doGuessing () : unit {O.init O.guess O.guessed}
}.

最後に、chooseRangeがすべての攻撃者のグローバル変数を初期化しなければならないことを、スターアノテーションによって指定できる。

module type ADV(O: OR) = {
  proc * chooseRange() : int * int {}
  proc doGuessing() : unit {O.guess}
}.

このようなチェックの強制はEasyCryptの型検査では実行されないが、ロジック(applyやrewriteなどのタクティクを参照)によってなされる。

推測ゲームの例の全容は次のようになっている。

require import Bool IntDiv DInterval.

module (SimpAdv : ADV) (O: OR) = {
  var range : int * int
  var tries :int
  
  proc chooseRange() : int * int = {
    range <- (1, 100);
    tries <- 10;
    return range;
  }

  proc doGuessing() : unit = {
    var x : int;
    while (0 < tries) {
      x <$ [range.`1 .. range.`2];
      O.guess(x);
      tries <- tries - 1;
    }
  }
}.

module type GAME = {
  proc main(): bool
}.

module Game(Adv: ADV) : GAME = {
  module A = Adv(Or)

  proc main(): bool = {
    var low, high, tries, secret : int;
    var advWon : bool; 
    (low, high) <@ A.chooseRange();
    if (high - low < 10)
      advWon <- false;
    else {
      tries <- (high - low + 1) %/ 10; (* /% は整数の割り算 *)
      secret <$ [low .. high];
      Or.init(secret, tries);
      A.doGuessing();
      advWon <@ Or.guessed();
    }
    return advWon;
  }
}.

module SimpGame : GAME = Game(SimpAdv).

SimpAdvは攻撃者の簡単な実装である。SimpAdvの宣言に含まれる制約SimpAdv : ADVは、EasyCryptにSimpAdvがモジュール型ADVを実装しているかどうかを確かめさせる。すなわち、chooseRangeの実装はOを使わず、doGuessingはguess以外のOの手続きを使わず、chooseRangeはSimpAdvのグローバル変数を初期化する。
chooseRangeは1から100までから範囲を選び、その範囲と何回推測を行うかをグローバル変数に記録して初期化する(なぜ10が賢明な選択なのかはGameのコードを見て確認せよ)。
doGuessingは10回のランダムな推測を行う。

SimpAdvの定義中のパラメータOはORの手続きの適切なサブセットをもつモジュール型Tと一致するように制限されるが、これによってSimpAdvの手続きがOのどの手続きを呼び出せるかをさらに制限する。一方で、TがOR以外の手続きを提供することはできない。*1
SimpAdvはパラメータ化されたモジュールであるものの、別のパラメータを無視するモジュールからグローバル変数の一つを参照するには、たとえば以下のようにする。

module Y = {
  proc f() : int = {
    return SimpAdv.tries;
  }
}.

一方で、どのオラクルをパラメータとして使うのか指定する必要があるSimpAdvの手続きを呼び出すには、次のようにする。

module Y' = {
  proc f() : unit = {
    SimpAdv(Or).doGuessing();
  }
}.

モジュールGameはAdvという攻撃者に、パラメータとして具体的なguessing oracle Orを与えた結果のモジュールAを与える。Gameのmain関数は、ゲームを実行するためにOrとAを用いる。

• main関数は攻撃者が選んだ推測範囲を取得するためにAのchooseRangeを呼び出す。もしも範囲が10より少ない要素しかもたないのであれば、chooseRangeはfalseを返し、それ以上は何も行わない。攻撃者が与えられた範囲が小さすぎるということである。
• そうでなければ、Or.initを使って範囲からランダムに選ばれた秘密情報と、範囲の1/10の数でguessing oracleを初期化する。
• その後、A.doGuessingを呼び出し、攻撃者に秘密情報を推測を試みさせる。
• 最後に、Or.guessedを呼び出して攻撃者が秘密情報を正しく推測できたかどうかを調べ、その結果のbooleanを、結果として返す。

最後に、宣言

module SimpGame = Game(SimpAdv).

は、Gameを我々の簡単な攻撃者SimpAdvで特殊化してSimpGameを宣言する。この宣言をしたとき、EasyCryptの型検査器はSimpAdvがADVの要件を満たすかどうかを検証する。読者は、何がグローバル変数やOrの手続き(またはSimpAdvのあとに宣言されたゲームの手続き)に直接アクセス、呼び出しできるSimpAdvを作成してしまい、我々が想定している攻撃者の能力に違反することを防ぐのかを疑問に思うかもしれない。答えとしては、EasyCryptの型検査器はそれをする立場にはないのである。そのかわり、次のセクションで、このような制限がEasyCryptの論理を使ってどのようにモデル化されているのかをみることにする。

*1:なんのこっちゃわからなかったので訳も胡乱だが、つまり、ORを包含するようなモジュール型TのモジュールOからは、ORがもつ手続きしか呼び出せない、ということかと思われる。