andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

SPDL: Introduced preconstructed PKI with pk/sk/k.

Browse Source 
Introduced K(A1...AN) constant function for symmetric pre-shared keys.
Added inverses (pk,sk) as default constructs.
This commit is contained in:
Cas Cremers 2010-11-10 11:15:00 +01:00
parent 03a8a1b6e7
commit 4ac74f321f
3 changed files with 16 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/main.c
View File

@ -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 */

10
src/specialterm.c
View File

@ -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);

3
src/specialterm.h
View File

@ -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;