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 spdlcomplete %type 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