Library Sec1_SyntaxDefs
Contents :
0: General House Keeping
1: Syntax definitions
2: Equality, membership and extraction functions for the syntax
2A: Equality functions
2B: Membership functions
2C: Extraction of submembers functions
3: Substitution
4: Ground terms and rules instances
5: Tamarin Reduction
6: Example
7: Definitions from Chapter 5 of the thesis
8: Tests and Definitions for Well formedness
8A: Functions to test no or One Input / Output in facts
8B: Definitions on Variables and Terms for Equivalence proof
8C: Well formedness definitions
9: Some useful lemmas on well formedness
10: Definitions from Chapter 6 of the thesis
10A: Types of Facts allowed in the system
11: Props and Theorems from Chapter 6
Load Sec0_UtilityFunctions.
============================
1: Syntax definitions
===========================
Definition freshNameSetup : Type := string. Definition freshNameProto : Type := string.
Definition sidTerm : Type := string.
Definition publicName : Type := string.
Inductive name : Type :=
| Fresh_S : freshNameSetup -> name
| Fresh_P : freshNameProto -> name
| Pub : publicName -> name.
Definition n : string := "n".
Definition x : string := "x".
Definition names : Type := list name.
Definition variable : Type := string.
Definition variables : Type := list variable.
Inductive baseTerm : Type :=
| Var : variable -> baseTerm
| Name : name -> baseTerm.
Definition baseTerms : Type := list baseTerm.
Definition func_name : Type := string.
Inductive term : Type :=
| Func : func_name -> list baseTerm -> term
| Bterm : baseTerm -> term.
Definition terms : Type := list term.
Inductive tpair: Type :=
| pair : term -> term -> tpair
| emptypair : tpair.
Definition tpairs : Type := list tpair.
Action Label with facts (values)
Inductive actionLabel : Type :=
| ActLabel : name -> terms -> actionLabel.
I'm not sure if this should be name, of some over kind
Label with facts : List of Action Label with facts (values)
Inductive label : Type :=
| BasicLabel : list actionLabel -> label
| LoggedLabel : actionLabel -> list actionLabel -> label
| LoggedSIDLabel : baseTerm -> actionLabel -> list actionLabel -> label.
Definition emptyLabel := (BasicLabel []).
Inductive fact : Type :=
| IN : terms -> fact
An input
| OUT : terms -> fact
An output
| K : terms -> fact
Attacker knowledge
| STATE : name -> terms -> fact
General protocol state informtaion. I'm not sure if this should be name, or some over kind kind of identifier
| FR_P : baseTerm -> fact.
A new fresh name in protocol stage
Definition facts : Type := list fact.
A rule is a triple : pattern followed by Label followed by patterns
Definition trace : Type := list label.
Inductive rule : Type :=
| RuleSetup : facts -> label -> facts -> rule
| RuleProto : facts -> label -> facts -> rule.
A ruleList : List of rule
Definition ruleList : Type := list rule.
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
Global Index
S
Sec1_SyntaxDefs [library]Library Index
S
Sec1_SyntaxDefs| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
This page has been generated by coqdoc