...
 
Commits (38)
File added
***(
This file is part of the Maude 2 interpreter.
Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA.
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
)
***
*** Maude Diophantine solver.
*** Version 2.3.
***
fmod VECTOR{X :: DEFAULT} is
protecting (ARRAY * (sort Entry{X,Y} to Entry{Y},
sort Array{X,Y} to Vector{Y})
){Nat, X} .
endfm
fmod INDEX-PAIR is
protecting NAT .
sort IndexPair .
op _,_ : Nat Nat -> IndexPair [ctor] .
endfm
view IndexPair from TRIV to INDEX-PAIR is
sort Elt to IndexPair .
endv
fmod MATRIX{X :: DEFAULT} is
protecting (ARRAY * (sort Entry{X,Y} to Entry{Y},
sort Array{X,Y} to Matrix{Y})
){IndexPair, X} .
endfm
fmod INT-VECTOR is
protecting VECTOR{Int0} * (sort Entry{Int0} to IntVectorEntry,
sort Vector{Int0} to IntVector,
op empty to zeroVector) .
endfm
view IntVector from TRIV to INT-VECTOR is
sort Elt to IntVector .
endv
fmod INT-MATRIX is
protecting MATRIX{Int0} * (sort Entry{Int0} to IntMatrixEntry,
sort Matrix{Int0} to IntMatrix,
op empty to zeroMatrix) .
endfm
fmod DIOPHANTINE is
protecting STRING .
protecting INT-MATRIX .
protecting SET{IntVector} * (sort NeSet{IntVector} to NeIntVectorSet,
sort Set{IntVector} to IntVectorSet,
op _,_ : Set{IntVector} Set{IntVector} -> Set{IntVector} to
(_,_) [prec 121 format (d d ni d)]) .
sort IntVectorSetPair .
op [_|_] : IntVectorSet IntVectorSet -> IntVectorSetPair [format (d n++i n ni n-- d)] .
op natSystemSolve : IntMatrix IntVector String -> IntVectorSetPair
[special (
id-hook MatrixOpSymbol (natSystemSolve)
op-hook succSymbol (s_ : Nat ~> NzNat)
op-hook minusSymbol (-_ : NzNat ~> Int)
op-hook stringSymbol (<Strings> : ~> Char)
op-hook emptyVectorSymbol (zeroVector : ~> IntVector)
op-hook vectorEntrySymbol (_|->_ : Nat Int ~> IntVectorEntry)
op-hook vectorSymbol (_;_ : IntVector IntVector ~> IntVector)
op-hook emptyMatrixSymbol (zeroMatrix : ~> IntMatrix)
op-hook matrixEntrySymbol (_|->_ : IndexPair Int ~> IntMatrixEntry)
op-hook matrixSymbol (_;_ : IntMatrix IntMatrix ~> IntMatrix)
op-hook indexPairSymbol (_,_ : Nat Nat ~> IndexPair)
op-hook emptyVectorSetSymbol (empty : ~> IntVectorSet)
op-hook vectorSetSymbol (_,_ : IntVectorSet IntVectorSet ~> IntVectorSet)
op-hook vectorSetPairSymbol ([_|_] : IntVectorSet IntVectorSet ~> IntVectorSetPair))] .
op natSystemSolve : IntMatrix IntVector -> IntVectorSetPair .
eq natSystemSolve(M:IntMatrix, V:IntVector) = natSystemSolve(M:IntMatrix, V:IntVector, "") .
endfm
***(
This file is part of the Maude 2 interpreter.
Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA.
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
)
***
*** Approximation of Maude 1.0 MachineInts.
*** Version 2.3.
***
*** Note that 0 lives in MachineZero. Also using out of range
*** integer constants may cause incorrect results. MACHINE-INT may
*** be instanciated using a view that maps $nrBits to any power of
*** 2 that is >= 2.
***
fmod RENAMED-INT is
protecting INT * (
sort Zero to MachineZero,
sort NzNat to NzMachineNat,
sort Nat to MachineNat,
sort NzInt to NzMachineInt,
sort Int to MachineInt,
op s_ : Nat -> NzNat to $succ,
op sd : Nat Nat -> Nat to $sd,
op -_ : Int -> Int to $neg,
op _+_ : Int Int -> Int to $add,
op _-_ : Int Int -> Int to $sub,
op _*_ : NzInt NzInt -> NzInt to $mult,
op _quo_ : Int NzInt -> Int to $quo,
op _rem_ : Int NzInt -> Int to $rem,
op _^_ : Int Nat -> Int to $pow,
op abs : NzInt -> NzNat to $abs,
op gcd : NzInt Int -> NzNat to $gcd,
op lcm : NzInt NzInt -> NzNat to $lcm,
op min : NzInt NzInt -> NzInt to $min,
op max : NzInt NzInt -> NzInt to $max,
op _xor_ : Int Int -> Int to $xor,
op _>>_ : Int Nat -> Int to $shr,
op _<<_ : Int Nat -> Int to $shl,
op _divides_ : NzInt Int -> Bool to $divides
) .
endfm
fth BIT-WIDTH is
protecting RENAMED-INT .
op $nrBits : -> NzMachineNat .
var N : NzMachineNat .
eq $divides(2, $nrBits) = true [nonexec] .
ceq $divides(2, N) = true if $divides(N, $nrBits) /\ N > 1 [nonexec] .
endfth
view 32-BIT from BIT-WIDTH to RENAMED-INT is
op $nrBits to term 32 .
endv
view 64-BIT from BIT-WIDTH to RENAMED-INT is
op $nrBits to term 64 .
endv
fmod MACHINE-INT{X :: BIT-WIDTH} is
***
*** Note that operations
*** ~_ _&_ _|_ _<_ _<=_ _>_ _=>_
*** are inherited unmodified.
***
vars I J : MachineInt .
var K : NzMachineInt .
op $mask : -> NzMachineInt [memo] .
eq $mask = $sub($nrBits, 1) .
op $sign : -> NzMachineInt [memo] .
eq $sign = $pow(2, $mask) .
op maxMachineInt : -> NzMachineInt [memo] .
eq maxMachineInt = $sub($sign, 1) .
op minMachineInt : -> NzMachineInt [memo] .
eq minMachineInt = $neg($sign) .
op $wrap : MachineInt -> MachineInt .
eq $wrap(I) = (I & maxMachineInt) | $neg(I & $sign) .
op _+_ : MachineInt MachineInt -> MachineInt [assoc comm prec 33] .
eq I + J = $wrap($add(I, J)) .
op -_ : MachineInt -> MachineInt .
eq - I = $wrap($neg(I)) .
op _-_ : MachineInt MachineInt -> MachineInt [prec 33 gather (E e)] .
eq I - J = $wrap($sub(I, J)) .
op _*_ : MachineInt MachineInt -> MachineInt [assoc comm prec 31] .
eq I * J = $wrap($mult(I, J)) .
op _/_ : MachineInt NzMachineInt -> MachineInt [prec 31 gather (E e)] .
eq I / K = $wrap($quo(I, K)) .
op _%_ : MachineInt NzMachineInt -> MachineInt [prec 31 gather (E e)] .
eq I % K = $rem(I, K) .
op _^_ : MachineInt MachineInt -> MachineInt [prec 55 gather (E e)] .
eq I ^ J = $xor(I, J) .
op _>>_ : MachineInt MachineInt -> MachineInt [prec 35 gather (E e)] .
eq I >> J = $shr(I, ($mask & J)) .
op _<<_ : MachineInt MachineInt -> MachineInt [prec 35 gather (E e)] .
eq I << J = $wrap($shl(I, ($mask & J))) .
endfm
***(
This file is part of the Maude 2 interpreter.
Copyright 2009 SRI International, Menlo Park, CA 94025, USA.
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
)
***
*** Maude meta-interpreters.
*** Version 2.5.
***
mod META-INTERPRETER is
protecting META-LEVEL .
including CONFIGURATION .
op interpreter : Nat -> Oid .
op createInterpreter : Oid Oid -> Msg [ctor msg format (b o)] .
op createdInterpreter : Oid Oid Oid -> Msg [ctor msg format (m o)] .
op insertModule : Oid Oid Module -> Msg [ctor msg format (b o)] .
op insertedModule : Oid Oid -> Msg [ctor msg format (m o)] .
op showModule : Oid Oid Qid Bool -> Msg [ctor msg format (b o)] .
op showingModule : Oid Oid Module -> Msg [ctor msg format (m o)] .
op reduceTerm : Oid Oid Qid Term -> Msg [ctor msg format (b o)] .
op reducedTerm : Oid Oid Nat Term Sort -> Msg [ctor msg format (m o)] .
op rewriteTerm : Oid Oid Bound Qid Term -> Msg [ctor msg format (b o)] .
op rewroteTerm : Oid Oid Nat Term Sort -> Msg [ctor msg format (m o)] .
op frewriteTerm : Oid Oid Bound Nat Qid Term -> Msg [ctor msg format (b o)] .
op frewroteTerm : Oid Oid Nat Term Sort -> Msg [ctor msg format (m o)] .
op quit : Oid Oid -> Msg [ctor msg format (b o)] .
op bye : Oid Oid -> Msg [ctor msg format (m o)] .
op interpreterManager : -> Oid
[special (
id-hook InterpreterManagerSymbol
op-hook succSymbol (s_ : Nat ~> NzNat)
op-hook interpreterOidSymbol (interpreter : Nat ~> Oid)
op-hook createInterpreterMsg (createInterpreter : Oid Oid ~> Msg)
op-hook createdInterpreterMsg (createdInterpreter : Oid Oid Oid ~> Msg)
op-hook insertModuleMsg (insertModule : Oid Oid Module ~> Msg)
op-hook insertedModuleMsg (insertedModule : Oid Oid ~> Msg)
op-hook showModuleMsg (showModule : Oid Oid Qid Bool ~> Msg)
op-hook showingModuleMsg (showingModule : Oid Oid Module ~> Msg)
op-hook reduceTermMsg (reduceTerm : Oid Oid Qid Term ~> Msg)
op-hook reducedTermMsg (reducedTerm : Oid Oid Nat Term Sort ~> Msg)
op-hook rewriteTermMsg (rewriteTerm : Oid Oid Bound Qid Term ~> Msg)
op-hook rewroteTermMsg (rewroteTerm : Oid Oid Nat Term Sort ~> Msg)
op-hook frewriteTermMsg (frewriteTerm : Oid Oid Bound Nat Qid Term ~> Msg)
op-hook frewroteTermMsg (frewroteTerm : Oid Oid Nat Term Sort ~> Msg)
op-hook quitMsg (quit : Oid Oid ~> Msg)
op-hook byeMsg (bye : Oid Oid ~> Msg)
op-hook shareWith (metaReduce : Module Term ~> ResultPair)
)] .
endm
***(
This file is part of the Maude 2 interpreter.
Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA.
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
)
***
*** Maude LTL satisfiability solver and model checker.
*** Version 2.3.
***
fmod LTL is
protecting BOOL .
sort Formula .
*** primitive LTL operators
ops True False : -> Formula [ctor format (g o)] .
op ~_ : Formula -> Formula [ctor prec 53 format (r o d)] .
op _/\_ : Formula Formula -> Formula [comm ctor gather (E e) prec 55 format (d r o d)] .
op _\/_ : Formula Formula -> Formula [comm ctor gather (E e) prec 59 format (d r o d)] .
op O_ : Formula -> Formula [ctor prec 53 format (r o d)] .
op _U_ : Formula Formula -> Formula [ctor prec 63 format (d r o d)] .
op _R_ : Formula Formula -> Formula [ctor prec 63 format (d r o d)] .
*** defined LTL operators
op _->_ : Formula Formula -> Formula [gather (e E) prec 65 format (d r o d)] .
op _<->_ : Formula Formula -> Formula [prec 65 format (d r o d)] .
op <>_ : Formula -> Formula [prec 53 format (r o d)] .
op []_ : Formula -> Formula [prec 53 format (r d o d)] .
op _W_ : Formula Formula -> Formula [prec 63 format (d r o d)] .
op _|->_ : Formula Formula -> Formula [prec 63 format (d r o d)] . *** leads-to
op _=>_ : Formula Formula -> Formula [gather (e E) prec 65 format (d r o d)] .
op _<=>_ : Formula Formula -> Formula [prec 65 format (d r o d)] .
vars f g : Formula .
eq f -> g = ~ f \/ g .
eq f <-> g = (f -> g) /\ (g -> f) .
eq <> f = True U f .
eq [] f = False R f .
eq f W g = (f U g) \/ [] f .
eq f |-> g = [](f -> (<> g)) .
eq f => g = [] (f -> g) .
eq f <=> g = [] (f <-> g) .
*** negative normal form
eq ~ True = False .
eq ~ False = True .
eq ~ ~ f = f .
eq ~ (f \/ g) = ~ f /\ ~ g .
eq ~ (f /\ g) = ~ f \/ ~ g .
eq ~ O f = O ~ f .
eq ~(f U g) = (~ f) R (~ g) .
eq ~(f R g) = (~ f) U (~ g) .
endfm
fmod LTL-SIMPLIFIER is
including LTL .
*** The simplifier is based on:
*** Kousha Etessami and Gerard J. Holzman,
*** "Optimizing Buchi Automata", p153-167, CONCUR 2000, LNCS 1877.
*** We use the Maude sort system to do much of the work.
sorts TrueFormula FalseFormula PureFormula PE-Formula PU-Formula .
subsort TrueFormula FalseFormula < PureFormula <
PE-Formula PU-Formula < Formula .
op True : -> TrueFormula [ctor ditto] .
op False : -> FalseFormula [ctor ditto] .
op _/\_ : PE-Formula PE-Formula -> PE-Formula [ctor ditto] .
op _/\_ : PU-Formula PU-Formula -> PU-Formula [ctor ditto] .
op _/\_ : PureFormula PureFormula -> PureFormula [ctor ditto] .
op _\/_ : PE-Formula PE-Formula -> PE-Formula [ctor ditto] .
op _\/_ : PU-Formula PU-Formula -> PU-Formula [ctor ditto] .
op _\/_ : PureFormula PureFormula -> PureFormula [ctor ditto] .
op O_ : PE-Formula -> PE-Formula [ctor ditto] .
op O_ : PU-Formula -> PU-Formula [ctor ditto] .
op O_ : PureFormula -> PureFormula [ctor ditto] .
op _U_ : PE-Formula PE-Formula -> PE-Formula [ctor ditto] .
op _U_ : PU-Formula PU-Formula -> PU-Formula [ctor ditto] .
op _U_ : PureFormula PureFormula -> PureFormula [ctor ditto] .
op _U_ : TrueFormula Formula -> PE-Formula [ctor ditto] .
op _U_ : TrueFormula PU-Formula -> PureFormula [ctor ditto] .
op _R_ : PE-Formula PE-Formula -> PE-Formula [ctor ditto] .
op _R_ : PU-Formula PU-Formula -> PU-Formula [ctor ditto] .
op _R_ : PureFormula PureFormula -> PureFormula [ctor ditto] .
op _R_ : FalseFormula Formula -> PU-Formula [ctor ditto] .
op _R_ : FalseFormula PE-Formula -> PureFormula [ctor ditto] .
vars p q r s : Formula .
var pe : PE-Formula .
var pu : PU-Formula .
var pr : PureFormula .
*** Rules 1, 2 and 3; each with its dual.
eq (p U r) /\ (q U r) = (p /\ q) U r .
eq (p R r) \/ (q R r) = (p \/ q) R r .
eq (p U q) \/ (p U r) = p U (q \/ r) .
eq (p R q) /\ (p R r) = p R (q /\ r) .
eq True U (p U q) = True U q .
eq False R (p R q) = False R q .
*** Rules 4 and 5 do most of the work.
eq p U pe = pe .
eq p R pu = pu .
*** An extra rule in the same style.
eq O pr = pr .
*** We also use the rules from:
*** Fabio Somenzi and Roderick Bloem,
*** "Efficient Buchi Automata from LTL Formulae",
*** p247-263, CAV 2000, LNCS 1633.
*** that are not subsumed by the previous system.
*** Four pairs of duals.
eq O p /\ O q = O (p /\ q) .
eq O p \/ O q = O (p \/ q) .
eq O p U O q = O (p U q) .
eq O p R O q = O (p R q) .
eq True U O p = O (True U p) .
eq False R O p = O (False R p) .
eq (False R (True U p)) \/ (False R (True U q)) = False R (True U (p \/ q)) .
eq (True U (False R p)) /\ (True U (False R q)) = True U (False R (p /\ q)) .
*** <= relation on formula
op _<=_ : Formula Formula -> Bool [prec 75] .
eq p <= p = true .
eq False <= p = true .
eq p <= True = true .
ceq p <= (q /\ r) = true if (p <= q) /\ (p <= r) .
ceq p <= (q \/ r) = true if p <= q .
ceq (p /\ q) <= r = true if p <= r .
ceq (p \/ q) <= r = true if (p <= r) /\ (q <= r) .
ceq p <= (q U r) = true if p <= r .
ceq (p R q) <= r = true if q <= r .
ceq (p U q) <= r = true if (p <= r) /\ (q <= r) .
ceq p <= (q R r) = true if (p <= q) /\ (p <= r) .
ceq (p U q) <= (r U s) = true if (p <= r) /\ (q <= s) .
ceq (p R q) <= (r R s) = true if (p <= r) /\ (q <= s) .
*** condition rules depending on <= relation
ceq p /\ q = p if p <= q .
ceq p \/ q = q if p <= q .
ceq p /\ q = False if p <= ~ q .
ceq p \/ q = True if ~ p <= q .
ceq p U q = q if p <= q .
ceq p R q = q if q <= p .
ceq p U q = True U q if p =/= True /\ ~ q <= p .
ceq p R q = False R q if p =/= False /\ q <= ~ p .
ceq p U (q U r) = q U r if p <= q .
ceq p R (q R r) = q R r if q <= p .
endfm
fmod SAT-SOLVER is
protecting LTL .
*** formula lists and results
sorts FormulaList SatSolveResult TautCheckResult .
subsort Formula < FormulaList .
subsort Bool < SatSolveResult TautCheckResult .
op nil : -> FormulaList [ctor] .
op _;_ : FormulaList FormulaList -> FormulaList [ctor assoc id: nil] .
op model : FormulaList FormulaList -> SatSolveResult [ctor] .
op satSolve : Formula ~> SatSolveResult
[special (
id-hook SatSolverSymbol
op-hook trueSymbol (True : ~> Formula)
op-hook falseSymbol (False : ~> Formula)
op-hook notSymbol (~_ : Formula ~> Formula)
op-hook nextSymbol (O_ : Formula ~> Formula)
op-hook andSymbol (_/\_ : Formula Formula ~> Formula)
op-hook orSymbol (_\/_ : Formula Formula ~> Formula)
op-hook untilSymbol (_U_ : Formula Formula ~> Formula)
op-hook releaseSymbol (_R_ : Formula Formula ~> Formula)
op-hook formulaListSymbol
(_;_ : FormulaList FormulaList ~> FormulaList)
op-hook nilFormulaListSymbol (nil : ~> FormulaList)
op-hook modelSymbol
(model : FormulaList FormulaList ~> SatSolveResult)
term-hook falseTerm (false)
)] .
op counterexample : FormulaList FormulaList -> TautCheckResult [ctor] .
op tautCheck : Formula ~> TautCheckResult .
op $invert : SatSolveResult -> TautCheckResult .
var F : Formula .
vars L C : FormulaList .
eq tautCheck(F) = $invert(satSolve(~ F)) .
eq $invert(false) = true .
eq $invert(model(L, C)) = counterexample(L, C) .
endfm
fmod SATISFACTION is
protecting BOOL .
sorts State Prop .
op _|=_ : State Prop -> Bool [frozen] .
endfm
fmod MODEL-CHECKER is
protecting QID .
including SATISFACTION .
including LTL .
subsort Prop < Formula .
*** transitions and results
sorts RuleName Transition TransitionList ModelCheckResult .
subsort Qid < RuleName .
subsort Transition < TransitionList .
subsort Bool < ModelCheckResult .
ops unlabeled deadlock : -> RuleName .
op {_,_} : State RuleName -> Transition [ctor] .
op nil : -> TransitionList [ctor] .
op __ : TransitionList TransitionList -> TransitionList [ctor assoc id: nil] .
op counterexample : TransitionList TransitionList -> ModelCheckResult [ctor] .
op modelCheck : State Formula ~> ModelCheckResult
[special (
id-hook ModelCheckerSymbol
op-hook trueSymbol (True : ~> Formula)
op-hook falseSymbol (False : ~> Formula)
op-hook notSymbol (~_ : Formula ~> Formula)
op-hook nextSymbol (O_ : Formula ~> Formula)
op-hook andSymbol (_/\_ : Formula Formula ~> Formula)
op-hook orSymbol (_\/_ : Formula Formula ~> Formula)
op-hook untilSymbol (_U_ : Formula Formula ~> Formula)
op-hook releaseSymbol (_R_ : Formula Formula ~> Formula)
op-hook satisfiesSymbol (_|=_ : State Formula ~> Bool)
op-hook qidSymbol (<Qids> : ~> Qid)
op-hook unlabeledSymbol (unlabeled : ~> RuleName)
op-hook deadlockSymbol (deadlock : ~> RuleName)
op-hook transitionSymbol ({_,_} : State RuleName ~> Transition)
op-hook transitionListSymbol
(__ : TransitionList TransitionList ~> TransitionList)
op-hook nilTransitionListSymbol (nil : ~> TransitionList)
op-hook counterexampleSymbol
(counterexample : TransitionList TransitionList ~> ModelCheckResult)
term-hook trueTerm (true)
)] .
endfm
This diff is collapsed.
***(
This file is part of the Maude 2 interpreter.
Copyright 1997-2014 SRI International, Menlo Park, CA 94025, USA.
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
)
***
*** SMT bindings.
*** Version alpha 104.
***
set include BOOL off .
set include BOOLEAN off .
fmod BOOLEAN is
sort Boolean .
op true : -> Boolean [special (id-hook SMT_Symbol (true))] .
op false : -> Boolean [special (id-hook SMT_Symbol (false))] .
op not_ : Boolean -> Boolean [prec 53 special (id-hook SMT_Symbol (not))] .
op _and_ : Boolean Boolean -> Boolean [gather (E e) prec 55 special (id-hook SMT_Symbol (and))] .
op _xor_ : Boolean Boolean -> Boolean [gather (E e) prec 57 special (id-hook SMT_Symbol (xor))] .
op _or_ : Boolean Boolean -> Boolean [gather (E e) prec 59 special (id-hook SMT_Symbol (or))] .
op _implies_ : Boolean Boolean -> Boolean [gather (e E) prec 61 special (id-hook SMT_Symbol (implies))] .
op _===_ : Boolean Boolean -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (===))] .
op _=/==_ : Boolean Boolean -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (=/==))] .
op _?_:_ : Boolean Boolean Boolean -> Boolean [gather (e e e) prec 71 special (id-hook SMT_Symbol (ite))] .
endfm
fmod INTEGER is
protecting BOOLEAN .
sort Integer .
op <Integers> : -> Integer [special (id-hook SMT_NumberSymbol (integers))] .
op -_ : Integer -> Integer [special (id-hook SMT_Symbol (-))] .
op _+_ : Integer Integer -> Integer [gather (E e) prec 33 special (id-hook SMT_Symbol (+))] .
op _*_ : Integer Integer -> Integer [gather (E e) prec 31 special (id-hook SMT_Symbol (*))] .
op _-_ : Integer Integer -> Integer [gather (E e) prec 33 special (id-hook SMT_Symbol (-))] .
op _div_ : Integer Integer -> Integer [gather (E e) prec 31 special (id-hook SMT_Symbol (div))] .
op _mod_ : Integer Integer -> Integer [gather (E e) prec 31 special (id-hook SMT_Symbol (mod))] .
op _<_ : Integer Integer -> Boolean [prec 37 special (id-hook SMT_Symbol (<))] .
op _<=_ : Integer Integer -> Boolean [prec 37 special (id-hook SMT_Symbol (<=))] .
op _>_ : Integer Integer -> Boolean [prec 37 special (id-hook SMT_Symbol (>))] .
op _>=_ : Integer Integer -> Boolean [prec 37 special (id-hook SMT_Symbol (>=))] .
op _===_ : Integer Integer -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (===))] .
op _=/==_ : Integer Integer -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (=/==))] .
op _?_:_ : Boolean Integer Integer -> Integer [gather (e e e) prec 71 special (id-hook SMT_Symbol (ite))] .
*** seems to break CVC4
op _divisible_ : Integer Integer -> Boolean [prec 51 special (id-hook SMT_Symbol (divisible))] .
endfm
fmod REAL is
protecting BOOLEAN .
sort Real .
op <Reals> : -> Real [special (id-hook SMT_NumberSymbol (reals))] .
op -_ : Real -> Real [special (id-hook SMT_Symbol (-))] .
op _+_ : Real Real -> Real [gather (E e) prec 33 special (id-hook SMT_Symbol (+))] .
op _*_ : Real Real -> Real [gather (E e) prec 31 special (id-hook SMT_Symbol (*))] .
op _-_ : Real Real -> Real [gather (E e) prec 33 special (id-hook SMT_Symbol (-))] .
op _/_ : Real Real -> Real [gather (E e) prec 31 special (id-hook SMT_Symbol (/))] .
op _<_ : Real Real -> Boolean [prec 37 special (id-hook SMT_Symbol (<))] .
op _<=_ : Real Real -> Boolean [prec 37 special (id-hook SMT_Symbol (<=))] .
op _>_ : Real Real -> Boolean [prec 37 special (id-hook SMT_Symbol (>))] .
op _>=_ : Real Real -> Boolean [prec 37 special (id-hook SMT_Symbol (>=))] .
op _===_ : Real Real -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (===))] .
op _=/==_ : Real Real -> Boolean [gather (e E) prec 51 special (id-hook SMT_Symbol (=/==))] .
op _?_:_ : Boolean Real Real -> Real [gather (e e e) prec 71 special (id-hook SMT_Symbol (ite))] .
endfm
fmod REAL-INTEGER is
protecting INTEGER .
protecting REAL .
op toReal : Integer -> Real [special (id-hook SMT_Symbol (toReal))] .
op toInteger : Real -> Integer [special (id-hook SMT_Symbol (toInteger))] .
op isInteger : Real -> Boolean [special (id-hook SMT_Symbol (isInteger))] .
endfm
set include BOOLEAN on .
***(
This file is part of the Maude 2 interpreter.
Copyright 2004-2006 SRI International, Menlo Park, CA 94025, USA.
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
)
***
*** Maude internet socket external objects.
*** Version 2.3.
***
mod SOCKET is
protecting STRING .
including CONFIGURATION .
op socket : Nat -> Oid [ctor] .
op createClientTcpSocket : Oid Oid String Nat -> Msg [ctor msg format (b o)] .
op createServerTcpSocket : Oid Oid Nat Nat -> Msg [ctor msg format (b o)] .
op createdSocket : Oid Oid Oid -> Msg [ctor msg format (m o)] .
op acceptClient : Oid Oid -> Msg [ctor msg format (b o)] .
op acceptedClient : Oid Oid String Oid -> Msg [ctor msg format (m o)] .
op send : Oid Oid String -> Msg [ctor msg format (b o)] .
op sent : Oid Oid -> Msg [ctor msg format (m o)] .
op receive : Oid Oid -> Msg [ctor msg format (b o)] .
op received : Oid Oid String -> Msg [ctor msg format (m o)] .
op closeSocket : Oid Oid -> Msg [ctor msg format (b o)] .
op closedSocket : Oid Oid String -> Msg [ctor msg format (m o)] .
op socketError : Oid Oid String -> Msg [ctor msg format (r o)] .
op socketManager : -> Oid
[special (
id-hook SocketManagerSymbol
op-hook succSymbol (s_ : Nat ~> NzNat)
op-hook stringSymbol (<Strings> : ~> String)
op-hook socketOidSymbol (socket : Nat ~> Oid)
op-hook createClientTcpSocketMsg (createClientTcpSocket : Oid Oid String Nat ~> Msg)
op-hook createServerTcpSocketMsg (createServerTcpSocket : Oid Oid Nat Nat ~> Msg)
op-hook createdSocketMsg (createdSocket : Oid Oid Oid ~> Msg)
op-hook acceptClientMsg (acceptClient : Oid Oid ~> Msg)
op-hook acceptedClientMsg (acceptedClient : Oid Oid String Oid ~> Msg)
op-hook sendMsg (send : Oid Oid String ~> Msg)
op-hook sentMsg (sent : Oid Oid ~> Msg)
op-hook receiveMsg (receive : Oid Oid ~> Msg)
op-hook receivedMsg (received : Oid Oid String ~> Msg)
op-hook closeSocketMsg (closeSocket : Oid Oid ~> Msg)
op-hook closedSocketMsg (closedSocket : Oid Oid String ~> Msg)
op-hook socketErrorMsg (socketError : Oid Oid String ~> Msg))] .
endm
***(
This file is part of the Maude 2 interpreter.
Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA.
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
)
***
*** Strict total ordering on terms of a given kind.
*** Version 2.3.
***
fmod TERM-ORDER{X :: TRIV} is
protecting EXT-BOOL .
protecting CONVERSION .
protecting META-LEVEL .
vars E F : [X$Elt] .
vars Q P : Qid .
vars A B : NeTermList .
vars C D : TermList .
vars T U : Term .
op lt : [X$Elt] [X$Elt] -> Bool .
eq lt(E, F) = $lt(upTerm(E), upTerm(F)) .
op $lt : TermList TermList -> Bool .
eq $lt(Q, P) = string(Q) < string(P) .
eq $lt(Q[A], P) = $lt(Q, P) .
eq $lt(Q, P[B]) = $lt(Q, P) or-else Q == P .
eq $lt(Q[A], P[B]) =
if Q == P then $lt(A, B)
else $lt(Q, P)
fi .
eq $lt(empty, B) = true .
eq $lt(C, empty) = false .
eq $lt((T, C), (U, D)) =
if T == U then $lt(C, D)
else $lt(T, U)
fi .
endfm
This diff is collapsed.
This diff is collapsed.
Usage: ./psl.py <FILENAME>.psl
or
./psl.sh <FILENAME>.sh
The difference is that the second command also automatically loads the
generated Maude file into Maude-NPA, along with all the other files that
Maude-NPA needs to run properly, using the version of Maude included in the
repository (maude27 as of May 14 2015). Note that if you invoke the shell
script, then Maude-NPA will be loaded whether or not the PSL script
successfully executes. So invoking psl.py is recommended until the
specification is well-formed.
The program will generate one files:
<FILENAME>.maude.
<FILENAME>.maude
contains the Maude-NPA modules that can be loaded into the Maude-NPA.
Note that although the translation program itself works with Maude 2.6, the
Maude-NPA
version
that the generated modules are compatible with relies on a version of Maude
that is
not-quite-ready for release. Therefore, in addition to the translation code,
included
is an experimental version of Maude, the Maude prelude, and the Maude-NPA that
these modules are compatible with.
To load <FILENAME>.maude into the Maude-NPA, type:
./maude27 -no-prelude prelude.maude maude-npa.maude <FILENAME>.maude
For more details about PSL, see psl_description.pdf (a draft of Andrew Cholewa's
Spring 2015 Masters Thesis at University of Illinois at Urbana-Champaign),
included with this repository.
spec NEEDHAM-SCHROEDER is
Theory
types SName Name Key Nonce Masterkey Sessionkey .
subtypes Masterkey Sessionkey < Key .
subtype SName < Name .
subtype Name < Public .
// Nonce operator
op n : Name Fresh -> Nonce .
// Principals
op a : -> Name . // Alice
op b : -> Name . // Bob
op i : -> Name . // Intruder
// Server name
op s : -> SName .
// MKey
op mkey : Name Name -> Masterkey .
// Seskey
op seskey : Name Name Nonce -> Sessionkey .
//encrypt
op e : Key Msg -> Msg .
op d : Key Msg -> Msg .
// successor
op dec : Nonce -> Msg .
op null : -> Msg .
// Concatenation
op _;_ : Msg Msg -> Msg [gather (e E)] .
eq d(K:Key, e (K:Key, Z:Msg )) = Z:Msg .
eq e(K:Key, d (K:Key, Z:Msg )) = Z:Msg .
Protocol
vars ANAME BNAME SNAME A1NAME A2NAME B2NAME : Name .
var r r0 r1 r2 : Fresh .
vars M1 M2 : Msg .
vars KA KB : Key .
vars NA2 NB NB2 : Nonce .
roles A B S .
Def(A) = na := n(ANAME, r), keyAS := mkey(ANAME, SNAME) .
Def(B) = nb := n(BNAME, r0), keyBS := mkey(BNAME, SNAME),
nb1 := n(BNAME, r2) .
Def(S) = keyA2S := mkey(A2NAME, SNAME), keyB2S := mkey(B2NAME, SNAME),
sesKey := seskey(A2NAME, B2NAME, n(SNAME, r1)) .
In(A) = ANAME, SNAME, BNAME .
In(B) = SNAME, BNAME .
In(S) = SNAME .
1 . A -> B : ANAME |- A1NAME .
2 . B -> A : e(keyBS, A1NAME ; nb) |- M1 .
3 . A -> S : ANAME ; BNAME ; na ; M1 |-
A2NAME ; B2NAME ; NA2 ; e(keyB2S, A2NAME ; NB2) .
4 . S -> A : e(keyA2S, NA2 ; B2NAME ; sesKey ; e(keyB2S, sesKey ; NB2 ; A2NAME)) |-
e(keyAS, na ; BNAME ; KA ; M2) .
5 . A -> B : M2 |- e(keyBS, KB ; nb ; A1NAME) .
6 . B -> A : e(KB, nb1) |- e(KA, NB) .
7 . A -> B : e(KA, dec(NB)) |- e(KB, dec(nb1)) .
Out(A) = KA .
Out(B) = KB .
Out(S) = sesKey .
Intruder
var A : Name .
var r : Fresh .
var K : Key .
vars M M1 : Msg .
var N : Nonce .
=> A, s, n(i, r) .
=> mkey(i, A), mkey(A, i) .
=> mkey(i, s), mkey(s, i) .
M, M1 <=> M ; M1 .
K, M => d(K, M), e(K, M) .
N <=> dec(N) .
Attacks
0 .
//Get rid of In(), Out() and replace it with
//Subst() that looks at all the variables.
B executes protocol .
Subst(B) = A1NAME |-> a, BNAME |-> b, SNAME |-> s .
ends
spec Carlse-SK is
Theory
types Uname Sname Name Key Nonce Masterkey Sessionkey .
subtype Masterkey Sessionkey < Key .
subtype Sname Uname < Name .
subtype Name < Public .
op n : Name Fresh -> Nonce .
ops a b i : -> Uname [ctor] .
op s : -> Sname [ctor] .
op mkey : Name Name -> Masterkey [comm] .
op seskey : Name Name Nonce -> Sessionkey .
op e : Key Msg -> Msg .
op d : Key Msg -> Msg .
op _;_ : Msg Msg -> Msg [gather (e E)] .
var K : Key .
var Z : Msg .
eq d(K:Key, e (K:Key, Z:Msg )) = Z:Msg .
eq e(K:Key, d (K:Key, Z:Msg )) = Z:Msg .
/*
A -> B : A,na
B -> S : A,na,B,nb
S -> B : E(kbs:kab,nb,A),E(kas:na,B,kab)
B -> A : E(kas:na,B,kab),E(kab:na),nb'
A -> B : E(kab:nb')
*/
Protocol
vars ANAME BNAME ANAME1 ANAME2 BNAME1 : Uname .
var SNAME : Sname .
vars M N MA : Msg .
vars NA NA1 NB NB1 : Nonce .
var K : Key .
var SKA SKB : Sessionkey .
vars r r1 r2 : Fresh .
roles A B S .
Def(A) = na := n(ANAME, r), kas := mkey(ANAME, s) .
Def(B) = nb := n(BNAME, r), kbs := mkey(BNAME, s),
nb1 := n(BNAME, r1) .
Def(S) = ns := n(SNAME, r2), kab := seskey(ANAME2, BNAME1, ns),
ksa := mkey(ANAME2, SNAME), ksb := mkey(BNAME1, SNAME) .
In(A) = ANAME, BNAME, SNAME .
In(B) = BNAME, SNAME .
In(S) = SNAME .
1 . A -> B : ANAME ; na
|- ANAME1 ; NA .
2 . B -> S : ANAME1 ; NA ; BNAME ; nb
|- ANAME2 ; NA1 ; BNAME1 ; NB .
3 . S -> B : e(ksb, kab ; NB ; ANAME2) ; e(ksa, NA1 ; BNAME1 ; kab)
|- e(kbs, SKB ; nb ; ANAME1) ; MA .
4 . B -> A : MA ; e(SKB, NA) ; nb1
|- e(kas, na ; BNAME ; SKA) ; e(SKA, na) ; NB1 .
5 . A -> B : e(SKA, NB1)
|- e(SKB, nb1) .
Out(A) = SKA, NB1, na .
Out(B) = SKB, nb1, nb, NA .
Out(S) = kab, NB, NA1 .
Intruder
vars ANAME : Uname .
var r : Fresh .
vars M N : Msg .
var K : Key .
=> ANAME, s, mkey(i, s), mkey(i, ANAME) .
K, M => d(K, M), e(K, M) .
M, N <=> M ; N .
Attacks
0 .
B executes protocol .
Subst(B) = ANAME1 |-> a , BNAME |-> b, SNAME |-> s .
1 .
B executes protocol .
Subst(B) = ANAME1 |-> a, BNAME |-> b, SNAME |-> s .
Intruder learns SKB .
2 .
B executes protocol .
Subst(B) = ANAME1 |-> a, BNAME |-> b, SNAME |-> s .
without:
A executes protocol .
Subst(A) = ANAME |-> a, BNAME |-> b, SNAME |-> s, NB1 |-> n(b, r1) .
ends
spec Danning-Sacco is
Theory
types UName SName Name Key Nonce Masterkey Sessionkey .
subtype Masterkey Sessionkey < Key .
subtype SName UName < Name .
subtype Name < Public .
op n : Name Fresh -> Nonce .
op t : Name Fresh -> Nonce .
ops a b i : -> UName [ctor] .
op s : -> SName [ctor] .
op mkey : Name Name -> Masterkey .
op seskey : Name Name Nonce -> Sessionkey .
op e : Key Msg -> Msg .
op d : Key Msg -> Msg .
op _;_ : Msg Msg -> Msg [gather (e E)] .
var K : Key .
var Z : Msg .
eq d(K, e(K, Z)) = Z .
eq e(K, d(K, Z)) = Z .
Protocol
vars ANAME BNAME AS BS AB : UName .
var SNAME : SName .
vars r r' : Fresh .
vars TSA TSB : Nonce .
var K : Key .
vars SK SK1 SKA SKB : Sessionkey .
vars M N X Y : Msg .
roles A B S .
In(A) = ANAME, BNAME, SNAME .
In(B) = BNAME, SNAME .
In(S) = SNAME .
Def(A) = kas := mkey(ANAME, SNAME) .
Def(B) = kbs := mkey(BNAME, SNAME) .
Def(S) = kab := seskey(AS, BS, n(SNAME,r)), ts := t(SNAME, r'),
ksa := mkey(AS, SNAME), ksb := mkey(BS, SNAME) .
1 . A -> S : ANAME ; BNAME |- AS ; BS .
2 . S -> A : e(ksa, BS ; kab ; ts ; e(ksb, AS ; kab ; ts))
|- e(kas, BNAME ; SKA ; TSA ; M) .
3 . A -> B : M |- e(kbs, AB ; SKB ; TSB) .
Out(A) = SKA, TSA .
Out(B) = SKB, TSB .
Out(S) = kab, ts .
Intruder
var D : Name .
var r : Fresh .
var K : Key .
vars M N : Msg .
=> D, n(i, r), t(i, r) .
=> mkey(i, D), mkey(D, i) .
K, M => d(K, M), e(K, M) .
M, N <=> M ; N .
Attacks
0 .
A executes protocol .
Subst(A) = ANAME |-> a , BNAME |-> b, SNAME |-> s .
1 .
A executes protocol .
Subst(A) = ANAME |-> a , BNAME |-> b, SNAME |-> s .
Intruder learns SKA .
2 .
S executes protocol .
Subst(S) = AS |-> a, BS |-> b, SNAME |-> s .
Intruder learns kab .
ends
spec ISO5 is
Theory
types UName SName Name Key Nonce Masterkey Sessionkey .
subtype Masterkey Sessionkey < Key .
subtype SName UName < Name .
subtype Name < Public .
op n : Name Fresh -> Nonce .
ops a b i : -> UName [ctor] .
op s : -> SName [ctor] .
op mkey : Name Name -> Masterkey [comm] .
op seskey : Name Name Nonce -> Sessionkey .
op e : Key Msg -> Msg .
op d : Key Msg -> Msg .
op _;_ : Msg Msg -> Msg [gather (e E)] .
var K : Key .
var Z : Msg .
eq d(K, e(K, Z)) = Z .
eq e(K, d(K, Z)) = Z .
/*
A -> B : A,na
B -> S : A,na,B,nb1
S -> B : E(kbs:nb1,kab,A), E(kas:na,kab,B)
B -> A : E(kas:na,kab,B),E(kab:nb,na)
A -> B : E(kab:na,nb)
*/
Protocol
vars ANAME BNAME AB AS BS : UName .
var SNAME : SName .
vars K : Key .
vars SKA SKB : Sessionkey .
vars r r' : Fresh .
vars NAB NAS NBA NBS : Nonce .
var MA : Msg .
roles A B S .
Def(A) = na := n(ANAME, r), kas := mkey(ANAME, s) .
In(A) = ANAME, BNAME, SNAME .
Def(B) = nb := n(BNAME, r), nb1 := n(BNAME, r'), kbs := mkey(BNAME,s) .
In(B) = BNAME, SNAME .
Def(S) = ksa := mkey(AS, s), ksb := mkey(BS, s),
kab := seskey(AS, BS, n(s,r)) .
In(S) = SNAME .
1 . A -> B : ANAME ; na
|- AB ; NAB .
2 . B -> S : AB ; NAB ; BNAME ; nb1
|- AS ; NAS ; BS ; NBS .
3 . S -> B : e(ksb, NBS ; kab ; AS) ; e(ksa, NAS ; kab ; BS)
|- e(kbs, nb1 ; SKB ; AB) ; MA .
4 . B -> A : MA ; e(SKB, nb ; NAB)
|- e(kas, na ; SKA ; BNAME ) ; e(SKA, NBA ; na) .
5 . A -> B : e(SKA, na ; NBA)
|- e(SKB, NAB ; nb) .
Out(A) = na, NBA, SKA .
Out(B) = NAB, nb, nb1, SKB .
Out(S) = NAS, NBS, kab .
Intruder
vars C D : Name .
var K : Key .
vars M N : Msg .
var r : Fresh .
=> C, s, mkey(i, D), mkey(i, s) .
K, M => d(K, M), e(K, M) .
M, N <=> M ; N .
Attacks
0 .
B executes protocol .
Subst(B) = AB |-> a , BNAME |-> b, SNAME |-> s .
1 .
B executes protocol .
Subst(B) = AB |-> a , BNAME |-> b , SNAME |-> s .
Intruder learns SKB .
2 .
B executes protocol .
Subst(B) = AB |-> a , BNAME |-> b , SNAME |-> s .
without:
A executes protocol .
Subst(A) = ANAME |-> a, BNAME |-> b , SNAME |-> s, NBA |-> n(b, r) .
ends
spec Kao-Chow is
Theory
types UName SName Name Key Nonce Masterkey Sessionkey .
subtype Masterkey Sessionkey < Key .
subtype SName UName < Name .
subtype Name < Public .
op n : Name Fresh -> Nonce .
op t : Name Fresh -> Nonce .
ops a b i : -> UName [ctor] .
op s : -> SName [ctor] .
op mkey : Name Name -> Masterkey .
op seskey : Name Name Nonce -> Sessionkey .
op e : Key Msg -> Msg .
op d : Key Msg -> Msg .
op _;_ : Msg Msg -> Msg [gather (e E)] .
var K : Key .
var Z : Msg .
eq d(K, e(K, Z)) = Z .
eq e(K, d(K, Z)) = Z .
/*
A -> S : A , B , na
S -> B : E(kas:A,B,na,kab) , E(kbs:A,B,na,kab)
B -> A : E(kas:A,B,na,kab) , E(kab:na) , nb
A -> B : E(kab:nb)
*/
Protocol
vars ANAME BNAME : UName .
var SNAME : SName .
vars MA M N : Msg .
vars r r1 r2 : Fresh .
var NAB : Nonce .
vars SKA SKB : Sessionkey .
var NAS NBS : Nonce .
var NBA : Nonce .
roles A B S .
In(A) = ANAME, BNAME, SNAME .
In(B) = ANAME, BNAME, SNAME .
In(S) = ANAME, BNAME, SNAME .
Def(A) = na := n(ANAME, r), kas := mkey(ANAME, s) .
Def(B) = nb := n(ANAME, r1), kbs := mkey(BNAME, s) .
Def(S) = kas := mkey(ANAME, s), kbs := mkey(BNAME, s),
kab := seskey(ANAME,BNAME,n(s,r2)) .
1 . A -> S : ANAME ; BNAME ; na
|- ANAME ; BNAME ; NAS .
2 . S -> B : e(kas, ANAME ; BNAME ; NAS ; kab) ; e(kbs, ANAME ; BNAME ; NAS ; kab)
|- MA ; e(kbs, ANAME ; BNAME ; NAB ; SKB) .
3 . B -> A : MA ; e(SKB, NAB) ; nb
|- e(kas, ANAME ; BNAME ; na ; SKA) ; e(SKA, na) ; NBA .
4 . A -> B : e(SKA, NBA)
|- e(SKB, nb) .
Out(A) = na, NBA, SKA .
Out(B) = NAB, nb, SKB .
Out(S) = NAS, NBS, kab .
Intruder
var D : Name .
var r : Fresh .
var K : Key .
vars M N : Msg .
=> D, n(i, r), mkey(i, D), mkey(D, i) .
K, M => d(K, M), e(K, M) .
M ; N <=> M, N .
Attacks
0 .
B executes protocol .
Subst(B) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
1 .
B executes protocol .
Subst(B) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
Intruder learns SKB .
2 .
B executes protocol .
Subst(B) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
without:
A executes protocol .
Subst(A) = ANAME |-> a, BNAME |-> b, SNAME |-> s .
ends
spec Otway-Rees is
Theory
types UName SName Name Key Nonce Masterkey
Sessionkey .
subtypes Masterkey Sessionkey < Key .
subtypes SName UName < Name < Public .
op n : Name Fresh -> Nonce .
ops a b i : -> UName .
op s : -> SName .
op mkey : Name Name -> Masterkey .
op seskey : Name Name Nonce -> Sessionkey .
op e : Key Msg -> Msg . //encryption
op d : Key Msg -> Msg . //decryption
op _;_ : Msg Msg -> Msg [gather (e E)] .
var K : Key .
var Z : Msg .
eq d(K, e(K, Z)) = Z .
eq e(K, d(K, Z)) = Z .
Protocol
vars ANAME BNAME : UName .
var SNAME : SName .
vars r r' r'' rM : Fresh .
vars RA CB CS RB : Nonce .
vars M1 MA : Msg .
var KCA KCB : Sessionkey .
roles A B S .
Def(A) = c := n(ANAME, rM), ra := n(ANAME, r),
skA := mkey(ANAME, SNAME) .
Def(B) = rb := n(BNAME, r'),
skB := mkey(BNAME, SNAME) .
Def(S) = skA := mkey(ANAME, SNAME),
skB := mkey(BNAME, SNAME),
kc := seskey(ANAME, BNAME,
n(SNAME, r'')) .
In(A) = ANAME, BNAME, SNAME .
In(B) = ANAME, BNAME, SNAME .
In(S) = ANAME, BNAME, SNAME .
1 . A -> B : c ; ANAME ; BNAME ; e(skA, ra ; c ;
ANAME ; BNAME)
|- CB ; ANAME ; BNAME ; M1 .
2 . B -> S : CB ; ANAME ; BNAME ;
M1 ;
e(skB, rb ; CB ; ANAME ; BNAME)
|- CS ; ANAME ; BNAME ;
e(skA, RA ; CS ; ANAME ; BNAME) ;
e(skB, RB ; CS ; ANAME ; BNAME) .
3 . S -> B : CS ; e(skA, RA ; kc) ;
e(skB, RB ; kc)
|- CB ; MA ;
e(skB, rb ; KCB) .
4 . B -> A : CB ; MA
|- c ; e(skA, ra ; KCA) .
Out(A) = c, ra, KCA .
Out(B) = rb, KCB, MA, M1, CB .
Out(S) = kc, RA, RB, CS .
Intruder
vars P : UName .
var S : SName .
vars K : Key .
vars N M : Msg .
=> s, P, mkey(i, s) .
M, N <=> M ; N .
K, M => d(K, M), e(K, M) .
P => mkey(P, i), mkey(i, P) .
Attacks
0 .
A executes protocol .
Subst(A) = ANAME |-> a, BNAME |-> b,
SNAME |-> s .
1 .
A executes protocol .
Subst(A) = ANAME |-> a, BNAME |-> b,
SNAME |-> s .
Intruder learns KCA .
2 .
A executes protocol .
Subst(A) = ANAME |-> a, BNAME |-> b,
SNAME |-> s .
without:
B executes protocol .
Subst(B) = M1 |-> e(skA, c ; ra ; ANAME ;
BNAME),
ANAME |-> a, BNAME |-> b,
SNAME |-> s .
ends
This diff is collapsed.
spec Woolam is
Theory
types UName SName Name Key Nonce Masterkey Sessionkey .
subtype Masterkey Sessionkey < Key .
subtype SName UName < Name .
subtype Name < Public .
op n : Name Fresh -> Nonce .
ops a b i : -> UName [ctor] .
op s : -> SName [ctor] .
op mkey : Name Name -> Masterkey .
op seskey : Name Name Nonce -> Sessionkey .
op e : Key Msg -> Msg .
op d : Key Msg -> Msg .
op _;_ : Msg Msg -> Msg [gather (e E)] .
var K : Key .
var Z : Msg .
eq d(K, e(K, Z)) = Z .
eq e(K, d(K, Z)) = Z .
/*
A -> B : A
B -> A : nb
A -> B : E(kas:nb)
B -> S : E(kbs:A,E(kas:nb))
S -> B : E(kbs:nb)
*/
Protocol
vars ANAME BNAME : UName .
var SNAME : SName .
vars NB NBS : Nonce .
vars MA M N : Msg .
var r : Fresh .
var K : Key .
var D : Name .
roles A B S .
In(A) = ANAME, BNAME, SNAME .
In(B) = ANAME, BNAME, SNAME .
In(S) = ANAME, BNAME, SNAME .
Def(A) = kas := mkey(ANAME, s) .
Def(B) = nb := n(BNAME,r), kbs := mkey(BNAME, s) .
Def(S) = kas := mkey(ANAME,s), kbs := mkey(BNAME,s) .
1 . A -> B : ANAME |- ANAME .
2 . B -> A : nb |- NB .
3 . A -> B : e(kas, NB) |- MA .
4 . B -> S : e(kbs, ANAME ; MA)
|- e(kbs, ANAME ; e(kas, NBS)) .
5 . S -> B : e(kbs, NBS)
|- e(kbs, nb) .
Out(A) = NB .
Out(B) = nb .
Out(S) = NB .
Intruder
var D : Name .
var r : Fresh .
var K : Key .
vars M N : Msg .
=> D, n(i, r), mkey(D, i), mkey(i, D) .
K, M => d(K, M), e(K, M) .
M, N <=> M ; N .
Attacks
//Empty attack for debugging purposes. If an "attack" isn't found, then
//there's something wrong with the specification.
0 .
B executes protocol .
Subst(B) = ANAME |-> a , BNAME |-> b, SNAME |-> s .
ends
spec Yahalom is
Theory
types Uname Sname Name Key Nonce Masterkey Sessionkey .
subtype Masterkey Sessionkey < Key .
subtype Sname Uname < Name .
subtype Name < Public .
op n : Name Fresh -> Nonce .
ops a b i : -> Uname [ctor] .
op s : -> Sname [ctor] .
op mkey : Name Name -> Masterkey .
op seskey : Name Name Nonce -> Sessionkey .
op e : Key Msg -> Msg .
op d : Key Msg -> Msg .
op _;_ : Msg Msg -> Msg [gather (e E)] .
eq d(K:Key, e(K:Key, Z:Msg )) = Z:Msg .
eq e(K:Key, d(K:Key, Z:Msg )) = Z:Msg .
/*
A -> B : A,na
B -> S : B,E(kbs:A,na,nb)