Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Verification of security protocols with state in ProVerif: Avoiding false attacks when verifying freshness
KTH, School of Computer Science and Communication (CSC).
2015 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesisAlternative title
Verifiering av säkerhetsprotokoll med persistenta variabler i ProVerif : Att undvika falska attacker vid verifiering av att genererade nycklar är unika (Swedish)
Abstract [en]

One of the issues when attempting to verify security properties of a protocol is how to model the protocol. We introduce a method for verifying event freshness in tools which use the applied π-calculus and are able to verify secrecy. Event freshness can be used to prove that a protocol never generates the same key twice. In this work we encode state in the applied π-calculus and perform bounded verification of freshness for MiniDC by using the ProVerif tool. MiniDC is a trivial protocol that for each iteration of a loop generates a unique key and outputs it to a private channel. When verifying freshness, the abstractions of ProVerif cause false attacks. We describe methods which can be used to avoid false attacks that appear when verifying freshness. We show how to avoid some false attacks introduced by private channels, state and protocols that disclose their secret. We conclude that the method used to verify freshness in MiniDCis impractical to use in more complicated protocols with state.

Abstract [sv]

Ett av problemen som uppstår vid verifiering av säkerhetsprotokoll är hur protokoll ska modelleras. Vi introducerar en metod för att verifiera att skapde termer inte har använts förr. Denna metod kan användas i program som använder applicerad π-kalkyl som input och kan verifiera sekretess. I detta arbete visar vi hur protokoll med persistenta variabler kan modelleras i applicerad π-kalkyl. Vi verifierar även MiniDC för ett begränsat antal iterationer med hjälp av ProVerif. MiniDC är ett enkelt protokoll som för varje iteration av en loop skapar en nyckel och skickar den över en privat kanal. När man verifierar att skapade termer inte har använts förr så introducerar ProVerifs abstraktioner falska attacker. Vi beskriver metoder som kan användas för att undvika dessa falska attacker. Dessa metoder kan användas för falska attacker introducerade av privata kanaler, persistenta variabler eller protokoll som avslöjar sin krypteringsnyckel. Vår slutsats är att metoden som används för att verifiera MiniDC är opraktisk att använda i mer komplicerade protokoll med persistenta variabler.

Place, publisher, year, edition, pages
2015.
Keyword [en]
formal verification ProVerif state counter applied pi calculus freshness security protocols
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-172323OAI: oai:DiVA.org:kth-172323DiVA: diva2:846632
External cooperation
Ericsson
Educational program
Master of Science in Engineering - Computer Science and Technology
Supervisors
Examiners
Available from: 2015-08-21 Created: 2015-08-17 Last updated: 2015-08-21Bibliographically approved

Open Access in DiVA

fulltext(893 kB)239 downloads
File information
File name FULLTEXT01.pdfFile size 893 kBChecksum SHA-512
748fb851d8dabe875ce48852ae7506bc3ae259de09f095637c9fba7c1cef983b1816b17b61a7a839338ae59eeceaa785117d381bdd6f40e8d922114d1c21b68b
Type fulltextMimetype application/pdf

By organisation
School of Computer Science and Communication (CSC)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 239 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 151 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf