From d4faeacd1eeb95d0bb303f397e19f957a402dd49 Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Wed, 21 Nov 2012 11:28:40 +0100
Subject: [PATCH] Implemented equality/pattern matching support.

Introduced a new event:

  match(pattern,groundterm)

This event can only be executed if pattern can be matched to groundterm.
Variable substitutions are persistent with respect to later events in
the same role.

Currently implemented as syntactic sugar, essentially unfolded in role R to:

  fresh x;
  send ( R,R, { groundterm }x );
  recv ( R,R, { pattern }x );

This work is not complete yet in the send that the output still contains
the unfolding. Ideally, the graph rendered detects this syntactic sugar
and renders a simplified event. This should be possible on the basis of
the label name prefix.

Conflicts:
	src/compiler.c
	src/parser.y
	src/scanner.l
	src/tac.h
---
 src/compiler.c    | 56 +++++++++++++++++++++++++++++++++++++++++++++++
 src/parser.y      | 10 +++++++++
 src/scanner.l     |  1 +
 src/specialterm.c |  5 +++++
 src/specialterm.h |  2 ++
 src/tac.h         |  3 ++-
 6 files changed, 76 insertions(+), 1 deletion(-)

diff --git a/src/compiler.c b/src/compiler.c
index 36b6b5b..5742e45 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -764,6 +764,59 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
   return cl;
 }
 
+//! Parse a match event, and add role definitions for it
+/**
+ * Implemented as pure syntactic sugar:
+ *
+ *   match(pattern,term)
+ *
+ * is essentially replaced by:
+ *
+ *   fresh XX;
+ *   send( {term}XX );
+ *   recv( {pattern}XX );
+ *
+ */
+void
+matchEvent (Tac tc)
+{
+  Term myrole;
+  Term msg1, msg2;
+  Term tvar;
+  Term mmsg;
+  Term mpat;
+  Symbol nsymb;
+  Term label1;
+  Labelinfo linfo;
+
+  /* Create fresh Nonce variable */
+  nsymb = symbolNextFree(TermSymb(TERM_Hidden));
+  tvar = symbolDeclare(nsymb,false);
+  //tvar->stype = termlistAdd(NULL,TERM_Nonce);
+
+  /* Make the concrete messages */
+  mpat = tacTerm (tc->t1.tac);
+  mmsg = tacTerm (tc->t2.tac);
+  msg1 = makeTermEncrypt(mmsg,tvar);
+  msg2 = makeTermEncrypt(mpat,tvar);
+
+  /* Declare the const */
+  thisRole->declaredconsts = termlistAdd(thisRole->declaredconsts, tvar);
+
+  /* And send & recv combo (implementing the syntactic sugar) */
+  label1 = freshTermPrefix(LABEL_Match);
+  linfo = label_create (label1, thisProtocol);
+  sys->labellist = list_append (sys->labellist, linfo);
+  myrole = thisRole->nameterm;
+
+  /* add send event */
+  thisRole->roledef = roledefAdd (thisRole->roledef, SEND, label1, myrole, myrole, msg1, NULL);
+  markLastRoledef (thisRole->roledef, tc->lineno);
+  /* add recv event */
+  thisRole->roledef = roledefAdd (thisRole->roledef, RECV, label1, myrole, myrole, msg2, NULL);
+  markLastRoledef (thisRole->roledef, tc->lineno);
+}
+
 //! Parse a communication event tc of type event, and add a role definition event for it.
 void
 commEvent (int event, Tac tc)
@@ -1185,6 +1238,9 @@ roleCompile (Term nameterm, Tac tc)
 	    firstEvent = 0;
 	    commEvent (SEND, tc);
 	    break;
+	  case TAC_MATCH:
+	    matchEvent (tc);
+	    break;
 	  case TAC_CLAIM:
 	    commEvent (CLAIM, tc);
 	    break;
diff --git a/src/parser.y b/src/parser.y
index 78868e2..b1df431 100644
--- a/src/parser.y
+++ b/src/parser.y
@@ -57,6 +57,7 @@ int yylex(void);
 %token 		HASHFUNCTION
 %token		KNOWS
 %token		TRUSTED
+%token 		MATCH
 
 %type	<tac>	spdlcomplete
 %type	<tac>	spdlrep
@@ -196,6 +197,15 @@ event		: READT label '(' termlist ')' ';'
 			t->t2.tac = $4;
 			$$ = t;
 		  }
+		| MATCH '(' term ',' term ')' ';'
+		  {
+		  	/* first argument is pattern, second should be
+			 * ground term */
+		  	Tac t= tacCreate(TAC_MATCH);
+			t->t1.tac = $3;
+			t->t2.tac = $5;
+			$$ = t;
+		  }
 		| CLAIMT optlabel '(' termlist ')' ';'
 		/* TODO maybe claims should be in the syntax */
 		  {	Tac t = tacCreate(TAC_CLAIM);
diff --git a/src/scanner.l b/src/scanner.l
index fa23f4c..cd7092f 100644
--- a/src/scanner.l
+++ b/src/scanner.l
@@ -160,6 +160,7 @@ role		{ return ROLE; }
 read		{ return READT; }
 recv		{ return RECVT; }
 send		{ return SENDT; }
+match		{ return MATCH; }
 var		{ return VAR; }
 const		{ return CONST; }
 fresh		{ return FRESH; }
diff --git a/src/specialterm.c b/src/specialterm.c
index 6459bd7..6244c8f 100644
--- a/src/specialterm.c
+++ b/src/specialterm.c
@@ -71,6 +71,8 @@ Term TERM_PK;
 Term TERM_SK;
 Term TERM_K;
 
+Term LABEL_Match;
+
 Termlist CLAIMS_dep_prec;
 
 //! Init special terms
@@ -118,6 +120,9 @@ specialTermInit (const System sys)
   knowledgeAddInverse (sys->know, TERM_PK, TERM_SK);
   knowledgeAddTerm (sys->know, TERM_PK);
 
+  /* Define a prefix for labels for the match function */
+  langcons (LABEL_Match, "!Match", TERM_Hidden);
+
   /* Construct a list of claims that depend on prec being not-empty */
   /* basically all authentication claims */
   CLAIMS_dep_prec = termlistAdd (NULL, CLAIM_Niagree);
diff --git a/src/specialterm.h b/src/specialterm.h
index 3a9f510..f5d5497 100644
--- a/src/specialterm.h
+++ b/src/specialterm.h
@@ -63,6 +63,8 @@ extern Term TERM_PK;
 extern Term TERM_SK;
 extern Term TERM_K;
 
+extern Term LABEL_Match;
+
 extern Termlist CLAIMS_dep_prec;
 
 void specialTermInit (const System sys);
diff --git a/src/tac.h b/src/tac.h
index f816b78..0ff1599 100644
--- a/src/tac.h
+++ b/src/tac.h
@@ -50,7 +50,8 @@ enum tactypes
   TAC_HASHFUNCTION,
   TAC_UNTRUSTED,
   TAC_COMPROMISED,
-  TAC_USERTYPE
+  TAC_USERTYPE,
+  TAC_MATCH
 };
 
 //! Structure to hold the compilation tree nodes