本研究では、ネットワークプロトコルのセキュリティ検 証の枠組を、並行計算の代数的形式体系であるMilnerの ＣＣＳにより示す。ＣＣＳによってシステム全体の振る 舞いをモデル化することにより、抽象的なレベルでの動 作を記述することができる。このような記述を導入する ことでシステムの本質的な動作確認を機械的に行なうこ とが可能になる。ネットワークプロトコルをＣＣＳで記 述することによって、ネットワークにおける情報交換の 安全性についてプロトコルの観点から論じる。本研究で はプライベートな情報を扱う電子メールに着目し、その セキュリティ検証の枠組を提案する。そのうえで、電子 メールシステムの弱点を特定し、実際に講じられている 対策の正当性を示す。