From 7bb1a48f8717748c7e49bbf161d91a0160471fff Mon Sep 17 00:00:00 2001
From: Tim Makarios <tjm1983@gmail.com>
Date: Thu, 19 Feb 2015 16:34:58 +1300
Subject: [PATCH] Defined indistinguishable

---
 Communication.thy | 26 +++++++++++++++++++++++++-
 1 file changed, 25 insertions(+), 1 deletion(-)

diff --git a/Communication.thy b/Communication.thy
index 71e8f70..20f4acd 100644
--- a/Communication.thy
+++ b/Communication.thy
@@ -54,8 +54,32 @@ inductive constructible :: "actor \<Rightarrow> message set \<Rightarrow> messag
             \<Longrightarrow> constructible a Ms (MessageList l)"
           -- {* a list of otherwise constructible messages *}
 
-subsubsection {* Indistinguishability of encrypted messages *}
+subsubsection {* Indistinguishability of messages *}
 datatype_new agent = CommunicationLayer | Actor actor
+
+text {* What pairs of messages should we not expect a particular agent to be able
+        to distinguish between, given a particular set of messages to work from?
+        This definition isn't intended to express a limit on what an attacker might
+        be able to do; rather, it's meant to limit what we might reasonably expect
+        an honest agent to be able to do without resorting to sophisticated
+        cryptanalysis or anything similarly difficult. *}
+inductive indistinguishable :: "agent \<Rightarrow> message set \<Rightarrow> message \<Rightarrow> message \<Rightarrow> bool"
+  where "indistinguishable CommunicationLayer _ _ _"
+      | "indistinguishable _ _ m m"
+      | "\<not> constructible a Ms m \<Longrightarrow> \<not> constructible a Ms m'
+          \<Longrightarrow> indistinguishable (Actor a) Ms (Signature _ m) (Signature _ m')"
+      | "indistinguishable A Ms m m'
+          \<Longrightarrow> indistinguishable A Ms (Signature a m) (Signature a m')"
+      | "A \<noteq> Actor a \<Longrightarrow> A \<noteq> Actor b \<Longrightarrow> A \<noteq> Actor c \<Longrightarrow> A \<noteq> Actor d
+          \<Longrightarrow> indistinguishable A _ (Encrypted a b _) (Encrypted c d _)"
+      | "indistinguishable A Ms m m'
+          \<Longrightarrow> indistinguishable A Ms (Encrypted a b m) (Encrypted a b m')"
+      | "indistinghishable A Ms m m'
+          \<Longrightarrow> indistinguishable A Ms (MessageList ms) (MessageList ms')
+          \<Longrightarrow> indistinguishable A Ms
+                (MessageList (m # ms))
+                (MessageList (m' # ms'))"
+
 type_synonym encrypted_message_data = "actor \<times> actor \<times> message"
 type_synonym
   encrypted_message_map = "encrypted_message_data \<Rightarrow> encrypted_message_data"
-- 
2.11.4.GIT