Skip to content

GitLab

V
VerifyTESLA
Commit 3014b25a authored by acholewa's avatar acholewa
Browse files
Options

Added copyright notices to the PSL files.

parent 7fc4bfd6
Hide whitespace changes
Inline Side-by-side
Showing with 182 additions and 237 deletions
PSL-Syntax.maude
View file @ 3014b25a
---(
Maude-PSL, Version: [1.0] [May 15th 2015]
Copyright (c) 2015, University of Illinois
All rights reserved.
Redistribution and use in source and binary forms, with or without modification,
are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation
and/or other materials provided with the distribution.
* Neither the name of the University of Illinois nor the names of its contributors
may be used to endorse or promote products derived from this software without
specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-----------------------------------------------------------------------------------------------------------
Copyright (c) 2015. To the extent that a federal employee is an author of
a portion of the software or a derivative work thereof, no copyright is
claimed by the United States Government, as represented by the Secretary
of the Navy ("GOVERNMENT") under Title 17, U.S. Code. All Other Rights Reserved.
Permission to use, copy, and modify this software and its documentation is
hereby granted, provided that both the copyright notice and this permission
notice appear in all copies of the software, derivative works or modified
versions, and any portions thereof, and that both notices appear in
supporting documentation.
GOVERNMENT ALLOWS FREE USE OF THIS SOFTWARE IN ITS "AS IS" CONDITION AND
DISCLAIM ANY LIABILITY OF ANY KIND FOR ANY DAMAGES WHATSOEVER RESULTING
FROM THE USE OF THIS SOFTWARE.
GOVERNMENT requests users of this software to return modifications,
improvements or extensions that they make to:
maudenpa@chacs.nrl.navy.mil]
-or-
Naval Research Laboratory, Code 5543
4555 Overlook Avenue, SW
Washington, DC 20375
---)
---(
The following modules contain the operators and axioms for the data structures
used in the translation from Maude-PSL to Maud-NPA specifications. Anything
prefixed by a '$' is considered "internal," and shouldn't be used outside
......
psl.maude
View file @ 3014b25a
---(
Maude-PSL, Version: [1.0] [May 15th 2015]
Copyright (c) 2015, University of Illinois
All rights reserved.
Redistribution and use in source and binary forms, with or without modification,
are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation
and/or other materials provided with the distribution.
* Neither the name of the University of Illinois nor the names of its contributors
may be used to endorse or promote products derived from this software without
specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-----------------------------------------------------------------------------------------------------------
Copyright (c) 2015. To the extent that a federal employee is an author of
a portion of the software or a derivative work thereof, no copyright is
claimed by the United States Government, as represented by the Secretary
of the Navy ("GOVERNMENT") under Title 17, U.S. Code. All Other Rights Reserved.
Permission to use, copy, and modify this software and its documentation is
hereby granted, provided that both the copyright notice and this permission
notice appear in all copies of the software, derivative works or modified
versions, and any portions thereof, and that both notices appear in
supporting documentation.
GOVERNMENT ALLOWS FREE USE OF THIS SOFTWARE IN ITS "AS IS" CONDITION AND
DISCLAIM ANY LIABILITY OF ANY KIND FOR ANY DAMAGES WHATSOEVER RESULTING
FROM THE USE OF THIS SOFTWARE.
GOVERNMENT requests users of this software to return modifications,
improvements or extensions that they make to:
maudenpa@chacs.nrl.navy.mil]
-or-
Naval Research Laboratory, Code 5543
4555 Overlook Avenue, SW
Washington, DC 20375
---)
---(
This file contains the second stage of the translation from a Maude-PSL specification to a Maude-NPA specification. To use this code, load it into
Maude and call red T ., where T is an AC soup containing the following:
**********************
......
psl.py
View file @ 3014b25a
"""
Maude-PSL, Version: [1.0] [May 15th 2015]
Copyright (c) 2015, University of Illinois
All rights reserved.
Redistribution and use in source and binary forms, with or without modification,
are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation
and/or other materials provided with the distribution.
* Neither the name of the University of Illinois nor the names of its contributors
may be used to endorse or promote products derived from this software without
specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-----------------------------------------------------------------------------------------------------------
Copyright (c) 2015. To the extent that a federal employee is an author of
a portion of the software or a derivative work thereof, no copyright is
claimed by the United States Government, as represented by the Secretary
of the Navy ("GOVERNMENT") under Title 17, U.S. Code. All Other Rights Reserved.
Permission to use, copy, and modify this software and its documentation is
hereby granted, provided that both the copyright notice and this permission
notice appear in all copies of the software, derivative works or modified
versions, and any portions thereof, and that both notices appear in
supporting documentation.
GOVERNMENT ALLOWS FREE USE OF THIS SOFTWARE IN ITS "AS IS" CONDITION AND
DISCLAIM ANY LIABILITY OF ANY KIND FOR ANY DAMAGES WHATSOEVER RESULTING
FROM THE USE OF THIS SOFTWARE.
GOVERNMENT requests users of this software to return modifications,
improvements or extensions that they make to:
maudenpa@chacs.nrl.navy.mil]
-or-
Naval Research Laboratory, Code 5543
4555 Overlook Avenue, SW
Washington, DC 20375
"""
#!/usr/bin/python
from __future__ import print_function
import itertools
......
pslSemantics.maude deleted 100644 → 0
View file @ 7fc4bfd6
---(
This file contains the basic semantics of the translation from PSL syntax to Maude-NPA
syntax. It does NOT contain any of the additional helper functions, nor does it contain
any of the sorts, memberships, functions, or conditions used in error-checking. It also
does not include anything involving the Definitions.
---)
load NPA-Syntax.maude .
---TODO: Rewrite the error message terms so that they are easier for Python to parse.
mod SPECIFICATION is
protecting DEFINITION-PROTOCOL-RULES .
protecting META-TERM .
------------------------ACU Soup of transitionary data structures----------------------------------
sort TransData .
op mt : -> TransData .
op __ : TransData TransData -> TransData [assoc comm id: mt format(n n o)] .
---------------------------------Strand transitionary data stucture-------------------------------
sort StrDatum StrData .
subsort StrDatum < StrandData .
op mt : -> StrData [ctor] .
op _&_ : StrData StrData -> StrData [assoc comm id: mt format(d d n d)] .
op [_] : StrData -> TransData .
---First argument is the principal. Second argument are the strand input.
---Third argument is the strand. Fourth argument is the strand output.
op _|->{_}_{_} : Msg MsgSet Strand MsgSet -> StrDatum [ctor prec 30] .
------------------------Sections------------------------------------------------------------------
sort Sect Sects SubSect SectName Stmt Stmts .
subsort Sect < TransData .
subsort Stmt < Stmts .
op mt : -> Stmts [ctor] .
op __ : Stmts Stmts -> Stmts [assoc id: mt format(n n o) prec 55] .
ops Protocol Intruder Attacks : -> SectName .
subsorts Sect < Sects .
op __ : SectName Stmts -> SubSect [format(d nt o) prec 60] .
op mt : -> Sects .
op __ : Sects Sects -> Sects [ctor assoc comm id: mt format(d n o) prec 65] .
op [_] : Sects -> TransData [ctor] .
----------------------Protocol Section----------------------------------------
--------------------------Input and Output---------------------------------------
sort ProtStmt ProtStmts .
subsort ProtStmt < Stmt .
subsorts ProtStmt < ProtStmts < Stmts .
op mtProtocol : -> ProtocolSection .
rl [InputOutput] :
[
Protocol
PS1:Stmts
In(P) = IN .
PS2:Stmts
Out(P) = OUT .
PS3:Stmts
SS:SubSections
]
[SD:StrandData]
=>
[
Protocol
PS1:Stmts PS2:Stmts PS3:Stmts
SS:SubSections
]
[P |-> {IN} :: nil :: [(nil).SMsgList-L | nil]
{OUT} & SD:StrandData] .
rl [OutputInput] :
[
Protocol
PS1:Stmts
Out(P) = OUT .
PS2:Stmts
In(P) = IN .
PS3:Stmts
SS:SubSections
]
[SD:StrandData]
=>
[
Protocol
PS1:Stmts PS2:Stmts PS3:Stmts
SS:SubSections
]
[P |-> {IN} :: nil :: [(nil).SMsgList-L | nil] {OUT} &
SD:StrandData] .
---Note: This relies on statement order. Do we want to preserve that? Don't see any reason
---not to. Only an idiot would write a protocol's steps out of order.
rl [StepsToStrands] :
[
Protocol
N . A -> B : TA |- TB .[LN]
S:Stmts
SS:SubSections
]
[A |-> {INA} :: FSA :: [nil | MSA]{OUTA} &
B |-> {INB} :: FSB :: [nil | MSB]{OUTB} &
SD:StrandData]
=>
[
Protocol
S:Stmts
SS:SubSections
]
[A |-> {INA} :: FSA, fresh(TA) :: [ nil | MSA, +(TA)] {OUTA} &
B |-> {INB} :: FSB :: [ nil | MSB, -(TB)] {OUTB} &
SD:StrandData] .
eq [ (Protocol mt) SS:SubSections ] = [ mtProtocol SS:SubSections ] [mtAttackData] .
---------------------------------Intruder-----------------------------------------
op [_] : StrSet -> TransData [ctor] .
op mtMsgSet : -> MsgSet .
op mtIntruder : -> IntrSec .
eq (=> MS:MsgSet .) = (mtMsgSet => MS:MsgSet .) .
eq (MS:MsgSet => M:Msg, M1:Msg, MS1:MsgSet .) =
(MS:MsgSet => M:Msg .) (MS:MsgSet => M1:Msg, MS1:MsgSet .)
rl [IntruderConversion] :
[
Intruder
MS:MsgSet => M:Msg .
S:Stmts
SS:SubSections
]
[SS:StrandSet]
=>
[
Intruder
IS:Stmts
SS:SubSections
]
[:: fresh(M:Msg) :: [ nil | buildList(MS:MsgSet), +(M:Msg)] & SS:StrandSet] .
eq [Intruder mt SS:SubSections] = [mtIntruder SS:SubSections] .
-------------------------------Attacks----------------------------------------------
op without:_ : CoreAttNoIntr -> WithoutBlock [ctor prec 35] .
sort Map Maps .
subsort Map < Maps .
op _|->_ : Msg Msg -> Map [ctor prec 20] .
op _,_ : Maps Maps -> Maps [ctor assoc comm prec 25] .
op ditto : -> Maps [ctor] .
op In`(_`) = _.[_] : Msg Map Nat -> InOutMap [ctor prec 28] .
op Out`(_`) = _.[_] : Msg Map Nat -> InOutMap [ctor prec 28] .
sorts CoreAtt CoreAttNoIntr .
subsort CoreAttNoIntr < CoreAtt .
op ___ : InOutMap ExecStmt InOutMap -> CoreAttNoIntr [ctor prec 30] .
op __ : CoreAttack CoreAttack -> CoreAttack [ctor] .
op ____ : InOutMap ExecStmt IntrStmt InOutMap -> CoreAtt [ctor prec 30] .
sort AttData .
op __ : AttData AttData -> AttData [ctor comm assoc id: mtAttData] .
op mtAttData : -> AttData .
---Syntax for System, from NPA-Syntax.maude
---op _||_||_||_||_ : StrandSet IntruderKnowledge SMsgList GhostList Properties -> System
[format (d n d n d n d n d d)] .
op [_|->_] : Nat System -> AttData .
op [_] : AttData -> TransData .
rl [translateAttacksWithout] :
[
Attacks
N . {CA:CoreAtt WA:WithoutBlocks}
A:AttStmts
SS:SubSections
]
[SP:StrData]
[AT:AttData]
=>
[SP:StrData]
[
Attacks
A:Stmts
SS:SubSects
]
[ AT:AttData
[N:Nat |-> genAttackStrands(CA:CoreAtt, SP:StrData)
|| genIntruderKnowledge(CA:CoreAtt)
|| nil
|| nil
|| never(genNeverPatterns(WA:WithoutBlocks, SP:StrData))]] .
rl [translateAttack] :
[
Attacks
N .{CA:CoreAtt}
A:AttStmts
SS:SubSects
]
[SP:StrData]
[AT:AttData]
=>
[SP:StrData]
[
Attacks
A:AttStmts
SS:SubSects
]
[AT:AttData
[N:Nat |-> genAttackStrands(CA:CoreAtt, SP:StrData)
|| genIntruderKnowledge(CA:CoreAtt)
|| nil
|| nil
|| nil]] .
op genAttackStrands : CoreAttack StrandData -> StrandSet .
eq genAttackStrands(In(P) = INM:Maps .
P executes protocol .
Intruder learns MS:MsgSet .
Out(P) = OUTM:Maps .,
P |-> {IN} S:Strand {OUT} & SD:StrData)
= applyMaps(applyMaps(S:Strand, OUTM:Maps), INM:Maps) .
eq genAttackStrands(In(P) = INM:Maps .
P executes protocol .
Out(P) = OUTM:Maps .,
P |-> {IN} S:Strand {OUT} & SD:StrData)
= applyMaps(applyMaps(S:Strand, OUTM:Maps), INM:Maps) .
---genIntruderKnowledge is a straightforward translation of the Intruder learns ... into the M inI ... syntax
op genNeverPatterns : WithoutBlocks StrandData -> NeverPatternSet .
eq genNeverPatterns(without: CA:CoreAttNoIntr WB:WithoutBlocks, SP:StrData)
= (genAttackStrands(CA:CoreAttNoIntr, SP:StrandData) || empty) genNeverPatterns(WB:WithoutBlocks, SP:StrData) .
eq genNeverPatterns(without: CA:CoreAttNoIntr, SP:StrData) = genAttackStrands(CA:CoreAttNoIntr, SP:StrData) || empty .
endm
pslTree.py
View file @ 3014b25a
"""
Important: To simplify implementation, the parser assumes that the set of user-defined tokens are disjoint from the set of top level tokens.
Maude-PSL, Version: [1.0] [May 15th 2015]
Copyright (c) 2015, University of Illinois
All rights reserved.
Redistribution and use in source and binary forms, with or without modification,
are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation
and/or other materials provided with the distribution.
* Neither the name of the University of Illinois nor the names of its contributors
may be used to endorse or promote products derived from this software without
specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-----------------------------------------------------------------------------------------------------------
Copyright (c) 2015. To the extent that a federal employee is an author of
a portion of the software or a derivative work thereof, no copyright is
claimed by the United States Government, as represented by the Secretary
of the Navy ("GOVERNMENT") under Title 17, U.S. Code. All Other Rights Reserved.
Permission to use, copy, and modify this software and its documentation is
hereby granted, provided that both the copyright notice and this permission
notice appear in all copies of the software, derivative works or modified
versions, and any portions thereof, and that both notices appear in
supporting documentation.
GOVERNMENT ALLOWS FREE USE OF THIS SOFTWARE IN ITS "AS IS" CONDITION AND
DISCLAIM ANY LIABILITY OF ANY KIND FOR ANY DAMAGES WHATSOEVER RESULTING
FROM THE USE OF THIS SOFTWARE.
GOVERNMENT requests users of this software to return modifications,
improvements or extensions that they make to:
maudenpa@chacs.nrl.navy.mil]
-or-
Naval Research Laboratory, Code 5543
4555 Overlook Avenue, SW
Washington, DC 20375
"""
"""
Important: To simplify implementation, the parser assumes that the set of user-defined tokens are disjoint from the set of top level
tokens.
"""
import re
import pslErrors
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment