From 40d5991ad09541c6487cf23b746c9f9218d79297 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Mon, 5 Dec 2005 14:58:35 +0000
Subject: [PATCH] - Added some notes. - Added extraction of asymmetric keys.

---
 scripts/if2spdl/If.py        | 16 ++++++++--
 scripts/if2spdl/Spdl.py      | 37 +++++++++++++++++-----
 scripts/if2spdl/generator.py | 60 ------------------------------------
 scripts/if2spdl/notes.txt    |  7 +++++
 4 files changed, 50 insertions(+), 70 deletions(-)
 delete mode 100644 scripts/if2spdl/generator.py

diff --git a/scripts/if2spdl/If.py b/scripts/if2spdl/If.py
index 975a5d4..f65db28 100644
--- a/scripts/if2spdl/If.py
+++ b/scripts/if2spdl/If.py
@@ -22,6 +22,9 @@ class Message(object):
 			return msgto
 		else:
 			return self
+	
+	def aKeys(self):
+		return []
 
 class Constant(Message):
 	def __init__ (self,type,s,optprime=""):
@@ -74,7 +77,10 @@ class Composed(Message):
 			new.right = self.right.substitute(msgfrom, msgto)
 			return new
 
-class PublicCrypt(Message):
+	def aKeys(self):
+		return self.left.aKeys() + self.right.aKeys()
+
+class SPCrypt(Message):
 	def __init__ (self,key,message):
 		self.key = key
 		self.message = message
@@ -97,8 +103,14 @@ class PublicCrypt(Message):
 			new.message = self.message.substitute(msgfrom, msgto)
 			return new
 
+	def aKeys(self):
+		return self.message.aKeys() + self.key.aKeys()
 
-class SymmetricCrypt(PublicCrypt):
+class PublicCrypt(SPCrypt):
+	def aKeys(self):
+		return self.message.aKeys() + [self.key]
+
+class SymmetricCrypt(SPCrypt):
 	pass
 
 class XOR(Composed):
diff --git a/scripts/if2spdl/Spdl.py b/scripts/if2spdl/Spdl.py
index 409c080..9623913 100644
--- a/scripts/if2spdl/Spdl.py
+++ b/scripts/if2spdl/Spdl.py
@@ -67,6 +67,7 @@ class Role(object):
 		self.knowledge = If.MsgList([])
 		self.constants = If.MsgList([])
 		self.variables = If.MsgList([])
+		self.asymmetric = If.MsgList([])	# Asymmetric keys 
 	
 	def prependRule(self,rule):
 		self.rules = [rule] + self.rules
@@ -95,6 +96,16 @@ class Role(object):
 
 	def appendEvent(self, event):
 		self.event += [event]
+	
+	def substitute(self, msgfrom, msgto):
+		def subst(o):
+			o = o.substitute(msgfrom, msgto)
+
+		subst(self.events)
+		subst(self.knowledge)
+		subst(self.constants)
+		subst(self.variables)
+		subst(self.asymmetric)
 
 	def inTerms(self):
 		l = []
@@ -113,16 +124,10 @@ class Role(object):
 		res += "\trole " + self.name + "\n"
 		res += "\t{\n"
 
-		
+		res += pfc + "Rule list based messages\n\n"
+		res += pfc + "Asymmetric keys: " + str(self.asymmetric) + "\n"
 
-
-		# TODO declare constants, variables
-		res += pfc + "Constants and variables\n"
-		res += pf + "const " + self.constants.spdl() + ";\n"
-		res += pf + "var   " + self.variables.spdl() + ";\n"
-		res += "\n"
 		# Message sequence (based on rules)
-		res += pfc + "Rule list based messages\n"
 		res += pfc + "Knowledge before: " + str(self.rules[0].before.knowledge) + "\n"
 		for rule in self.rules:
 			# Read
@@ -136,6 +141,14 @@ class Role(object):
 				res += pfc + action("send",rule.sendFact) + ";\n"
 		res += "\n"
 
+		# TODO declare constants, variables
+		res += pfc + "Constants and variables\n"
+		if len(self.constants) > 0:
+			res += pf + "const " + self.constants.spdl() + ";\n"
+		if len(self.variables) > 0:
+			res += pf + "var   " + self.variables.spdl() + ";\n"
+		res += "\n"
+
 		# Message sequence (based on event list)
 		res += pfc + "Event list based messages\n"
 		for event in self.events:
@@ -230,12 +243,20 @@ def sanitizeRole(protocol, role):
 				noncecounter = noncecounter + 1
 				replacelist.append( (t,msg) )
 				role.constants.append(msg)
+				### TEST
+				print "Substituting %s by %s" % (str(t), str(msg))
 	# Apply replacelist
 	if len(replacelist) > 0:
 		for ev in role.events:
 			for (f,t) in replacelist:
 				ev.substitute(f,t)
 
+	# Extract keys
+	akeys = []
+	for ev in role.events:
+		akeys += ev.message.aKeys()
+	role.asymmetric = uniq(akeys)
+
 
 		
 
diff --git a/scripts/if2spdl/generator.py b/scripts/if2spdl/generator.py
deleted file mode 100644
index 47c9a60..0000000
--- a/scripts/if2spdl/generator.py
+++ /dev/null
@@ -1,60 +0,0 @@
-#!/usr/bin/python
-
-import pprint
-
-def unfold(arg):
-	for x in arg:
-		pprint.pprint(x)
-
-def intruderKnowledge(x):
-	print "Intruder knowledge"
-	print x[0], str(x[1])
-
-def scenario(x):
-	print "Scenario",x,"ignoring for now"
-
-def initialState(arg):
-	arg = arg[0]	# One level deeper (has no implication rule)
-	print "Initial State"
-	print len(arg)
-	for x in arg:
-		if x[0] == "h":
-			print "Some stupid semi time thing"
-		if x[0] == "i":
-			intruderKnowledge(x),"ignoring for now"
-		elif x[0] == "w":
-			scenario(x)
-
-# Ignore for now
-def protocolRules(arg):
-	return
-	
-# Goals: ignored for now
-def goal(arg):
-	return
-
-def labeledRule(lr):
-	type = None
-	label = None
-	if lr[0] == "lb":
-		label = lr[1]
-	if lr[2] == "type":
-		type = lr[3]
-	arg = lr[4]
-
-	if type == "Init":
-		initialState(arg)
-	elif type == "Protocol_Rules":
-		protocolRules(arg)
-	elif type == "Goal":
-		goal(arg)
-
-def generateSpdl(ll):
-	if ll[0] == "option":
-		print "Option [" + ll[1] + "]"
-		for i in ll[2]:
-			labeledRule(i)
-		return
-
-	print "Not understood element: "
-	print ll[0]
diff --git a/scripts/if2spdl/notes.txt b/scripts/if2spdl/notes.txt
index 80bd335..c03528b 100644
--- a/scripts/if2spdl/notes.txt
+++ b/scripts/if2spdl/notes.txt
@@ -9,4 +9,11 @@ Regarding the AVISPA IF report:
   STSecrecy
   matching_request
  
+Regarding translation:
+- Read/Send tuples with knowledge updates are horrible.
+  Assuming a 1-1 mapping from after knowledge of step n with before
+  knowledge of step n+1.
+- Public key status in role defs is that of a variable, possible fixes
+  by substitutions from the scenario. That is plain ugly: scenario is
+  needed to explain meaning of role definition.