modifs erreurs missing avec commentaires

tamarin-prover · Jun 24, 2024 · 0c146ad · 0c146ad
1 parent bf2d0f2
commit 0c146ad
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 120 deletions.
diff --git a/src/grammar/tamarinParser.js b/src/grammar/tamarinParser.js
@@ -10,16 +10,15 @@ parser.setLanguage(Tamarin);
 var sourceCodePath = './tree-sitter-tamarin/example_file.spthy';
 var sourceCode = fs.readFileSync(path.resolve(__dirname, sourceCodePath), 'utf8');
 var tree = parser.parse(sourceCode);
-console.log(tree.rootNode.toString());
-/*function display_tree(node : Parser.SyntaxNode | null){
-    if (node !== null){
-    console.log(node.toString());
-    for (let i = 0 ; i< node.childCount; i++){
-        if(node.child(i) !== null){
-            display_tree(node.child(i));
+function display_tree(node) {
+    var _a;
+    if (node !== null) {
+        console.log((_a = node.parent) === null || _a === void 0 ? void 0 : _a.children);
+        for (var i = 0; i < node.childCount; i++) {
+            if (node.child(i) !== null) {
+                display_tree(node.child(i));
+            }
         }
     }
 }
-}
-
-display_tree(tree.rootNode)*/ 
+display_tree(tree.rootNode);
diff --git a/src/grammar/tamarinParser.ts b/src/grammar/tamarinParser.ts
@@ -16,17 +16,17 @@ const sourceCode = fs.readFileSync(path.resolve(__dirname, sourceCodePath), 'utf
 
 const tree = parser.parse(sourceCode);
 
-console.log(tree.rootNode.toString());
 
-/*function display_tree(node : Parser.SyntaxNode | null){
+function display_tree(node : Parser.SyntaxNode | null){
     if (node !== null){
-    console.log(node.toString());
+    console.log(node.parent?.children);
     for (let i = 0 ; i< node.childCount; i++){
         if(node.child(i) !== null){
             display_tree(node.child(i));
         }
     }
+
 }
 }
 
-display_tree(tree.rootNode)*/
+display_tree(tree.rootNode)
diff --git a/src/grammar/tree-sitter-tamarin/example_file.spthy b/src/grammar/tree-sitter-tamarin/example_file.spthy
@@ -10,119 +10,15 @@ Date: 	        June 2024
 theory WideMouthedFrog
 begin
 
-builtins  hashing, symmetric-encryption
+
 
 
 
 
 
 rule Generate_Secret_key_AS:
     [Fr(~k)]
-  --> 
-    [!Secretk($A, $S, ~k)]  // Generate a private key for both Alice and Server
-
-
-    rule Generate_Secret_key_BS:
-    [Fr(~k)] 
   -->
-    [!Secretk($B, $S, ~k)]  // Generate a private key for both Bob and Server
-
-
-
-
-rule Reveal_secretk:
-    [ !Secretk(A, B, ltk) ]
-  --[ Secretk_reveal(A, B) ]->
-    [ Out(ltk) ]
-
-
-rule Alice_1:
-    [
-        !Secretk($A, $S, kas)
-        ,Fr(~kab)
-        ,Fr(~Ta)
-    ]
-  --[Alice_sends($A, $S, ~kab)]->
-    [
-      Out(<$A,senc(<' 1', ~Ta, $B, ~kab>,kas)>)  
-    ]
-
-rule Server_1:
-    [
-        !Secretk($B, $S, kbs)
-        ,!Secretk($A, $S, kas)
-        ,In(<$A,senc(<' 1', Ta, $B, kab>,kas)>)
-        ,Fr(~Ts)
-    ]
-  --[Server_send($A, $S, $B, kab)]->
-    [
-       Out(senc(<' 2', ~Ts, $A, kab>,kbs)) 
-    ]
-
-rule Bob_1:
-    [
-        !Secretk($B, $S, kbs)
-        ,In(senc(<' 2', Ts, $A, kab>,kbs))
-    ]
-  --[Bob_receive($S, $B, kab)]->
-    [
-
-    ]
-
-
-lemma key_secrecy_1:
-    " not(Ex A S kab #i #j.
-        Alice_sends(A, S, kab) @i
-
-        &K(kab) @j
-
-        & not( (Ex #r. Secretk_reveal(A, S) @r)
-        | (Ex B #r. Secretk_reveal(B, S) @r))
-        )
-    "
-
-lemma key_secrecy_2:
-    "not(Ex A B S kab #i #j.
-        Server_send(A, S, B, kab) @i
-
-        &K(kab) @j
-
-        & not ((Ex #r. Secretk_reveal(B, S) @r)
-        | (Ex #r. Secretk_reveal(A,S) @r))  
-
-    )
-    "
-
-lemma authentication_kab_1:
-    "
-    All A B S kab #i.(
-        Server_send(A, S, B, kab) @i
-        ==>
-        ((Ex #j. Alice_sends(A, S, kab) @j)
-        |(Ex #j. Secretk_reveal(A,S) @j & j < i))
-    )
-    "
-
-lemma authentication_kab_2:
-    "
-    All  B S kab #i.(
-        Bob_receive(S, B, kab) @i
-        ==>
-        ((Ex A #j. Server_send(A, S, B, kab) @j)
-        |(Ex #j. Secretk_reveal(B,S) @j & j < i))
-    )
-    "
-
-
-
-lemma message_honest_setup:
-    exists-trace
-    "Ex A B S kab #i #j #k.
-        Alice_sends(A, S, kab) @i
-        & Server_send(A, S, B, kab) @j & i < j 
-        & Bob_receive(S, B, kab) @k & j < k 
-        & not(Ex #r. Secretk_reveal(A, S) @ r)
-        & not(Ex #r. Secretk_reveal(B, S) @ r )
+    [!Secretk($A, $S, ~k) // Generate a private key for both Alice and Server
 
-    "
 end