Cervesatoiliano@itdnrlnavymil(2)

1、MSR 3:One Year LaterIliano Cervesatoilianoitd.nrl.ITT Industries, inc NRL Washington, DC/ilianoProtocol eXchange Seminar, UMBCMay 27-28, 2004NSPK in MSR 3A: princ. L: princ B:princ.pubK B nonce mset. B: princ. kB: pubK B. nA: nonce. net (nA, AkB), L (A, B, kB, nA) B: princ.

2、kB: pubK B. kA: pubK A. kA: prvK kA. nA: nonce. nB: nonce. net (nA, nBkA), L (A, B, kB, nA) net (nBkB)A B: nA, AkBB A: nA, nBkAA B: nBkBInterpretation of LRule invocationImplementation detailControl flowLocal state of roleExplicit viewImportant for DOSMSR 2 spec.1MSR 3: One Year LaterNSPK in MSR 3A:

3、princ. B: princ. kB: pubK B. nA: nonce. net (nA, AkB), (kA: pubK A. kA: prvK kA. nB: nonce. net (nA, nBkA) net (nBkB)A B: nA, AkBB A: nA, nBkAA B: nBkBSuccinctContinuation-passing styleRule asserts what to do nextLexical control flowState is implicitAbstractNot an MSR 2 spec.2MSR 3: One Year LaterLo

4、oks Familiar?A B: nA, AkBB A: nA, nBkAA B: nBkBProcess calculusA:princ.B: princ. kB: pubK B.kA: pubK A. kA: prvK kA. nB: nonce.nnA: (nA, AkB) .net .net (nBkB) . 0NA, AKBNA, NBKANBKBAlice (A,B,NA,NB) :NA Fresh, pA (A,B)Parametric strand3MSR 3: One Year LaterWhat is MSR 3?A new language for security p

5、rotocolsSupports State transition specsConservative over MSR 2Process algebraic specsRewriting re-interpretation of logicRich composable set of connectivesUniversal connectorNeutral paradigm4MSR 3: One Year LaterMore than the Sum of its PartsProcess- and transition-based specs.in the same languageCh

6、oose the paradigmUsers preferenceHighlight characteristics of interestSupport various verification techniques (FW)Mix and match stylesWithin a spec.Within a protocolWithin a role5MSR 3: One Year LaterWhat is in MSR 3 ?Security-relevant signatureNetworkEncryption, Typing infrastructureDependent types

7、SubsortingData Access Specification (DAS)Module systemEquationsFromMSR 2FromMSR 1From MSR 2implementationw-MultisetsMSR 2ProtocolsRepr. gap6MSR 3: One Year Laterw-MultisetsSpecification language for concurrent systemsCrossroad ofState transition languagesPetri nets, multiset rewriting, Process calcu

8、liCCS, p-calculus, (Linear) logicBenefitsAnalysis methods from logic and type theoryCommon ground for comparingMultiset rewritingProcess algebraAllows multiple styles of specificationUnified approachw-MultisetsMSR 2ProtocolsRepr. gap7MSR 3: One Year LaterSyntaxA:= aatomic object| 1 empty|A BA, Bform

9、ation|A BA Brewrite|Tno-op|A & BA | B choice|x. Ainstantiation|x. Ageneration|! AreplicationGeneralizes FO multiset rewriting (MSR 1-2)x1xn. a(x) y1yk. b(x,y)8MSR 3: One Year LaterState and TransitionsStatesS ; G ; DS ; DS is a listG and D arecommutative monoidsTransitionsS; G; D S; G; DS; G; D * S;

10、 D* for reflexive and transitive closureConstructor: “,”Empty: “”- logic- system w- rewriting - processes- security9MSR 3: One Year LaterTransition SemanticsS ; G ; (D, A, A B)S ; G ; (D, B)T (no rule)&S ; G ; (D, A1 & A2)S ; G ; (D, Ai)S ; G ; (D, x. A)S ; G ; (D, t/xA)if S |- tS ; G ; (D, x. A)(S,

11、 x) ; G ; (D, A)!S ; G ; (D, !A)S ; (G, A) ; DS ; (G, A) ; D S ; (G, A) ; (D, A)S ; G ; D * S ; D S ; G ; D * S ; Dif S ; G ; D S ; G ; D and S ; G ; D * S ; D 10MSR 3: One Year LaterLinear LogicFormulasA, B := a | 1 | A B | A B | ! A | T | A & B | x. A | x. ALV sequentsG ; D -S CGoalformulaSignatur

12、eUnrestrictedcontextLinearcontextConstructor: “,”Empty: “”- logic- system w- rewriting - processes- security11MSR 3: One Year LaterLogical DerivationsProof of C from D and GEmphasis on CC is inputFiniteClosedRules shownMajor premisePreserves CMinor premiseStarts subderivationG; D -S CG; D -S CG; D -

13、S CG; C -S C- logic- system w- rewriting - processes- security12MSR 3: One Year LaterA Rewriting Re-InterpretationTransitionFrom conclusionTo major premiseEmphasis on G, D and SC is output, at bestDoes not changePossibly infiniteOpenMinor premiseAuxiliary rewrite chainFiniteTopped with axiomG; D -S

14、CG; D -S CG; D -S CG; C -S C- logic- system w- rewriting - processes- security13MSR 3: One Year LaterInterpreting Unary RulesS; G; (D, !A) S; (G, A); DG; D, A -S,x CG; D, $x.A -S C G, A; D -S CG; D , !A -S CS |- t G; D, t/xA -S CG; D, x.A -S CG; D, A, B -S CG; D, AB -S CS; G; (D, AB ) S; G; (D, A, B

15、)S; G; (D, x. A) S; G; (D, t/xA)if S |- tS; G; (D, x. A) (S, x); G; (D, A)- logic- system w- rewriting - processes- security14MSR 3: One Year LaterBinary Rules and AxiomMinor premiseAuxiliary rewrite chainTop of treeFocus shifts to RHSAxiom ruleObservationG; D -S A G; D, B -S CG; D, D , AB -S CG; A

16、-S A- logic- system w- rewriting - processes- security15MSR 3: One Year LaterObservationsObservation statesS ; DIn D, we identify, with with 1Categorical semanticsIdentified with x1. xn. DFor S = x1, , xnDe Bruijns telescopesObservation transitionsS; G; D * S; DAG,G; A -S,S AG; D -S S. AD = DS; D =

17、S. D- logic- system w- rewriting - processes- security16MSR 3: One Year LaterInterpreting Binary RulesS; G; (D, D, A B) S; G; (D, B)if S; G; D * S; AG; D -S A G; D, B -S CG; D, D , AB -S CG; D -S A G; D, A -S C G; D, D -S CS; G; D, D S; G; (A, D) if S; G; D * S; AG; A -S AS; G; D * S; DS; G; D * S;

18、Dif S; G; D S; G; Dand S; G; D * S; D- logic- system w- rewriting - processes- security17MSR 3: One Year LaterFormal CorrespondenceSoundnessIfS ; G ; D * S,S; DthenG ; D -S S. DCompleteness?No! We have only crippled right rules ; ; a b, b c * ; a c- logic- system w- rewriting - processes- security18

19、MSR 3: One Year LaterSystem wWith cut, rule for can be simplified toS; G; (D, A, A B) S; G; (D, B)Cut elimination holds= in-lining of auxiliary rewrite chainsBut Careful with extra signature symbolsCareful with extra persistent objectsNo rule for needs a premise does not depend on *- logic- system w

20、- rewriting - processes- security19MSR 3: One Year LaterMultiset RewritingMultiset: set with repetitions alloweda := | a, aCommutative monoidMultiset rewriting (a.k.a. Petri nets)Rewriting within the monoid Fundamental model of distributed computingAlternative: Process AlgebrasBasis for security pro

21、tocol spec. languagesMSR family several othersMany extensions, more or less ad hoc- logic- system w- rewriting - processes- security20MSR 3: One Year LaterThe Atomic Objects of MSR 3 Atomic termsPrincipalsAKeysKNoncesNOtherRaw data, timestamp, ConstructorsEncryption_Pairing(_, _)OtherSignature, hash

22、, MAC, Fully definablePredicatesNetwork netMemory MAIntruderIw-MultisetsMSR 2ProtocolsRepr. gap21MSR 3: One Year LaterTypesFully definablePowerful abstraction mechanismAt various user-definable levelFinely tagged messagesUntyped: msg onlySimplify specification and reasoningAutomated type checkingSim

23、ple typesA : princn : noncem : msg, Dependent typesk : shK A BK : pubK AK : privK K, w-MultisetsMSR 2ProtocolsRepr. gap22MSR 3: One Year LaterSubsortingAllows atomic terms in messagesDefinableNon-transmittable termsSub-hierarchiesDiscriminant for type-flaw attackst : tw-MultisetsMSR 2ProtocolsRepr.

24、gap23MSR 3: One Year LaterData Access SpecificationPrevent illegitimate use of informationProtocol specification divided in rolesOwner = principal executing the roleA signing/encrypting with Bs keyA accessing Bs private data, Simple static checkCentral meta-theoretic notionDetailed specification of

25、Dolev-Yao access modelGives meaning to Dolev-Yao intruderCurrent effort towards integration in type systemDefinablePossibility of going beyond Dolev-Yao modelw-MultisetsMSR 2ProtocolsRepr. gap24MSR 3: One Year LaterModules and EquationsModulesBundle declarations with simple import/export interfaceKe

26、ep specifications tidyReusableEquations(For free from underlying Maude engine)Specify useful algebraic propertiesAssociativity of pairsAllow to go beyond free-algebra modelDec(k, Enc(k, M) = Mw-MultisetsMSR 2ProtocolsRepr. gap25MSR 3: One Year LaterState-Based vs. Process-BasedState-based languagesMu