学生時代は，「時間の概念を含む暗号プロトコルの理論的な安全性検証」というテーマで，研究を行っていました．
暗号プロトコルは，暗号技術を使った，メッセージのやりとり，手順のことです．そして当時，そんな暗号プロトコルによっては，タイムスタンプと呼ばれる時刻情報を，やりとりするメッセージの中に組み込み，それを参照して「このメッセージはまあ問題なさそう」「このタイムスタンプは古いぞ．過去のメッセージを使った，リプレイ攻撃じゃないのか?」なんて判定するのに活用していました*1．
そのような，時間の概念を含む暗号プロトコルに対して，従来の，すなわち時間の概念を十分に考慮していなかった，暗号プロトコルの安全性検証法を拡張して，対象を表現し，安全性を判定する枠組を提案する，という研究です．
ここで「対象」というのは，その手順となる暗号プロトコルそのもののほか，敵対者が盗聴などでどんな情報を知り得るか，そして何を目標とするか，というのが含まれると思ってください．敵対者の目標が達成されるというのは，その暗号プロトコルが安全でないことを意味します*2．
時間の概念を十分に考慮していなかったとき，対称暗号の暗号化と復号の関係，すなわち「ある平文をある鍵で暗号化して暗号文を作り，それを，暗号化と同じ鍵で復号すると，元の平文が得られる」という性質は，次のような，左辺から右辺へ変換するというルール---これを「書換え規則」と呼ぶことにします---で記述できます．
d(x,e(x,y))→y
この書換え規則において，xが鍵，yが平文に対応する変数で，eは暗号化，dは復号を表す関数記号です．
この左辺と右辺を，木で表すことができます．解析木，または構文木ですね．
さてここに，時間の概念をどう取り入れるかを，手短に説明します．まず時間を自然数として表現します．「時間」と「時刻」を区別しておきますと，時間は自然数全体からなる集合で，時刻はその要素，すなわち一つ一つの自然数に対応づけられます．
次に，式や木としてどう表せるかを考えます．
自然数は0から始まるものとして，これには，「0」という記号を割り当てます．
ですが，自然数の1になる時刻は，「1」としません．「tick(0)」とします．tickというのは，1単位時間が経過したことを表す，1変数関数です．時刻0から，1回tickすることで，tick(0)すなわち時刻1になったと思ってください．
自然数の2になる時刻はというと…「tick(tick(0))」です．時刻tick(0)に対して，1回tickをするので，tick(tick(0))です．
あとは分かると思いますが，0に，何回tickを施したか，その回数が，時刻となるわけです．
いくつか補足しますと，このような時刻0を用意し，それより前の時間というのを考えないとき，時刻0のことをエポック(epoch)と呼んだり，そのシステムではエポックを仮定すると言ったりします．それと，0に何回tickをかぶせたかというのは，離散数学の授業でペアノの公理を学んだと思いますが，基本的にはあれと同じです．tickは，後者関数と同一視できます．
で…0，tick(0)，tick(tick(0))を，木で表すとどうなるか，イメージできますか? こうです．*3
tickがもっと増えたらどうなるか，分かりますか? 「木」と言っても分岐のない，鎖型で表示されます．
ここで，0，tick(0)，tick(tick(0))はいずれも，式として許されます．こういうのを「項」と呼びます．逆に，tickだけとか，tickとtickを連結しただけというのは，項ではありません．
時間・時刻の表現に，ひと工夫を加えます．「いつ，そのアクションをするか」というのを表現できるようにしておきたいので，変数を一つ入れて良いこととします．この変数は，今言った「いつ」，きちんと言うと，基準となる時刻に相当します．
変数xは時刻xも表すわけです．時刻x+1は…xに1回tickを適用すれば，その時刻になりますので，tick(x)と書けます．時刻x+2は，もちろん，tick(tick(x))です．
図にすると，こうです．
こうして，変数で表すことにする特定の時刻から，定数時間が経過することが，表現できます．しかしその時刻より前の時間を表現することは，考えません．それと，基準時の変数とは別に，経過時間の変数を用意して，足したり引いたりすることも，考えることなく，暗号プロトコルを表現していくことにします．
先ほど，dとeの組み合わせで書いた書換え規則ですが，そこに現れる項は，情報に対応づけられます．具体的にはxとy，それとe(x,y)です．左辺全体，すなわちd(x,e(x,y))も，項ですが，あとで説明する事情により，議論の対象から外しておきます．
そういった情報それぞれに，時刻をくっつけて，「時刻付き情報」という種類の項をつくることにします．一般形は，x@tです．図だと，こうです．
@を，情報と時刻を結び付けるための2引数関数で，中間記法をとったものだと思ってください．一般には「@(x,t)」のように書くべきところを，読みやすさのため「x@t」と表記する，ということです．
変数ばかりではイメージがわきにくいと思うので，少し具体的な項を書いてみると，k@0や，e(k,m)@50です．ここで50と書きましたが，「0にtickを50回適用して得られる項」の省略形です．このe(k,m)@50は，木でどのようになるかというと…こうです．*4
このように「時刻」と「時刻付き情報」を準備してやっと，時間の概念を考慮した書換え規則が説明できます．対称暗号の暗号化と復号の関係は，次の書換え規則で記述できます．
D(x@t, e(x,y)@t)→y@(t+α)
木にすると，こうです．
ここでxが鍵，yが平文，tが基準となる時刻で，いずれも変数です．eは先ほどと同じ暗号化関数ですが，Dは復号の操作を表す関数です．eとDの違いは，eは，時刻なしの2つの情報を引数にとるのに対し，Dは2つの時刻付き情報を引数にとるところにあります．
αは変数ではなく，この規則，すなわち復号の操作に依存して定める定数です．そしてt+αは，tに時刻の経過を表す1引数関数をα回施してできる項の簡略表現と言えます．これにより，操作をして新たな情報を得ようとすると，αという時間的コストがかかるというのを記述できます．
もう一つ重要なのは，左辺に2度出現する「@t」です．これは，複数の情報に対して操作をするとき，その情報は同じ時刻に存在することを要請しています．
となると，k@0とe(k,m)@50の2つから，D(k@0,e(k,m)@50)としても，今書いた規則が適用できず，復号ができません．そこで，情報の保持に関する書換え規則
Hold(x@t)→x@(t+1)
を追加します．これは，「敵対者が，ある時刻tに情報xを所有していたら，その次の時刻t+1にもその情報xを所有している」という意味です．このHoldを繰り返し適用すれば，ある時刻tに情報xを所有したら，その時刻以降ずっと，情報xを所有するということになります．
式にすると，
Hold(Hold(…k@0…))⇒…⇒k@50
です．それによって，
D(k@50,e(k,m)@50)⇒m@(50+α)
とすることができます．なお，「→」は規則に関する両辺の関係，「⇒」は規則を適用して得られる，項の関係を表す記号です．
このようにして，情報と時刻を結びつけて書換え規則で表せること，またその中には操作による時間的コストを適切に記述できることを見てきました．時間の都合で一言だけに済ませますが，タイムスタンプを参照して，メッセージが新しいとか古いとか判定するため，「条件付き書換え規則」というのを取り入れました．それから，@の第2引数に自然数が現れれば「時刻」ですが，そうでないところに自然数が出現することがあり，それは「タイムスタンプ」です．このタイムスタンプも，1個の変数を含んでよく，通常それはタイムスタンプ情報に対応づけられます．
もちろん「書けるようになったこと」だけが成果ではありません．時間の概念の取扱いが十分でなかった他のアプローチに対して，優位性を示すことができました．
様相論理と呼ばれる論理に基づく枠組だったのですが，そこで安全であると結論づけられていた暗号プロトコルに対して，私が言った方式で対象を記述し，安全性を検証してみたところ，攻撃方法が存在する，すなわちそれが安全でないと示せたのです．
先生にも見てもらって「なるほど，確かに」とおっしゃってもらい，論文にまとめようという意欲がわきました．まあその後，論文として掲載されるまでには，紆余曲折に四苦八苦があったわけですが．
オリジナル
- 俺数教協 3. 論文解説
- 6月10日の講義（情報セキュリティ）で，余談その1として話しました．
*1:タイムスタンプのほか，通し番号や，nonceと呼ばれるセッション内でのみ有効な情報を用いて，リプレイ攻撃を防止する試みは，研究をしていたときにも認識していましたし，授業でも，参考書『秘密の国のアリス』に書かれていることもあって，説明しています．
*2:例えばもし，「敵対者は，鍵を持っていなくても暗号文を瞬時に解読できる」といった能力があると仮定すると，いわば何でもありなので，暗号プロトコルは安全でないとなります．なので，「安全である」にせよ「安全でない」にせよ，敵対者や実行環境に何らかの前提を置いた上での判定となります．
*3:同月24日に，こことこの次の図を差し替えました．
*4:同月25日に，「t」を「0」に変更しました．
