Library Sec6_TamarinExample

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 Sec5_TamarinReduction.

=====================

6: Example

=====================

Definition varX : term := Bterm (Var "x") .
Definition varY : term := Bterm (Var "Y") .
Definition AttackerReceive (ts:terms) : rule := RuleProto [ OUT ts ] emptyLabel [ K ts ].
Definition AttackerReceive1 : rule := RuleProto [ OUT [varX] ] emptyLabel [ K [varX] ].
Definition AttackerReceive2 : rule := RuleProto [ OUT [varX;varY] ] emptyLabel [ K [varX]; K [varY] ].
Definition AttackerSend (ts:terms) : rule := RuleProto [ K ts ] emptyLabel [ IN ts ].
Definition AttackerSend1 : rule := RuleProto [ K [varX] ] emptyLabel [ K [varX] ].
Definition AttackerSend2 : rule := RuleProto [ K [varX]; K [varY] ] emptyLabel [ IN [varX; varY] ].
Definition LtkFact : name := Pub "LtkFact".
Definition ltkA_var : baseTerm := (Var "ltkA").
Definition ltkB_var : baseTerm := (Var "ltkB").
Definition PkFact : name := Pub "PkFact".
Definition PkName : string := "Pkname".
Definition Pk : string := "Pkname".
Definition A : term := Bterm (Name (Pub "A")).
Definition B : term := Bterm (Name (Pub "B")).
Definition C : term := Bterm (Name (Pub "C")).



Definition registerPKruleA : rule := RuleSetup [ FR_P ltkA_var ] emptyLabel
                                [STATE LtkFact [A; (Bterm ltkA_var)]; STATE PkFact [A; Func PkName [ltkA_var]];
                                       OUT [Func PkName [ltkA_var]] ].

Definition registerPKruleB : rule := RuleSetup [ FR_P ltkB_var ] emptyLabel
                                [STATE LtkFact [B; (Bterm ltkB_var)]; STATE PkFact [B; Func PkName [ltkB_var]];
                                          OUT [Func PkName [ltkB_var]] ].

Definition St_I_1 : name := Pub "St_I_1".

Definition ni : baseTerm := (Var "ni").


Definition m1 : term := Func "aenc" [ ni; (Name (Pub "A"))].

Definition I_1_A_to_B : rule := RuleProto [(FR_P ni); STATE PkFact [B; Func PkName [ltkB_var]]]
(BasicLabel [ ActLabel (Pub "Out") [m1] ])
                                      [OUT [m1]; STATE St_I_1 [A; B; (Bterm ni)]; STATE PkFact [B; Func PkName [ltkB_var]]].


Definition SetupAndProtocolRules : ruleList := [registerPKruleA; registerPKruleB; I_1_A_to_B].

Lemma protocolRun1Step : run SetupAndProtocolRules [] [] [FR_P (Name (Fresh_P "ltkA")) ].

Lemma protocolRun2Step : run SetupAndProtocolRules [] []
              [FR_P (Name (Fresh_P "ltkB")); FR_P (Name (Fresh_P "ltkA"))].


Definition mapLtkAvarToName := "ltkA" !-> Fresh_P "ltkA"; subs_empty.

Definition registerPKruleAground : rule := RuleSetup [ FR_P (Name (Fresh_P "ltkA")) ]
                                emptyLabel
                                [STATE LtkFact [A; Bterm (Name (Fresh_P "ltkA"))];
                                 STATE PkFact [A; Func PkName [(Name (Fresh_P "ltkA"))]];
                                 OUT [Func PkName [(Name (Fresh_P "ltkA"))]] ].

Lemma protocolRun2to3Step : run SetupAndProtocolRules
              [FR_P (Name (Fresh_P "ltkB")); FR_P (Name (Fresh_P "ltkA"))]
              []
              [STATE LtkFact [A; (Bterm (Name (Fresh_P "ltkA")))];
               STATE PkFact [A; Func PkName [(Name (Fresh_P "ltkA"))]];
               OUT [Func PkName [(Name (Fresh_P "ltkA"))]];
               FR_P (Name (Fresh_P "ltkB"))].

Lemma protocolRunToStop3: run SetupAndProtocolRules [] []
              [STATE LtkFact [A; (Bterm (Name (Fresh_P "ltkA")))];
               STATE PkFact [A; Func PkName [(Name (Fresh_P "ltkA"))]];
               OUT [Func PkName [(Name (Fresh_P "ltkA"))]];
               FR_P (Name (Fresh_P "ltkB"))].

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

Sec6_TamarinExample [library]


Library Index

S

Sec6_TamarinExample


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