From 4ac74f321fb4186c7dd31a5f57f39d2ac1e57ccc Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Wed, 10 Nov 2010 11:15:00 +0100
Subject: [PATCH] SPDL: Introduced preconstructed PKI with pk/sk/k.

Introduced K(A1...AN) constant function for symmetric pre-shared keys.
Added inverses (pk,sk) as default constructs.
---
 src/main.c        |  6 +++---
 src/specialterm.c | 10 ++++++++++
 src/specialterm.h |  3 +++
 3 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/src/main.c b/src/main.c
index 59ca415..a6839ca 100644
--- a/src/main.c
+++ b/src/main.c
@@ -121,11 +121,11 @@ main (int argc, char **argv)
   /* start system */
   sys = systemInit ();
 
-  /* init compiler for this system */
-  compilerInit (sys);
-
+  /* init knowledge. Needs to go before compiler init for special term init */
   sys->know = emptyKnowledge ();
 
+  /* init compiler for this system */
+  compilerInit (sys);
 
   /* parse input */
 
diff --git a/src/specialterm.c b/src/specialterm.c
index 6b57c48..54130f4 100644
--- a/src/specialterm.c
+++ b/src/specialterm.c
@@ -54,6 +54,9 @@ Term AGENT_Bob;
 Term AGENT_Charlie;
 Term AGENT_Dave;
 Term AGENT_Eve;
+Term TERM_PK;
+Term TERM_SK;
+Term TERM_K;
 
 Termlist CLAIMS_dep_prec;
 
@@ -82,6 +85,13 @@ specialTermInit (const System sys)
   langcons (CLAIM_Empty, "Empty", TERM_Claim);
   langcons (CLAIM_Reachable, "Reachable", TERM_Claim);
 
+  /* Define default PKI using PK/SK/K */
+  langcons (TERM_PK, "pk", TERM_Function);
+  langcons (TERM_SK, "sk", TERM_Function);
+  langcons (TERM_K, "k", TERM_Function);
+  knowledgeAddInverse (sys->know, TERM_PK, TERM_SK);
+  knowledgeAddTerm (sys->know, TERM_PK);
+
   /* 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 b1fe7ac..aa23f08 100644
--- a/src/specialterm.h
+++ b/src/specialterm.h
@@ -48,6 +48,9 @@ extern Term AGENT_Bob;
 extern Term AGENT_Charlie;
 extern Term AGENT_Dave;
 extern Term AGENT_Eve;
+extern Term TERM_PK;
+extern Term TERM_SK;
+extern Term TERM_K;
 
 extern Termlist CLAIMS_dep_prec;