Home

view

1. ids e g server spy message tags ProVerif Declaring Constructors Constructor declarations private fun id n This declares a constructor id of arity n Examples fun encrypt 2 fun sign 2 fun hash 1 Private constructors can be useful too private fun serverkey 1 serverkey Alice is the key that Alice shares with the server The server can use this constructor to look up client keys The attacker cannot use this constructor ProVerif Declaring Destructors Destructor declarations private reduc id M N This declares a destructor id with its reduction rule The messages M N must not contain names but typically contain variables Itis also allowed to associate several reduction rules separated by semicolons with a single destructor Example reduc decrypt encrypt x y y X ProVerif Process Macros Process macros let id process After this declaration you can refer to the process by id ProVerif textually replaces the id by the process ProVerif Pattern matching ProVerif supports pattern matching both at input and in let expressions but only against possibly nested tuples To match you need to precede the id with To bind omit the Examples let tag B x decrypt ctext k in This pattern is matched by a triples tag B M binding M to x let hash x decrypt ctext k in No This is not
2. of names The closed process O is an S adversary iff its free names are contained in S The closed process P preserves the secrecy of n from S iff P O does not output M on c for any cin S This secrecy definition is slightly different from our earlier definition from class The differences are It defines secrecy for names only not for variables It defines secrecy for free names but not for new bound names The above definition could be adapted to define secrecy for new bound names but it would make the statement of the soundness theorem slightly uglier Soundness of the Logic Translation Soundness Theorem Let P be a closed process and s S If atftacker s cannot be logically derived from B P S then P preserves the secrecy of s from S Abadi and Blanchet s proof of this theorem is interesting e It translates B P S to an instance of a generic type system and relies on a soundness theorem for the type system See AB05 for details if interested Horn Clauses for an Unsafe Protocol A B s This process does not preserve secrecy of s from net Horn clauses B P net Initial attacker knowledge attacker net e Attacker rules mess x y A attacker x attacker y attacker x attacker y mess x y Protocol rules mess net s attacker s is logically derivable from these rules And here is how From mess net s and attacker net and
3. the first attacker rule it follows that attacker s by logical implication Horn Clauses for a Safe Protocol A B shk This process preserves secrecy of s from net Horn clauses B P net Initial attacker knowledge attacker net Attacker rules mess x y A attacker x attacker y attacker x attacker y gt mess x y attacker x attacker y gt attacker encrypt x y attacker encrypt x y attacker y attacker x Protocol rules mess net encrypt s k attacker s is not logically derivable from these rules Why not We ll see next time how ProVerif checks this systematically Looking at ProVerif s Horn Clauses At the top of ProVerif s output you always see a sequence of numbered rules This is the Horn clause representation of your spi calculus protocol ProVerif seems to use a slightly different translation that makes more use of the attacker predicate and less use of the mess predicate The translation sketched is from Abadi and Blanchet s paper ABO5 Why do Names have Arguments When looking at ProVerif s output you will notice that each name is associated with a possibly empty list of arguments e g n x y c The arguments record messages that existed before n got generated This information helps the theorem prover to rule out impossibilities Example P inp net x inp net y new n P When translating P the name
4. used as a receiving channel This is for instance the case for protocols that use only global channels like net as it is often the case in our protocol models ProVerif Attack Traces ProVerif s attack traces are sequences of output events input events correspondence events The attacker s input output events are omitted Often attack traces are contaminated by initialization messages Names found in the program text are subscripted by numbers This is because a single name in the program text corresponds to many names at runtime if inside a replication ProVerif Pitfalls to Avoid Often typos result in unreachable code Unreachable code is safe ProVerif does not check for typos Your protocol may verify due to a typo To prevent this Declare all free names Check for warnings at the very top of the output Test if you reach the end of the protocol by inserting a secrecy violation at the end query attacker typoflag new typoflag out net typoflag x end of the protocol x If the end of the protocol is reachable ProVerif finds the obvious attack on this From Spi calculus to Logic Formulas Now we will sketch how ProVerif translates spi calculus processes to a set of logic formulas Via this translation ProVerif reduces the secrecy problem for cryptographic protocols to a logical problem The translation is sound If no secrecy violation can be logi
5. z hash y then stop Executing P4 Pg Pa Pg new m let z decrypt encrypt hash m k k in if z hash m then stop decrypt encrypt hash m k k hash m new m if hash m hash m then stop ProVerif Top level Syntax A ProVerif source consists of asequence of declarations a process ProVerif sources decl process process Declarations declare free names constructors destructors process macros queries and possibly other things Processes are written in a version of the generic spi calculus ProVerif Names and Variables Names New bound identifiers are names Globally declared free identifiers are names Undeclared free identifiers are names Avoid these Variables Let bound identifiers are variables Input bound identifiers are variables Declare all your free names ProVerif warns you when your model contains undeclared free names Unfortunately it is easy to miss these warnings as they are at the very top of some very verbose output Check for these warnings and get rid of them as undeclared free names are almost always typos ProVerif Declaring Free Names Free names are public by default can optionally be declared private private free names are equivalent to names that are new bound in front of the main process Free name declarations private free idy idp Typical examples untrusted channels e g net agent
6. Verification of Security Protocols Chapter 5 ProVerif A Resolution Prover for Protocol Verification Christian Haack March 10 2008 Plan for Today We will learn about a tool called ProVerif ProVerif s input language is a generic variant of the spi calculus Unlike Cryptyc ProVerif does not require type annotations ProVerif fully automatically tries to prove that the protocol is robustly safe There are three possible outcomes ProVerif succeeds to prove robust safety ProVerif finds an attack as a counterexample to robust safety ProVerif can neither prove nor disprove robust safety In rare cases ProVerif does not terminate A Generic Spi calculus ProVerif s input language is a generic variant of the spi calculus This input language allows users to define their own cryptographic primitives Generic Spi Messages Constructors f ranges over constructor symbols each one with a fixed arity Messages M N L K x variable n name i Mp constructor application Binary constructors for symmetric and asymmetric encryption encrypt M K M encrypted with symmetric key K pencrypt M K M encrypted with encryption key K Constructors for n tupling hashing and key extraction ntuple My Mn hash M enc K dec K You can add more Generic Spi Destructors Destructors g ranges over destructor symbols each one with a fixed arity For e
7. ach destructor there is an associated set of equations of the following form g M Mn M where M4 Mn M do not contain names Symmetric key decryption decrypt M K decrypt encrypt x y y X Asymmetric key decryption pdecrypt M K pdecrypt pencrypt x enc y dec y x Projection ithOfn M ithOfn ntuple x1 Xn Xi Generic Spi Processes Processes PRIOTRTOR out L M P inp L M P stop P Q IP new n P let x g M1 Mn in P else Q Conditionals let definitions and pattern matching for tuples can be defined as derived forms Generic Spi Operational Semantics Destructors define partial functions We write def g for the set of all equations for g We say that 9 N Nn is defined iff there exists an equation 9 M Mn M in def g and a substitution o such that oM N for all i 1 n In this case we define 9 N Nn aM Do example on board Operational semantics for destructors let x g M Mn in P else Q M x P if g M Mn M let x 9 M Mn in P else Q Q if g M4 Mn is undefined All other rules of the operational semantics are exactly as in the non generic spi calculus Generic Spi An Example A generates public message m A B m hash m In generic spi Pa new m out net m encrypt hash m k Pg _ inp net x let y4 Y2 x in let z decrypt ye2 k in if
8. allowed because it does not match against a possibly nested tuple ProVerif Events Events process event M process Events can be inserted into processes They generalize correspondence assertions They have no effect at runtime just like correspondence assertions Examples event beginSend A B m event endSend A B m ProVerif Queries In the declaration section you need to query for the properties that you want ProVerif to analyze Secrecy query attacker M Queries if the attacker can obtain M Many one correspondence query ev M gt ev N Queries if event M is always preceded by event N One one correspondence query evinj M gt evinj N Queries if event M is always preceded by event N and every trace contains at least as many N events as M events ProVerif Names in Queries If a query mentions a name i e an identifier that is declared free or new bound this name stands for itself Example query attacker s process new s Note that in a top level query you can mention a name that is generated deep inside a process Weird scoping To prevent ambiguities ProVerif warns you when you use the same name in two different new binders ProVerif Variables in Queries Variables in correspondence queries are implicitly universally quantified Example query ev endSend x y z gt ev beginSend x y Z T
9. cally derived from the formula set that results from translating protocol P then P is robustly safe for secrecy The translation is incomplete If a secrecy violation can be logically derived from the set of formulas that results from translating protocol P then P may in rare cases still be robustly safe for secrecy Horn Clauses Processes are translated to sets of Horn clauses Horn clauses are predicate logic formulas of the following form 7 7 7 VX Pa M1 A A Pr Mn Q N where n gt 0 and P Pn Q are predicate symbols The universal quantifier is usually left implicit Resolution provers take a set of Horn clauses and a goal 4x P M and check if this goal is provable from the clauses ProVerif is based on a resolution prover that is tailored for protocol verification _ Facts The translation from spi targets a formula language with only two predicates Facts a facts attacker M attacker knowledge mess L M channel messages The unary predicate attacker has the following meaning attacker M The attacker knows M The binary predicate mess with the following meaning mess L M Message M is out on channel L The Structure of the Translation Input e aclosed process P a subset S of P s free names representing public names all names except those declared private Output a set B P S of Horn clauses The top level definition e B P S Ini
10. his is like query V x y z ev endSend x y z gt ev beginSend x y z This is probably what you want ProVerif Variables in Queries Variables in secrecy queries are implicitly existentially quantified Example query attacker x This is like query J x attacker x This is always true and probably not what you want You usually want to query for secrecy of names not variables ProVerif Modeling Internal Threats This is done as always include a compromised agent called spy publish the spy s secrets Furthermore we need to use conditional end events if a lt gt spy then event endSend a b m instead of event endSend a b m Why The latter is trivially violated for a spy ProVerif Conditional Secrecy Recall our conditional secrecy assertions if a lt gt spy then secret M How do we represent these in ProVerif Like this query attacker flag new flag if a lt gt spy then out M flag ProVerif Conditional Secrecy query attacker flag new flag if a lt gt spy then out M flag Why does this encoding work o If the attacker learns M then he also learns flag because flag gets published on channel M If the attacker learns flag then he can only have learned it through channel M because flag does not occur anywhere else in the program So the attacker must know M The second argument only works if we know that M is never
11. n gets represented by n x y The arguments indicate that x and y existed before n got generated The prover now knows that x n x y is impossible because n has been generated after x Homework have posted a homework assignment using ProVerif It s due on Monday 31 March References Martin Abadi and Bruno Blanchet Analyzing security protocols with secrecy types and logic programs Jounal of the ACM 52 1 102 146 2005 Bruno Blanchet ProVerif User Manual
12. tialAttackerKnowledge S U AttackerRules U ProtocolRules P Initial Attacker Knowledge The initial attacker knowledge is simple A InitialAttackerKnowledge S attacker n neS The Attacker Rules The attacker rules only depend on the choice of constructors and destructors Show attacker rules for sym crypto on blackboard in parallel For each constructor f attacker x attacker xn attacker f x Xn For each destructor g for each equation g M Mn M in def g attacker M A attacker M attacker M mess x y attacker x attacker y In words If message y is out on channel x and the attacker knows channel x then the attacker knows message y attacker x attacker y mess x y e In words If the attacker knows channel x and message y then the attacker can output message y on channel x The Protocol Rules The Basic Idea Each output statement out c N generates a Horn clause of the following form mess c1 M4 A mess cn Mn gt mess c N where M4 Mn are the messages that have been received previously Examples P inp net x inp net y out net x y ProtocolRules P mess net x A mess net y mess net x y Q inp net x let y decrypt x k in out net y ProtocolRules Q mess net encrypt y k mess net y See AB05 for the details of the translation Secrecy Definition Secrecy AB05 Let S be a finite set

view

Contents

Download Pdf Manuals

Related Search

Related Contents